Proof theoretical consistency proofs (Was: Re: Existential, Universal Quantifiers, Generalize Booleans)
Aatu Koskensilta
> Chip Eastham wrote:
>> Here's a concise account of the technique in
>> connection with a reworking by Goedel of Gentzen's
>> proof of the consistency of Peano arithmetic via cut
>> elimination (by W. W. Tait):
>>
>> [Goedel's Reformulation of Gentzen's 1st Consis. Proof]
>> http://home.uchicago.edu/~wwtx/GoedelandNCInew1.pdf
>
> Looking at that paper I'm totally confused at the
> start. They're talking about a proof of the consistency
> of PA. But there are countable ordinals running around
> the whole paper. I don't get this at all - if someone
> believes in the reality of the set omega doesn't that
> show that PA is consistent by exhibiting a model?
The short answer: omega is not sufficient, one needs to know facts about
omega, such as induction holding for all arithmetical properties. In
Gentzen's consistency proof *that* is not assumed - it would be, as you
note, quite pointless - but rather a very restricted form of induction
is accepted for a primitive recursive ordering of naturals which happens
to have the order type epsilon-0 (in addition to primitive recursive
arithmetic, i.e. basically just the most obvious finitistic operations
and facts about naturals). The point is that this principle, unlike the
unrestricted induction schema, is finitistically meaningful.
And then to the long answer which hopefully makes sense of the short
answer. Let's start from the beginning, with natural deduction
formulation - or sequent calculus, it doesn't really make any
difference. Gentzen's Haupsatz - literally "main theorem"; the German
name is used to impress non-logicians, or out of the force of habit -
says that if a sentence A is logically provable it is provable without
using the cut rule. What this means exactly is not important, but from
the Haupsatz we get another important property of natural deduction, the
subformula property: if a sentence A is provable, it is provable with a
proof containing only subformulae of A. In a cut-free proof of A, B&C is
always derived from B and C, A\/B from A or B and so forth, with no
complexity decreasing detours. From this we get a rather silly
consistency proof for natural deduction: take a contradiction of least
possible complexity. If it were provable, there would be a cut-free
proof of it, in which the contradiction would be derived from its
subformulae. But those can be taken to be atomic, and they aren't
axioms. Hence there is no proof of a contradiction. Of course, this is a
very perverse way to prove consistency of natural deduction, which is
obvious in any case. However, in proof theory such silly proofs can be
made to do useful work. For example, formalizing the Haupsatz, and
basically imitating the silly consistency proof, one can show that PA
proves that if a sentence A is logically provable in the natural
deduction calculus then A is true, which can be used to prove that PA
proves the consistency of every of its finitely axiomatizable
subtheories and hence is not finitely axiomatizable itself.
Now, if we could prove Haupsatz not only for logical provability, but
also for provability from the axioms of PA, we could establish the
consistency of PA using just the sort of silly proof we outlined above
for the consistency of natural deduction. Alas, cuts can't, in general,
be eliminated in presence of non-logical axioms. So we'll just cheat and
define a logic, which we will call omega-logic, in which the axioms of
arithmetic are logical axioms or rules of inference! Here's where
infinite trees and ordinals come into play. A proof will be a possibly
infinite well-founded tree labeled with formulae. As axioms we can take
the usual identity axioms and all true formulas of the form "t_1 = t_2"
where t_1 and t_2 are closed terms in the language of arithmetic. As
rules of inference, which tell us how a proof tree must be constructed,
we can take the usual natural deduction rules such as
A B A B
--------- ------ ------ ....
A&B A\/B A\/B
in addition we have the omega-rule, which makes the logic infinitary:
P(0) P(1) P(2) ... P(n) ... for all n in N
------------------------------------------
AxP(x)
We can again define what it means for a proof to be cut-free, which
amounts to just the cut rule not being used in the proof, and again
cut-free proofs will contain just subformulae of the conclusion. Such a
proof will be a possibly infinite tree with basic identities at leaves,
more complex formulae being derived from these step by step using the
usual rules of inference, excluding the cut rule, and the omega-rule. It
is obvious that such a proof can't prove a contradiction, which we can
take to be "0=1" in this context: 0=1 has no subformulae, and is not an
axiom, hence it can't be provable using a cut-free proof. It is also
obvious that every true arithmetical sentence is omega-provable,
although that's utterly irrelevant here.
Now, we can easily transform any usual proof in PA into an omega-proof,
just replacing appeals to the induction axiom by applications of the
omega-rule. The result will be a labeled tree of height at most
something like omega^omega. Now, it turns out that cuts can be
eliminated in omega-proofs. This gives us a consistency proof of PA:
every PA proof can be transformed into an omega-proof, which in turn can
be transformed into a cut-free omega-proof, and those can't prove a
contradiction. Thus far relatively clear - I hope! - but the obvious
question is: what's the point? Well-founded trees etc. are all seemingly
set theoretical things, way beyond PA already, so why not just stick
with the trivial and easy consistency proof for PA (the axioms are true;
the rules of inference preserve truth; no contradiction is true; hence
PA is consistent)? The answer is that we can actually make the above
finitistic modulo a certain possibly finitistically unacceptable but
still finitistically meaningful principle.
First, we note that a countable tree can be represented as a set of
finite sequences of naturals. The root will be the empty sequence <>,
it's children will be <0>, <1>, <2>, ... the children of <0> will be
<0,0>, <0,1>, <0,2> ... the children of <1> will be <1,0>, <1,1>, <1,2>,
... and so forth. As usual, we can code finite sequences of naturals as
naturals using e.g. Gödel's beta-function or primes and exponentiation.
We can't, in the language of arithmetic, talk about arbitrary sets of
such finite sequences, but we *can* talk about primitive recursive sets
of finite sequences (and recursively enumerable, and in general of Pi_n
and Sigma_n sets for any fixed n). Thus we can talk about an omega-proof
provided it is primitive recursive (or arithmetically definable, which
actually does not make any difference since an arithmetical well-founded
tree is always primitive recursive). The omega-proofs obtained from PA
proofs are certainly always primitive recursive as the transformation is
utterly trivial. And cut-elimination for omega-logic is actually
*effective*: there is a primitive recursive algorithm which when given
an omega-proof (or, actually, a code of an omega proof) produces an
omega-proof with less cuts, of greater height (the upper bound on the
height of such a "reduced" proof being, surprise, epsilon-0). Now, we
come to countable ordinals: we can assign an ordinal < epsilon-0 to an
omega-proof obtained from a PA proof, measuring the "indirectness" of
the proof, so that every cut increases the ordinal, and at applications
of the omega-rule we take the supremum of the ordinals assigned to the
proofs of the premises. Now, even countable ordinals are infinitary and
set theoretical. However, we can just pick a suitable natural primitive
recursive ordering < with order type epsilon-0, obtained e.g. from terms
in Cantor normal form such that basic operations on ordinals < epsilon-0
correspond to p.r. operations on the codes (naturals) of those ordinals.
So we assign naturals to codes of certain p.r. omega-proofs,
corresponding to the infinitary assignment of ordinals. Next we can show
that the procedure removing cuts from omega-proofs decreases the the
corresponding natural ("ordinal") according to <. If there is a proof of
contradiction in PA, applying repeatedly the cut-removing procedure to
the corresponding omega-proof can't terminate with a cut-free proof,
since those can't prove a contradiction. Thus there must be a *primitive
recursive* infinite <-descending sequence of naturals. But this is
exactly what is prohibited by the principle of "quantifier free
transfinite induction for <" or "quantifier free transfinite induction
up to epsilon-0". ("Quantifier free" because primitive recursive
properties are expressed in the language of PRA with formulas with no
quantifiers).
Now, in the above we used just very basic finitistic principles and
primitive recursive properties and relations, together with the scheme
"A does not define an infinite <-descending sequence" where A is p.r.
and < is a particular primitive recursive ordering of naturals.
Everything is finitistically meaningful, the only question being the
acceptability of transfinite induction for <. However, < is described in
a very concrete fashion - e.g. using Cantor normal form - so one can
almost literally "see" that the cut-elimination procedure must
terminate, even if this is not really "finitistically acceptable". Thus,
unlike in case of the trivial consistency proof for PA, this proof
actually seems to have some epistemological significance... (Originally
Gentzen didn't say anything about ordinals or infinite trees, but
instead defined an ordering on ordinary proofs, and the above
formulation is essentially due to Schütte.)
Since Gentzen proof theorists have extended these methods to cover
stronger and stronger theories, most notably subsystems of second order
arithmetic (or "analysis" as it is also known). However, the
well-orderings and notation systems, as well as other techniques,
quickly become so byzantine that no one can seriously maintain that the
consistency proofs thus obtained have any epistemological significance.
Largely due to Kreisel's influence the emphasis on proving consistency
was replaced with other goals, most notably making explicit the
"constructive content" of wildly non-constructive systems. Gentzen
proved that no well-ordering of type epsilon-0 can be shown to be
well-ordering in PA (due to the second incompleteness theorem), and that
for every ordinal alpha < epsilon-0 there is an ordering of order type
alpha that can be shown to be well-ordering in PA. In modern parlance we
say that epsilon-0 is the proof theoretical ordinal of PA. If we
consider just finitistically meaningful sentences, then PA goes beyond
finitistically acceptable principles *exactly* by transfinite induction
up to epsilon-0, so Gentzen's consistency proof actually tells us how
and to what extent PA is non-finitistic, so to speak locates or isolates
the non-finitistic portion of PA. Determining the proof theoretical
ordinal of a theory is known as ordinal analysis in proof theory and
it's one of its main areas of activity. Here we run into certain
conceptual and technical problems: it is usually possible to come up
with some silly and perverse well-ordering or ordinal notation
transfinite induction for which proves the consistency of the theory
under consideration. But such unnatural orderings or notations tell us
nothing; what we want are "natural" ordinal notation systems, whatever
that means exactly. But I digress already.
Hope this rambling explanation gives you at least some vague idea what's
going on in the proof theoretical consistency proofs. As always, the
above is modulo errors and glosses over many details. Anyhow, I don't
think these proof theoretical results have anything much to do with the
nominal subject of this thread, and as goes without saying, which of
course means I'm going to say it, your comments to Hatto are quite correct.
PS. Follow-ups set to sci.logic.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
David C. Ullrich
Yes, relatively. More than before, anyway.
>but the obvious
>question is: what's the point? Well-founded trees etc. are all seemingly
>set theoretical things, way beyond PA already, so why not just stick
>with the trivial and easy consistency proof for PA (the axioms are true;
>the rules of inference preserve truth; no contradiction is true; hence
>PA is consistent)?
Heh, yes, I was wondering about that.
Alas he'll probably miss that part, buried way down here.
>PS. Follow-ups set to sci.logic.
Oh?
************************
David C. Ullrich
Herman Jurjus
> David C. Ullrich wrote:
> (...) your comments to Hatto are quite correct.
Correct, yes, but imo also irrelevant and unnecessarily pedantic in the
context of Hatto's initial remarks.
Given the amount of nonsense that Hatto has produced recently, the
dismissive reaction to this particular point is way out of proportion,
don't you agree?
--
Cheers,
Herman Jurjus
Aatu Koskensilta
> Aatu Koskensilta wrote:
>> David C. Ullrich wrote:
> [snip]
>
>> (...) your comments to Hatto are quite correct.
>
> Correct, yes, but imo also irrelevant and unnecessarily pedantic in the
> context of Hatto's initial remarks.
Quite possibly. It's also possible that Hatto might actually learn
something.
> Given the amount of nonsense that Hatto has produced recently, the
> dismissive reaction to this particular point is way out of proportion,
> don't you agree?
Sure, but that's only to be expected. Arguing endlessly about relatively
unimportant issues is a venerable USENET tradition.