Re: Proof of a certain theorem in “Gödel's Proof” by Nagel & Newman

G. Frege schrieb:
On page 50 in the latest edition (2001) of "Gödel's Proof" Nagel &
Newman write:

"Each of these axioms may seem "obvious" and trivial. Nevertheless, it
is possible to derive from them with the help of the stated
Transformation Rules an indefinitely large class of theorems which are
far from obvious or trivial. For example, the formula

'((p -> q) -> ((r -> s) -> t)) -> ((u -> ((r -> s) -> t)) -> ((p -> u) -> (s -> t)))'

can be derived as a theorem. We are, however, not interested for the
moment in deriving theorems from the axioms."

I always felt the desire to "fill the gap" and formulate a proof for
this theorem. Now, finally, I took the time to do so. Note though that
without adding the crucial definition

S1 -> S2 =df ~S1 v S2

the system described by Nagel & Newman in their book is simply
_incomplete_, contrary to their claims. (Actually, without that
definition not even p -> p can be derived.) For simplicity I'm using a system adopting axiom schemas rather than axioms proper, and an additional (auxiliary) definition for "&".


System: H&A
~~~~~~~~~~~

This axiom system was proposed by Hilbert and Ackermann in D. Hilbert, W. Ackermann, "Grundzüge der theoretischen Logik", Berlin: Springer-Verlag, 1928.

Axiom-Schemata:

A1 (A v A) -> A
A2 A -> (A v B)
A3 (A v B) -> (B v A)
A4 (A -> B) -> ((C v A) -> (C v B))

Definitions:

A -> B =df ~A v B
A & B =df ~(~A v ~B)


> [.. snip very akwardly long proofs of simple tautologies ..]

I am trying to get a grip why these Hilbert Style
Proofs were so akwardly long in another post, and
now are so short. Will compare them to Natural
Deduction, and then do some free style speculation.

In Hilbert Style Proofs we have the only rule MP:

A A -> B
-----------
B

This can be viewed as a lambda calculus application:

t:A s:A->B
-------------
(s t):B

That is when the term t has the type A, and the term
s has the type A->B, then the application (s t) has
the type B.

In the notation t:A, the term t carries the proof
tree, and A is the conclusion.

The axioms of a Hilbert Style proofs are now simply
combinatorial constants. A famous set of combinatorial
constants S, K and I. They have the following types:

I: A->A
K: A->(B->A)
S: (A->(B->C))->((A->B)->(A->C))

And guess what? The axioms K+S+MP give intutionistic
logic, and the axioms I+K+S+MP give classical logic
(roughly, we must also then decide what we do
with A->f respective ~A).

http://en.wikipedia.org/wiki/Combinatory_logic#Logic

It should be possible to find constants for the
system in Hilbert and Ackermann in D. Hilbert, W.
Ackermann, "Grundzüge der theoretischen Logik", 1928.
The problem is a little bit that they use disjunction,
besides implication. So we would need a bigger
aparatus.

But that is not the point I would like to draw.
I would like to discuss the proof length.

Now natural deduction has additional rules. It
enhances hilbert style proofs. The following
things are added in natural deduction:

- Premisses: The view is not that only a
tautology is proofed, but from the beginning
the view is that we proof a consequence:

A1,..,An |- B.

Thus MP from Hilbert Sytle is viewed (roughly) as:

G |- A D |- A->B
-------------------
G,D |- B

Further an Axiom Ax from Hilbert Style is viewed as:

|- Ax

- Identity: There is a new rule, which allows to
use a premisse:

B |- B

- Discharge: There is new rule, which allows to
eliminate a premisse (roughly):

G,A |- B
----------
G |- A->B

(Note: The comment (roughly) indicates that an
exact formulation needs to be more elaborate,
because multisets are used before the |-)

Now if we go again types, we see that Natural Deduction
introduces the following:

- Premisses as Types: We will extend our judgements,
we will not only have a judgement t:A, but we will
have a judgment of the form:

x1:A1,..,xn:An |- t:A

Where xi are supposed to be variables.

A judgement for MP is now (roughly):

x:G |- s:A y:D |- t:A->B
-------------------------
x:G,y:D |- (s t):B

A judgment for an axiom is now:

|- c:Ax

- Identity:

A judgment for identity is now:

x:A |- x:A

- Discharge:

A judgment for discharge is now (roughly):

x:G,y:A |- t:B
------------------------
x:G |- (lambda y t):A->B

It should be noted that when we only consider the
derivation of tautologies (i.e. judgments of the
form |- t:A), we can number the variables as they
are introduced by identity (and later necessarely
discharged).

In summary we see that from a proof as types
viewpoint natural deduction adds variables and
lambda abstraction to the proof construction. And
that gives a little gain in proof length.

Or if we go from a natural deduction proof to
a hilbert style proof we would perform lambda
elimination (compare this to cut elimination).

Here is a little example (Which is intutionistic,
so we don't need some constants) (Whitehead et al.
2.05 Syll):

1 R |- R (identity)
2 P |- P (identity)
3 Q |- Q (identity)
4 P->Q, P |- Q (discharge, apply, apply 2, 3)
5 P->Q, R->P, R |- Q (discharge, apply, apply 4, 1)
6 P->Q, R->P |- R->Q (discharge 5)
7 P->Q |- ((R -> P) -> (R -> Q)) (discharge 6)
8 |- (P -> Q) -> ((R -> P) -> (R -> Q)) (discharge 7)

The corresponding proof term has 5 lambda abstractions
and 4 applications. Converting this beast to a
SKI-term and thus a hilber style proof, would lead
to a very long proof.

But interestingly there is also a short Hilbert Style
proof for this thing:

1 ax s: (((A->B)->((C->(A->B))->((C->A)->(C->B))))->(((A->B)->(C->(A->B)))->((A->B)->((C->A)->(C->B)))))
2 ax k: (((C->(A->B))->((C->A)->(C->B)))->((A->B)->((C->(A->B))->((C->A)->(C->B)))))
3 ax s: ((C->(A->B))->((C->A)->(C->B)))
4 mp 2, 3: ((A->B)->((C->(A->B))->((C->A)->(C->B))))
5 mp 1, 4: (((A->B)->(C->(A->B)))->((A->B)->((C->A)->(C->B))))
6 ax k: ((A->B)->(C->(A->B)))
7 mp 5, 6: ((A->B)->((C->A)->(C->B)))

This proof makes heavy use of instantiating the
axioms, which our natural deduction style proof
didn't make.

Also the above proofs are longer than the proof
by "G. Frege", the initial poster of this thread.
His proof is:

Theorem 2:

(P -> Q) -> ((R -> P) -> (R -> Q))

(1) (P -> Q) -> ((~R v P) -> (~R v Q)) Ax. 4
(2) (P -> Q) -> ((R -> P) -> (~R v Q)) Df. -> 1
(3) (P -> Q) -> ((R -> P) -> (R -> Q)) Df. -> 2

He doesn't make heavy instantiation of an axiom,
but rather does apply the rewriting of ~A v B
to A->B heavily.

My only objection is here:
- Can a rewriting be counted as one proof
step, aren't these in fact more elaborate
derivations.

Normal proof steps always work in the root
of the premisses and conclusions. They are
simple pattern matching.

But if you apply a definition, you have
to travers the premisse and then rebuild
the conclusion. This isn't a simple pattern
matching step.

Bye


.

Relevant Pages

  • Re: Minimal logic valid?
    ... rules and no axioms. ... while the axiomatic method uses axiomsand only detachment / ... Natural deduction has it. ... Hilbert style calculi dont have this context. ...
    (sci.logic)
  • Re: Prove axiom in S5
    ... >Does anybody know how to prove the following using Natural Deduction ... follows from two of the axioms, I mentioned, and not all three? ... > Posted Via Usenet.com Premium Usenet Newsgroup Services ...
    (sci.logic)
  • Re: Logarithm of transfinite numbers
    ... An axiomless system of natural deduction does not have ... True, because without axioms, you cannot generate a theorem. ... axiomatized with all true statements trivially being true... ...
    (sci.math)