Larry_D'Anna comments on The Cartoon Guide to Löb's Theorem - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (90)
simon:
OK so the question marks are boxes right? In that case then yes, PA |- "?(?C -> C) -> ?C". This is OK. The contradiction comes if PA |- "(?C->C)->C". But morally this doesn't have anything to do with the deduction theorem. PA proves Lob because everything in the proof of Lob is expressible inside of PA.
Like I said before, the deduction theorem is really just a technical lemma. If I'm doing ordinary mathematics (not logic), and I assume X, and prove Y, and then say "ok well now I've proved X -> Y", then I have not used the deduction theorem, because I'm writing a proof, not explicitly reasoning about proofs. The deduction theorem lies a meta level up, where we have a explicit, specific, technical definition of what constitutes a proof, and we are trying to prove theorems from that definition.
Nope, we are using an ordinary principle of mathematical reasoning. The deduction theorem says that if you have a proof that uses this principle and is otherwise first-order, you can convert it into a pure first order proof.
First order logic without any additional assumptions can't even express concepts like like PA. So, yea; that's why Gödel's theorem has that qualification, because there are plenty first order theories that are simple enough that they can't express integers.