Re: A missing definition in "Gödel's Proof" by Nagel & Newman (open letter)
- From: Newberry <newberryxy@xxxxxxxxx>
- Date: Sun, 04 Nov 2007 18:55:48 -0800
On Oct 30, 4:18 pm, G. Frege <nomail@invalid> wrote:
Dear Prof. Hofstadter!
I'm just reading "Gödel's Proof" by Nagel & Newman. Since you seem to be
the present editor of this book, I thought you might be interested in
the following exchange (taking place in the Usenet group sci.logic in
2005). See below.
Comment: Actually, I realized that this crucial definition was missing
in the book some time before the question came up in sci.logic.
Without this definition the exposition of the system (described in the
book) is simply incomplete (for example, without it not even p -> p
can be derived); and hence imho it should be added to the text.
Sincerely,
F. XXXXXX
Question/Problem:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Hi
With great interest I'm reading my way through the book by Nagel and
Newman on "Gödel's Proof". On page 50 in my edition (2001) it is stated
that p -> (~p -> q) is a theorem with a parenthetical remark: "(We shall
accept this as a fact, without exhibiting the derivation.)"
To support my understanding of the subject I've been trying to derive
the statement on my own - in vain.
Very frustrating - can anybody help or give a hint.
Regards
Peter, Denmark
Answer:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Actually, they forgot to mention an important information concerning the
considered axiom system. There
A -> B
is defined with
~A v B.
Below you will find a derivation of the theorem in question.
Axioms:
Ax. 1 (p v p) -> p
Ax. 2 p -> (p v q)
Ax. 3 (p v q) -> (q v p)
Ax. 4 (p -> q) -> ((r v p) -> (r v q))
Definition:
S1 -> S2 =df ~S1 v S2
Rules of derivation:
- Substitution
- From S1 and S1 -> S2 derive S2. (MP)
In addition (to simplify the derivations) the definition may be applied
and theorems may be introduced in any line of the derivation.
Theorem 1:
(p -> q) -> ((r -> p) -> (r -> q)) (HS)
(1) (p -> q) -> ((r v p) -> (r v q)) Ax. 4
(2) (p -> q) -> ((~r v p) -> (~r v q)) Subst. 1 [r/~r]
(3) (p -> q) -> ((r -> p) -> (~r v q)) Df. 2
(4) (p -> q) -> ((r -> p) -> (r -> q)) Df. 3
Theorem 2:
p -> p (Id)
(1) (p -> q) -> ((r -> p) -> (r -> q)) Th. 1
(2) ((p v p) -> q) -> ((r -> (p v p)) -> (r -> q)) Subst. 1 [p/(p v p)]
(3) ((p v p) -> p) -> ((r -> (p v p)) -> (r -> p)) Subst. 2 [q/p]
(4) ((p v p) -> p) -> ((p -> (p v p)) -> (p -> p)) Subst. 3 [r/p]
(5) (p v p) -> p Ax. 1
(6) (p -> (p v p)) -> (p -> p) MP 4,5
(7) p -> (p v q) Ax. 2
(8) p -> (p v p) Subst. 7 [q/p]
(9) p -> p MP 6,8
Theorem 3:
p v ~p (TND)
(1) p -> p Th. 2
(2) ~p v p Df. 1
(3) (p v q) -> (q v p) Ax. 3
(4) (~p v q) -> (q v ~p) Subst. 3 [p/~p]
(5) (~p v p) -> (p v ~p) Subst. 4 [q/p]
(6) p v ~p MP 5,2
Theorem 4:
p -> ~~p (DN)
(1) p v ~p Th. 3
(2) ~p v ~~p Subst. 1 [p/~p]
(3) p -> ~~p Df. 2
Theorem 5:
p -> (~p -> q) (ECQ)
(1) p -> ~~p Th. 4
(2) p -> (p v q) Ax. 2
(3) ~~p -> (~~p v q) Subst. 2 [p/~~p]
(4) ~~p -> (~p -> q) Df. 3
(5) (p -> q) -> ((r -> p) -> (r -> q)) Th. 1
(6) (~~p -> q) -> ((r -> ~~p) -> (r -> q)) Subst 5 [p/~~p]
(7) (~~p -> (~p -> q)) -> ((r -> ~~p) -> (r -> (~p -> q))) Subst 6 [q/(~p -> q)]
(8) (~~p -> (~p -> q)) -> ((p -> ~~p) -> (p -> (~p -> q))) Subst 7 [r/p]
(9) (p -> ~~p) -> (p -> (~p -> q)) MP 8,4
(10) p -> (~p -> q) MP 9,1
qed.
Historical note: This axiom system was proposed by Hilbert & Ackermann
in D. Hilbert, W. Ackermann, "Grundzüge der theoretischen Logik",
Berlin: Springer-Verlag, 1928. It's a simplified variant of Russell and
Whitehead's axiom system for propositional logic in /Principia/.
~~~~~~~~~~~~~~
Finally we may put all those proofs together.
Theorem:
p -> (~p -> q)
Proof:
(1) (p -> q) -> ((r v p) -> (r v q)) Ax. 4
(2) (p -> q) -> ((~r v p) -> (~r v q)) Subst. 1 [r/~r]
(3) (p -> q) -> ((r -> p) -> (~r v q)) Df. 2
(4) (p -> q) -> ((r -> p) -> (r -> q)) Df. 3
(5) ((p v p) -> q) -> ((r -> (p v p)) -> (r -> q)) Subst. 4 [p/(p v p)]
(6) ((p v p) -> p) -> ((r -> (p v p)) -> (r -> p)) Subst. 5 [q/p]
(7) ((p v p) -> p) -> ((p -> (p v p)) -> (p -> p)) Subst. 6 [r/p]
(8) (p v p) -> p Ax. 1
(9) (p -> (p v p)) -> (p -> p) MP 7,8
(10) p -> (p v q) Ax. 2
(11) p -> (p v p) Subst. 10 [q/p]
(12) p -> p MP 9,11
(13) ~p v p Df. 12
(14) (p v q) -> (q v p) Ax. 3
(15) (~p v q) -> (q v ~p) Subst. 14 [p/~p]
(16) (~p v p) -> (p v ~p) Subst. 15 [q/p]
(17) p v ~p MP 16,13
(18) ~p v ~~p Subst. 17 [p/~p]
(19) p -> ~~p Df. 18
(20) p -> (p v q) Ax. 2
(21) ~~p -> (~~p v q) Subst. 20 [p/~~p]
(22) ~~p -> (~p -> q) Df. 21
(23) (~~p -> q) -> ((r -> ~~p) -> (r -> q)) Subst. 4 [p/~~p]
(24) (~~p -> (~p -> q)) -> ((r -> ~~p) -> (r -> (~p -> q))) Subst. 23 [q/(~p -> q)]
(25) (~~p -> (~p -> q)) -> ((p -> ~~p) -> (p -> (~p -> q))) Subst. 24 [r/p]
(26) (p -> ~~p) -> (p -> (~p -> q)) MP 25,22
(27) p -> (~p -> q) MP 26,19
This may be a bit off topic but it is on Nagel/Newman. Here is what
the say:
QUOTE:
It follows. also, that that what we understand by the process of mathematical proof does not coincide with the exploitation of a formalized axiomatic method.
....
But, even so, the brain appers to embody a structure of rules of
operation which is far more powerful than the structure of currently
conceived artificial machines. <<
END OF QUOTE, p.99-100
Is all this nonsense?
.
- Follow-Ups:
- Prev by Date: Re: A missing definition in "Gödel's Proof" by Nagel & Newman (open letter)
- Next by Date: Re: Non standard models of PA
- Previous by thread: Re: A missing definition in “Gödel's Proof” by Nagel & Newman (open letter)
- Next by thread: Re: A missing definition in "Gödel's Proof" by Nagel & Newman (open letter)
- Index(es):
Relevant Pages
|
