To argue that a proof is being made concluding ?C using the assumption ?(◻C → C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- ”?(◻C → C) → ?C”) (i.e. my interpretation of Löb’s Theorem)
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.
But the proof uses an additional assumption which is the antecedent of an implication, and comes to a conclusion which is the consequent of the implication. To get the implication, we must use the deduction theorem or something like it, right?
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.
Is this fact a theorem of first order logic without any additional assumptions, or is it merely a theorem of PA? I admit I don’t know, as I’m not very familiar with first order logic, but it intuitively seems to me that if first order logic were powerful enough on its own to express concepts like “PA proves X” it would probably be powerful enough to express arithmetic, in which case the qualification in Gödel’s theorem that it only applies to theories that express arithmetic would be superfluous.
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.
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.