simon: Let me explain some of the terminology here, because that may be where the confusion lies.
A scentence is a finite string symbols that satisfies a certain set of syntactic constraints.
A theory is a (possibly infinite) set of sentences. PA is a theory.
A proof from a theory T is a finite set of sentences, each of which is either an element of T, or follows from the ones before according to a fixed set of rules.
The notation PA + X, where X is a sentences is just the union of PA and {X}.
The notation PA |- Y means that a proof from PA that ends in Y exists.
Now I have left out some technical details, like what exactly are the syntactic constraints on sentences, and what is the fixed set of rules for proofs, but we have enough to say what the deduction theorem means. It says
PA + X |- Y ⇒ PA |- “X → Y”
or in english: if there is a proof from the theory PA + X to the scentence Y, then there is a proof from PA alone that X->Y.
So, you see, the deduction theorem is really just a technical lemma. It meerly shows that (in one particular way) our technical definition of a first order proof behaves the way it ought to.
Now on to Lob’s theorem, which says that if PA |- “◻C → C” then PA |- “C”. Now in general if you want to prove PA |- A implies that PA |- B, one way to do it is to write a first order proof inside of PA that starts with A and ends with B. But that is not what is going on here. Instead we start with a proof of “◻C->C” and do something totally different than a first order proof inside of PA in order to come up with a proof that PA |- C.
simon: Let me explain some of the terminology here, because that may be where the confusion lies.
A scentence is a finite string symbols that satisfies a certain set of syntactic constraints.
A theory is a (possibly infinite) set of sentences. PA is a theory.
A proof from a theory T is a finite set of sentences, each of which is either an element of T, or follows from the ones before according to a fixed set of rules.
The notation PA + X, where X is a sentences is just the union of PA and {X}.
The notation PA |- Y means that a proof from PA that ends in Y exists.
Now I have left out some technical details, like what exactly are the syntactic constraints on sentences, and what is the fixed set of rules for proofs, but we have enough to say what the deduction theorem means. It says
PA + X |- Y ⇒ PA |- “X → Y”
or in english: if there is a proof from the theory PA + X to the scentence Y, then there is a proof from PA alone that X->Y.
So, you see, the deduction theorem is really just a technical lemma. It meerly shows that (in one particular way) our technical definition of a first order proof behaves the way it ought to.
Now on to Lob’s theorem, which says that if PA |- “◻C → C” then PA |- “C”. Now in general if you want to prove PA |- A implies that PA |- B, one way to do it is to write a first order proof inside of PA that starts with A and ends with B. But that is not what is going on here. Instead we start with a proof of “◻C->C” and do something totally different than a first order proof inside of PA in order to come up with a proof that PA |- C.