You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

redxaxder comments on Probabilistic Löb theorem - Less Wrong Discussion

24 Post author: Stuart_Armstrong 26 April 2013 06:45PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (39)

You are viewing a single comment's thread.

Comment author: redxaxder 27 April 2013 11:52:08AM *  0 points [-]

Why would you leave out quantifiers? Requiring the reader to stick their own existential or universal quantification in the necessary places isn't very nice.

Is this the correct interpretation of your assumptions? If not, what is it? I am not interested in figuring out which axioms are required to make your proof (which is also missing quantifiers) work.

  • If ⊢ A, then ⊢ ∀(a < 1)(□a A).
  • ⊢ □aA → ∀(c < 1)(∃(b > 0)(□c□a+b A)).
  • ⊢ □a(A → B) → ∃(b > 0)(□bA → □a+bB).
Comment author: Larks 27 April 2013 12:20:12PM 2 points [-]

" So the following derivation principles seem reasonable, where the latin indexes (a,b,c...) are meant to represent numbers that can be arbitrarily close to zero"

so universally quantified, but in the meta language.

Comment author: redxaxder 27 April 2013 09:00:17PM 0 points [-]

Thank you.

Comment author: Stuart_Armstrong 27 April 2013 06:46:27PM *  0 points [-]

As Larks said, we can quantify (the meta language looking in), but the system itself can't quantify. Because then the system could reason that "∀x>0, P(A)<x" means "P(A)=0", which is the kind of thing that causes bad stuff to happen. Here, the system can show "P(A)<x" separately for any given x>0, but can't prove the same statement with the universal quantifier.

Comment author: redxaxder 27 April 2013 09:12:29PM 0 points [-]

Is it unreasonable of me to be annoyed at that kind of writing?

If I understand what's going on correctly, you have a real-indexed schema of axioms and each of them is in your system.

When I read the axiom list the first time I saw that the letters were free variables (in the language you and I are writing in) and assumed that you did not intend for them to be free variables in the formula. My suggestion of how to bind the variables (in the language we are writing in) was (very) wrong, but I still think that it's unclear as written.

Am I confused?

Comment author: Stuart_Armstrong 28 April 2013 07:36:25AM *  0 points [-]

Is it unreasonable of me to be annoyed at that kind of writing?

No, it's perhaps not the best explained post I've done. Though it was intended more for technical purposes.

Am I confused?

Not any more, I hope!