Gentzen's hauptsatz
MoeBlee
studied all the technical details. I know that the hauptsatz says that
the cut-rule is not required. But why is that result so important and
prominent in mathematical logic?
Would someone (or any number of people) please explain - in rather non-
technical, layman's terms - what Gentzen's hauptsatz says and why it
is so important and prominent in mathematical logic. Does it pertain
only to technicalities of Gentzen's method of sequents, or is
something more general at stake? So, you see, I'm hoping for an
informal, relaxed preview of the signficance of the hauptsatz.
Daryl McCullough
MoeBlee says...
Gentzen's result is important because it proves that Peano arithmetic
(or whatever variant of arithmetic he was working with) is consistent:
there is no proof of a contradiction. It's a proof-theoretic (as opposed
to model-theoretic) proof of consistency.
The reason why cut-free proofs are important is that it is easy to
show that there can be no cut-free proof of a contradiction. So if
*every* proof can be converted into a cut-free proof, then it follows
that there is no proof of a contradiction, period.
--
Daryl McCullough
Ithaca, NY
herbzet
And THAT'S why we pay you the big bucks.
Thanks.
--
hz
Daryl McCullough
>And THAT'S why we pay you the big bucks.
Umm. I don't know if this is the right time to bring it up, but
speaking of big bucks, I haven't received a check from sci.logic
in a long time. I'm sure it's in the mail, right?
MoeBlee
wrote:
> In article <e9757737-7fbc-40a7-b2f3-0a474982b...@v5g2000prm.googlegroups.com>,
> Gentzen's result is important because it proves that Peano arithmetic
> (or whatever variant of arithmetic he was working with) is consistent:
> there is no proof of a contradiction. It's a proof-theoretic (as opposed
> to model-theoretic) proof of consistency.
This is classical PA we're talking about (not intutionistic PA, aka
'Heyting arithmetic' or 'HA')? (Though we also know they are
equiconsistent, right? That can be proven in what - HA, PA?)
If we were to formalize this proof-theoretic conistency proof, then
what would a typical formal system for it be? (Since it has to be a
system either stronger than PA or not comparable to PA).
> The reason why cut-free proofs are important is that it is easy to
> show that there can be no cut-free proof of a contradiction. So if
> *every* proof can be converted into a cut-free proof, then it follows
> that there is no proof of a contradiction, period.
Are you referring specifically to proofs from the axioms of PA? I
mean, it doesn't hold of ANY axiom set that you can't get a
contradiction from it using a cut-free proof, does it?
MoeBlee
Daryl McCullough
>
>On Jan 21, 8:52=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough)
>wrote:
>> In article <e9757737-7fbc-40a7-b2f3-0a474982b...@v5g2000prm.googlegroups.=
>com>,
>
>> Gentzen's result is important because it proves that Peano arithmetic
>> (or whatever variant of arithmetic he was working with) is consistent:
>> there is no proof of a contradiction. It's a proof-theoretic (as opposed
>> to model-theoretic) proof of consistency.
>
>This is classical PA we're talking about (not intutionistic PA, aka
>'Heyting arithmetic' or 'HA')? (Though we also know they are
>equiconsistent, right? That can be proven in what - HA, PA?)
I believe it is for intuitionistic PA, but for PA, I believe it
is straight-forward to show that classical PA is consistent if and
only if intuitionistic PA is.
>If we were to formalize this proof-theoretic conistency proof, then
>what would a typical formal system for it be? (Since it has to be a
>system either stronger than PA or not comparable to PA).
It's mostly formalizable in PA. Using PA, you can formalize what
a formula is, what a proof is, and what it means for a theory to
be consistent. You can also define the cut-elimination operation.
A proof of B by the cut rule basically amounts to two subproofs:
P1: A proof of B using another statement, A, as an assumption.
P2: A proof of A.
Cut-elimination is an operation on proofs that amounts to gluing
proof P2 everywhere that proof P1 uses A as an assumption.
Through the "proofs as programs" paradigm, cut elimination is
basically equivalent to beta reduction in the lambda calculus.
That's the step by which (lambda x . A) B is replaced by
A', where A' is formed from A by replacing all occurrences of
x by the term B.
What can't be proved in PA is that if you repeatedly apply cut
elimination, the process eventually terminates in a cut-free
proof. This fact is equivalent to the claim that epsilon-0 is
a computable ordinal. You can associate every proof in PA with
an ordinal less than epsilon-0 (actually, a representation for
the ordinal) in such a way that cut-elimination always reduces
the associated ordinal.
>> The reason why cut-free proofs are important is that it is easy to
>> show that there can be no cut-free proof of a contradiction. So if
>> *every* proof can be converted into a cut-free proof, then it follows
>> that there is no proof of a contradiction, period.
>
>Are you referring specifically to proofs from the axioms of PA? I
>mean, it doesn't hold of ANY axiom set that you can't get a
>contradiction from it using a cut-free proof, does it?
Cut elimination works with theories besides PA, but it doesn't
work with every theory. For example, as I understand it, proofs
in ZFC cannot be
MoeBlee
wrote:
> MoeBlee says...
> >On Jan 21, 8:52=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough)
> >wrote:
> >> In article <e9757737-7fbc-40a7-b2f3-0a474982b...@v5g2000prm.googlegroups.=
> >com>,
>
> >> Gentzen's result is important because it proves that Peano arithmetic
> >> (or whatever variant of arithmetic he was working with) is consistent:
> >> there is no proof of a contradiction. It's a proof-theoretic (as opposed
> >> to model-theoretic) proof of consistency.
>
> >This is classical PA we're talking about (not intutionistic PA, aka
> >'Heyting arithmetic' or 'HA')? (Though we also know they are
> >equiconsistent, right? That can be proven in what - HA, PA?)
>
> I believe it is for intuitionistic PA, but for PA, I believe it
> is straight-forward to show that classical PA is consistent if and
> only if intuitionistic PA is.
>
> >If we were to formalize this proof-theoretic conistency proof, then
> >what would a typical formal system for it be? (Since it has to be a
> >system either stronger than PA or not comparable to PA).
>
> It's mostly formalizable in PA.
Are we talking about the famous proof that uses induction on e0 in
addition to PA? If so, would I be correct to take it that the
hauptsatz is important for facilitating that proof?
> Using PA, you can formalize what
> a formula is, what a proof is, and what it means for a theory to
> be consistent. You can also define the cut-elimination operation.
>
> A proof of B by the cut rule basically amounts to two subproofs:
> P1: A proof of B using another statement, A, as an assumption.
> P2: A proof of A.
>
> Cut-elimination is an operation on proofs that amounts to gluing
> proof P2 everywhere that proof P1 uses A as an assumption.
Right, I know about that.
> Through the "proofs as programs" paradigm,
Is this the Curry-Howard isomorphism? Would you say something, in
rather basic, not-too-techical terms, what that is?
> cut elimination is
> basically equivalent to beta reduction in the lambda calculus.
> That's the step by which (lambda x . A) B is replaced by
> A', where A' is formed from A by replacing all occurrences of
> x by the term B.
>
> What can't be proved in PA is that if you repeatedly apply cut
> elimination, the process eventually terminates in a cut-free
> proof. This fact is equivalent to the claim that epsilon-0 is
> a computable ordinal. You can associate every proof in PA with
> an ordinal less than epsilon-0 (actually, a representation for
> the ordinal) in such a way that cut-elimination always reduces
> the associated ordinal.
I follow the gist of that; I'll ponder it more later.
> >> The reason why cut-free proofs are important is that it is easy to
> >> show that there can be no cut-free proof of a contradiction. So if
> >> *every* proof can be converted into a cut-free proof, then it follows
> >> that there is no proof of a contradiction, period.
>
> >Are you referring specifically to proofs from the axioms of PA? I
> >mean, it doesn't hold of ANY axiom set that you can't get a
> >contradiction from it using a cut-free proof, does it?
>
> Cut elimination works with theories besides PA, but it doesn't
> work with every theory. For example, as I understand it, proofs
> in ZFC cannot be
So it works for PA in particular, which is of particular concern, but
it may or may not work for other theories, if I understand you
correctly.
MoeBlee
Daryl McCullough
>Are we talking about the famous proof that uses induction on e0 in
>addition to PA? If so, would I be correct to take it that the
>hauptsatz is important for facilitating that proof?
Yes. You prove by induction on e0 that repeatedly applying
cut elimination on any proof in (intuitionistic) PA results
in a cut-free proof.
>> Using PA, you can formalize what
>> a formula is, what a proof is, and what it means for a theory to
>> be consistent. You can also define the cut-elimination operation.
>>
>> A proof of B by the cut rule basically amounts to two subproofs:
>> P1: A proof of B using another statement, A, as an assumption.
>> P2: A proof of A.
>>
>> Cut-elimination is an operation on proofs that amounts to gluing
>> proof P2 everywhere that proof P1 uses A as an assumption.
>
>Right, I know about that.
>
>> Through the "proofs as programs" paradigm,
>
>Is this the Curry-Howard isomorphism? Would you say something, in
>rather basic, not-too-techical terms, what that is?
Sure. You can associate proofs in intuitionistic logic with
terms in the lambda calculus. The basic rules are these:
1. Variables all have types associated with them.
2. Propositions (or statements) are considered types.
3. If x is a variable of type A, and A is a proposition,
then x is considered a proof of A (it's a proof by assumption)
3. If t is a proof of B, which uses variable x, and x has type A,
and A is a proposition, then (lambda x:A. t) is a proof of
A implies B.
4. If u is a proof of A implies B, and v is a proof of A, then
the expression (u v) is a proof of B.
Now, there is a rule for manipulation of lambda calculus expressions,
called "beta reduction". It works like this:
((lambda x:A . t) v) ==> t[with the variable x replaced by the term v]
Beta reduction on the lambda calculus expression associated with a
proof corresponds to cut elimination.
The nice thing about the Curry/Howard isomorphism is that
while a general lambda calculus term can be nonterminating
(the beta reduction steps can go on forever), any lambda
calculus term corresponding to an intuitionistic proof
always terminates. So the isomorphism is a way to develop
provably total programs.
MoeBlee
wrote:
> MoeBlee says...
> Yes. You prove by induction on e0 that repeatedly applying
> cut elimination on any proof in (intuitionistic) PA results
> in a cut-free proof.
Ah, thanks! But (and I don't mean to wear you out with my naive
questions), since proofs are finite, why would induction on e0 come
into play?
> >> Through the "proofs as programs" paradigm,
>
> >Is this the Curry-Howard isomorphism? Would you say something, in
> >rather basic, not-too-techical terms, what that is?
>
> Sure. You can associate proofs in intuitionistic logic with
> terms in the lambda calculus. The basic rules are these:
>
> 1. Variables all have types associated with them.
Do you mean 'types' in the general sense of, say, PM? So do you mean
that each variable is assigned a natural number that is that
variable's type?
> 2. Propositions (or statements) are considered types.
Then maybe this is a different sense of 'type' from what I usually
think of as types as in PM?
MoeBlee
herbzet
Daryl McCullough wrote:
> herbzet says...
>
> >And THAT'S why we pay you the big bucks.
>
> Umm. I don't know if this is the right time to bring it up, but
> speaking of big bucks, I haven't received a check from sci.logic
> in a long time. I'm sure it's in the mail, right?
Your virtual check is in the virtual mail.
(Don't spend it all in one place!)
Keep up the good work.
--
hz
Daryl McCullough
>
>On Jan 22, 2:58=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough)
>wrote:
>> MoeBlee says...
>
>> Yes. You prove by induction on e0 that repeatedly applying
>> cut elimination on any proof in (intuitionistic) PA results
>> in a cut-free proof.
>
>Ah, thanks! But (and I don't mean to wear you out with my naive
>questions), since proofs are finite, why would induction on e0 come
>into play?
Proofs may be finite, but that doesn't mean that the process of
rewriting proofs is terminating.
Here's a sketch of the argument for the consistency of intuitionistic
PA.
1. If P is a cut-free proof, then P is not
a proof of a contradiction.
2. If P and P' are proofs, and P can be rewritten to
P' by doing one step of cut-elimination, then P and P'
prove the same conclusion.
To complete the proof that there are no proofs of a contradiction,
you need the following induction principle:
3. if forall proofs P: cut-free(P) -> Phi(P)
and forall proofs P, P': (Phi(P') and (P rewrites to P')) -> Phi(P)
then (forall proofs P, Phi(P))
The instance of this schema that is needed is the case where
Phi(P) == P is not a proof of a contradiction. Then the
conclusion is:
4. For all proofs P, P is not a proof of a contradiction.
In order to establish the validity of induction principle 3,
you come up with a mapping level(P) from proofs to ordinals less than e0,
and you show that:
A. If P is cut-free, then level(P) = 0.
B. If P rewrites to P', then level(P') < level(P).
>> >> Through the "proofs as programs" paradigm,
>>
>> >Is this the Curry-Howard isomorphism? Would you say something, in
>> >rather basic, not-too-techical terms, what that is?
>>
>> Sure. You can associate proofs in intuitionistic logic with
>> terms in the lambda calculus. The basic rules are these:
>>
>> 1. Variables all have types associated with them.
>
>Do you mean 'types' in the general sense of, say, PM? So do you mean
>that each variable is assigned a natural number that is that
>variable's type?
No, I don't. You can basically think of types as sets.
In the simplest case, intuitionistic propositional
logic, then we have the following types:
1. There are infinitely many atomic types, which we can stipulate
are A_0, A_1, A_2, ...
You can think of these types as just names for unspecified sets
(possibly empty).
2. If X is a type and Y is a type, then X -> Y is a type.
This is the collection of all functions from X to Y.
3. If X is a type and Y is a type, then X x Y is a type.
This is the collection of all ordered pairs (x,y) such
that x is an element of X and y is an element of Y.
4. If X is a type and Y is a type, then X + Y is a type.
This is the collection of all ordered pairs (u,v) such
that either u=0 and v is an element of X, or u=1 and
v is an element of Y.
Then the proofs as programs paradigm associates each
type with a proposition as follows: Atomic types are
associated with corresponding propositional constants.
The function type X -> Y is associated with the proposition
"X implies Y". The product type X x Y are associated with
the proposition "X and Y". The disjoint union type X+Y
is associated with the proposition "X or Y".
So we have four sorts of objects:
1. Propositions in intuitionistic propositional logic.
2. Proofs of those propositions
3. Types
4. Elements of those types.
The proofs as programs paradigm associates each proposition
with a type, and associates each proof of a proposition with
an element of the corresponding type. So proving a proposition
corresponds to constructing an element of the corresponding
type, or vice-versa.
For example: In intuitionistic logic, we have the following
two inference rules:
1. A |- A
(By assumption; the left side of |- lists our assumptions,
and the right side lists a conclusion)
2. If A |- B, then |- A implies B
(implies introduction)
The corresponding type inference rules for lambda calculus
are these:
1. x:A |- x:A
(If x is declared to be a variable of type A, then x has type A.
We read t:A as "t has type A")
2. If x:A |- t:B, then |- (lambda x:A . t) : A -> B
(If t is an expression involving x, and whenever x has
type A, then t has type B, then lambda x:A. t is a function
mapping any element of A to an element of B).
So these two rules together show that (lambda x:A.x) : A -> A,
which can be interpreted as a proof of "A implies A"
Daryl McCullough
MoeBlee says...
>
>On Jan 22, 2:58=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough)
>wrote:
>> MoeBlee says...
>
>> Yes. You prove by induction on e0 that repeatedly applying
>> cut elimination on any proof in (intuitionistic) PA results
>> in a cut-free proof.
>
>Ah, thanks! But (and I don't mean to wear you out with my naive
>questions), since proofs are finite, why would induction on e0 come
>into play?
What we need to prove consistency is the following induction
principle:
If we can prove the following two statements:
1. forall proofs P, if P is cut-free then Phi(P),
2. forall proofs P1 and P2, if Phi(P2), and P1 rewrites to P2 (by
performing a single step of cut-elimination),
then Phi(P1).
then we can conclude:
3. forall proofs P, Phi(P)
If this principle holds, then we can prove that intuitionistic PA
is consistent by letting Phi(P) == P does not prove a contradiction.
We show that no cut-free proof can prove a contradiction, and then
show that if P1 rewrites to P2, and P2 does not prove a contradiction,
then P1 doesn't prove a contradiction (since the rewritten proof
proves the same conclusion as the original proof).
So we need to prove that the induction principle holds. This is
where e0 comes in. We construct a mapping from proofs to
(representations of) ordinals less than e0. Then we show that
if P1 rewrites to P2, then the ordinal corresponding to P2 is
strictly less than the ordinal corresponding to P1. Then the
above induction principle on proofs follows from from the
corresponding induction principle for e0.
>> >> Through the "proofs as programs" paradigm,
>>
>> >Is this the Curry-Howard isomorphism? Would you say something, in
>> >rather basic, not-too-techical terms, what that is?
>>
>> Sure. You can associate proofs in intuitionistic logic with
>> terms in the lambda calculus. The basic rules are these:
>>
>> 1. Variables all have types associated with them.
>
>Do you mean 'types' in the general sense of, say, PM? So do you mean
>that each variable is assigned a natural number that is that
>variable's type?
No. A type is basically a set of mathematical objects that are
related in that the same sorts of operations can be performed on
them. For example, naturals, booleans, reals can be considered types.
Then you can form new types from existing types by the following
sorts of operations:
1. Function space formation: If A is a type, and B is a type,
then A -> B is the type of all functions from A to B.
2. Product formation: If A and B are types, then AxB is the
type of ordered pairs (x,y) such that x is of type A, and y
is of type B.
3. Disjoint union formation: If A and B are types, then A+B is
the type of ordered pairs (x,y) such that either x=0 and y has
type A, or x=1 and y has type B.
In more sophisticated versions of constructive type theory, there
are also polymorphic types, and dependent products, etc.
Here's about the very simplest case of the proofs as programs
paradigm: intuitionistic propositional logic with "implies" as
the only connective.
The proof theory is pretty simple when written in terms of sequents.
There are three rules:
1. A |- A
(By assumption; if A is an assumption, then you can conclude A)
2. If A |- B then |- A implies B
(implies introduction)
3. If |- A, and |- A implies B, then |- B
(implies elimination)
On the type-theoretic side, we have corresponding rules for
deducing the type of an expression (read u:v as "u has type v")
1. x:A |- x:A
(If we have declared that x is a variable of type A, then we
can conclude that x has type A)
2. If x:A |- u:B then |- (lambda x:A . u) : (A -> B)
3. If |- u:(A -> B), and |- v:A, then |- (u v) : B
(If u is a function from A to B, and v is an object of
type A, then (u v) has type B; (u v) means the result
of applying function u on argument v.)
You can see by the parallelism that every type built up
out of atomic types using the -> type constructor corresponds
to a proposition built up out of atomic propositions using
"implies". You can also see that if we manage to construct
an expression u of type Phi, then there is a corresponding
proof of the proposition corresponding to Phi. The simplest
example is this: The simplest proof of the proposition
"A implies A" corresponds to the lambda calculus expression
"lambda x:A . A", which is a function of type A -> A
(the identity function).
MoeBlee
wrote:
> MoeBlee says...
> >On Jan 22, 2:58=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough)
> >wrote:
> >> MoeBlee says...
>
> >> Yes. You prove by induction on e0 that repeatedly applying
> >> cut elimination on any proof in (intuitionistic) PA results
> >> in a cut-free proof.
>
> >Ah, thanks! But (and I don't mean to wear you out with my naive
> >questions), since proofs are finite, why would induction on e0 come
> >into play?
>
> Proofs may be finite, but that doesn't mean that the process of
> rewriting proofs is terminating.
What I can understand is that there is no upper bound on rewriting.
But why would that require jumping all the way up to e0?
However, I'm confident my lack of understanding stems only from lack
of familiarity with the exact technicals and notion of 'rewriting'.
> Here's a sketch of the argument for the consistency of intuitionistic
> PA.
>
> 1. If P is a cut-free proof, then P is not
> a proof of a contradiction.
>
> 2. If P and P' are proofs, and P can be rewritten to
> P' by doing one step of cut-elimination, then P and P'
> prove the same conclusion.
>
> To complete the proof that there are no proofs of a contradiction,
> you need the following induction principle:
>
> 3. if forall proofs P: cut-free(P) -> Phi(P)
> and forall proofs P, P': (Phi(P') and (P rewrites to P')) -> Phi(P)
> then (forall proofs P, Phi(P))
>
> The instance of this schema that is needed is the case where
> Phi(P) == P is not a proof of a contradiction. Then the
> conclusion is:
>
> 4. For all proofs P, P is not a proof of a contradiction.
>
> In order to establish the validity of induction principle 3,
> you come up with a mapping level(P) from proofs to ordinals less than e0,
> and you show that:
I'm following the gist of this okay. But would you explain why the
induction needs to be on e0?
> A. If P is cut-free, then level(P) = 0.
> B. If P rewrites to P', then level(P') < level(P).
Thank you very much for that whole outline. It gives me a good general
picture that I really needed!
Wow! Thanks for that great outline! I'm getting the basic picture. I'm
going to print it out to study at more leisure. This really helps!
MoeBlee
Aatu Koskensilta
> Gentzen's result is important because it proves that Peano arithmetic
> (or whatever variant of arithmetic he was working with) is consistent:
> there is no proof of a contradiction. It's a proof-theoretic (as opposed
> to model-theoretic) proof of consistency.
Gentzen's Haupsatz, cut-elimination for first-order logic, does not
yield consistency of PA. (It is provable already in PRA.) You're
thinking of a different result, also due to Gentzen.
--
Aatu Koskensilta (aatu.kos...@uta.fi)
"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
Aatu Koskensilta
> (Though we also know they are equiconsistent, right? That can be
> proven in what - HA, PA?)
The equiconsistency of HA and PA is provable in rather weak theories,
such as PRA -- all we need to verify is that the double-negation
translations of the axioms of PA are axioms of HA.
> If we were to formalize this proof-theoretic conistency proof, then
> what would a typical formal system for it be? (Since it has to be a
> system either stronger than PA or not comparable to PA).
Gentzen's consistency proof goes through in PRA + quantifier-free
induction up to epsilon-0, where "quantifier-free induction" is jargon
for induction restricted to primitive recursive predicates.
Aatu Koskensilta
> Are we talking about the famous proof that uses induction on e0 in
> addition to PA? If so, would I be correct to take it that the
> hauptsatz is important for facilitating that proof?
There's a bit about Gentzen's consistency proof in an old post
archived at
http://groups.google.com/group/sci.logic/msg/2515fdab7d624e82
(There are some technical inaccuracies, but perhaps the post is of
some help nevertheless.)
Daryl McCullough
>
>stevend...@yahoo.com (Daryl McCullough) writes:
>
>> Gentzen's result is important because it proves that Peano arithmetic
>> (or whatever variant of arithmetic he was working with) is consistent:
>> there is no proof of a contradiction. It's a proof-theoretic (as opposed
>> to model-theoretic) proof of consistency.
>
>Gentzen's Haupsatz, cut-elimination for first-order logic, does not
>yield consistency of PA. (It is provable already in PRA.) You're
>thinking of a different result, also due to Gentzen.
Hmm. I thought that that was where epsilon-0 came in: you can prove,
by induction on epsilon-0 that no proof is a proof of a contradiction.
That isn't done by cut elimination?
I'm pretty sure that cut elimination can be used to prove the
consistency of higher-order lambda calculus, which is strong
enough to interpret the Peano axioms. So cut elimination *can*
be used to prove the consistency of PA.
In this article: http://eom.springer.de/A/a013290.htm
it is suggested that the first proof-theoretic consistency
proof of PA was done by reformulating it in terms of an
omega-rule that allowed for cut elimination:
If formal arithmetic is defined as the Gentzen formal system of the usual type,
a cut (the analogue of modus ponens in Gentzen systems) cannot be eliminated.
Elimination of a cut becomes possible if the induction scheme is replaced by the
rule of infinite induction (omega-rule):
From A(0), A(1), ...
Conclude forall x, A(x)
...To each derivation of a formula A in formal arithmetic it is possible to
assign a number e such that the statement "e is an omega-proof of the formula A
without a cut" is true, and can even be proved in formal arithmetic. Since a
cut-free -proof of a closed quantifier-free formula contains no quantifiers, it
follows that formal arithmetic is consistent.
Aatu Koskensilta
> Hmm. I thought that that was where epsilon-0 came in: you can prove,
> by induction on epsilon-0 that no proof is a proof of a contradiction.
>
> That isn't done by cut elimination?
It is done, if we wish to manipulate ordinary first-order proofs in
PA, by "sort of cut-elimination". It is perhaps more readily expressed
as cut-elimination for infinitary proofs in omega-logic corresponding
to ordinary PA proofs with appeals to induction replaced by
applications of the omega-rule.
In usual terminology "Gentzen's Hauptsatz" refers to his 1934 result
that every logically provable sequent is provable without the
cut-rule.
> I'm pretty sure that cut elimination can be used to prove the
> consistency of higher-order lambda calculus, which is strong
> enough to interpret the Peano axioms. So cut elimination *can*
> be used to prove the consistency of PA.
Sure, but cut-elimination for first-order logic is not sufficient.
MoeBlee
> stevendaryl3...@yahoo.com (Daryl McCullough) writes:
> > Hmm. I thought that that was where epsilon-0 came in: you can prove,
> > by induction on epsilon-0 that no proof is a proof of a contradiction.
>
> > That isn't done by cut elimination?
>
> It is done, if we wish to manipulate ordinary first-order proofs in
> PA, by "sort of cut-elimination". It is perhaps more readily expressed
> as cut-elimination for infinitary proofs in omega-logic corresponding
> to ordinary PA proofs with appeals to induction replaced by
> applications of the omega-rule.
>
> In usual terminology "Gentzen's Hauptsatz" refers to his 1934 result
> that every logically provable sequent is provable without the
> cut-rule.
>
> > I'm pretty sure that cut elimination can be used to prove the
> > consistency of higher-order lambda calculus, which is strong
> > enough to interpret the Peano axioms. So cut elimination *can*
> > be used to prove the consistency of PA.
>
> Sure, but cut-elimination for first-order logic is not sufficient.
Okay, but then is it still reasonable to say that much of the
importance or attention paid to the hauptsatz is its role in the e0
consistency proof of PA? Or, are there are other aspects that account
for its prominence as not just a technical result about what moves one
may or may not make in a particular deductive calculus?
MoeBlee
Aatu Koskensilta
> In this article: http://eom.springer.de/A/a013290.htm
> it is suggested that the first proof-theoretic consistency
> proof of PA was done by reformulating it in terms of an
> omega-rule that allowed for cut elimination:
That's the modern approach. It is not, however, Gentzen's original
approach.