A missing definition in “Gödel's Proof” by Nagel & Newman (open letter)
G. Frege
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
G. Frege
>
> 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.
>
Actually, a footnote by the Ed. would do.
F.
translogi
Send an private email to Douglas Hofstadter
Hope he will respond
G. Frege
wrote:
>>
>> 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.
>>
>> Actually, a footnote by the Ed. would do.
>>
> Send an private email to Douglas Hofstadter
> Hope he will respond
>
Thanx for your support. Actually, I already got a slap in the face by
Hofstadter. His reply to my email was as follows:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Hello, and thanks for your note. I appreciate
your interest in "Gödel's Proof" and your
thoughts. There are always things that one
person or other would like to see "fixed", but at
this point the text is "fixed" (in another sense
of the word) and unlikely to be changed. But
thanks for the suggestion. -- Douglas Hofstadter.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Thus I decided "to go public". My point (which Hofstadter kindly decided
to ignore) is that several distinguished claims by Nagel & Newman (made
in their book) are _false_ without explicitly stating the missing
definition _as part of the system described_.
This is especially unfortunate because they spend a whole chapter
(chapter V) to _rigorously prove_ that the system in question is
/consistent/. This proof relies on the (alleged) "theorem" 'p ->
(~p -> q)'. But this "theorem" is _not_ derivable in the system as
described in the book.*)
Actually, they write/claim:
"Now, it happens that 'p -> (~p -> q)' (in words_ 'if p, then if not-p,
then q') is a theorem in the calculus. (We shall accept this as a fact,
without exhibiting the derivation.)"
Well, actually, it's NOT a fact, since 'p -> (~p -> q)' cannot be
derived in the system /as described/.
If THIS is not something that SHOULD be "fixed" (at least by mentioning
the missing definition in a footnote) what then?!
F.
______________________
*) In chapter V Hilbert & Ackermannn's variant of Russell & Whitehead's
system for propositional logic (in PM) is introduced. Even the formation
rules for wffs are given. The ONLY thing that is missing is the
_crucial_ information that 'A -> B' means '~A v B' (where A, B are
wffs).
--
E-mail: info<at>simple-line<dot>de
David C. Ullrich
>On Wed, 31 Oct 2007 15:55:11 -0000, translogi <wile...@googlemail.com>
>wrote:
>
>>>
>>> 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.
>>>
>>> Actually, a footnote by the Ed. would do.
>>>
>> Send an private email to Douglas Hofstadter
>> Hope he will respond
>>
>Thanx for your support. Actually, I already got a slap in the face by
>Hofstadter. His reply to my email was as follows:
>
>~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
>Hello, and thanks for your note. I appreciate
>your interest in "Gödel's Proof" and your
>thoughts. There are always things that one
>person or other would like to see "fixed", but at
>this point the text is "fixed" (in another sense
>of the word) and unlikely to be changed. But
>thanks for the suggestion. -- Douglas Hofstadter.
You should really get a grip - that's not a slap
in the face, it's a perfectly polite reply. He
even thanks you.
Anyway: Can you tell us exactly what the axioms
and rules of the system in the book are?
************************
David C. Ullrich
Peter_Smith
1. There are always, ALWAYS, typos/thinkos
2. Publishers don't want to keep reprinting revised versions (because
there are always more little glitches to be found: you've just got to
call a stop).
If it really is the case that
> > The ONLY thing that is missing is the
> >_crucial_ information that 'A -> B' means '~A v B' (where A, B are
> >wffs).
which is something known to any first-year student, i.e. anyone who is
likely to be tackling Nagel&Newman, then I put that down to a trivial
oversight, and not fuss!
ken.q...@excite.com
Is a truth-table for that statement that shows it to be true in all
combinations of T and F for p and q considered to be a valid
proof of its truth?
translogi
wrote:
>
> - Show quoted text -
>>>
Is a truth-table for that statement that shows it to be true in all
combinations of T and F for p and q considered to be a valid
proof of its truth?
<<<
NO Sorry i need to use capitals here.
Something is a proof if there is a derrivation of the theorem from
the axioms and inference rules.
A proof is very strict thing.
Truth tables do not prove anything.
But you can say (if you really like them) they show it
And if you are very philosophical you can follow Wittgenstein
"Every tautology itself shows that it is a tautology" 6,127
and
"What can be shown, cannot be said." 4.1212
So you can be lucky if your lecturer is philosophy minded, but i would
not do it.
ken.q...@excite.com
OK, got it. Thanks. And for the Tract. quotes.
Peter_Smith
>> Is a truth-table for that statement that shows it to be true in all
>> combinations of T and F for p and q considered to be a valid
>> proof of its truth?
>
> NO Sorry i need to use capitals here.
> Something is a proof if there is a derrivation of the theorem from
> the axioms and inference rules.
> A proof is very strict thing.
>
> Truth tables do not prove anything.
Really????? Surely a truth-table demonstration that a wff is a
tautology is a perfectly good proof that it is true (and indeed is
necessarily so). To be sure, you have to interpret the array of
symbols in the table as having a certain significance: but then you
have to interpret the array of symbols of any proof as having a
certain significance if it is to be a proof.
Jack Campin - bogus address
>>> all combinations of T and F for p and q considered to be a valid
>>> proof of its truth?
>> NO Sorry i need to use capitals here.
>> Something is a proof if there is a derrivation of the theorem from
>> the axioms and inference rules.
>> A proof is very strict thing.
>> Truth tables do not prove anything.
> Really????? Surely a truth-table demonstration that a wff is a
> tautology is a perfectly good proof that it is true (and indeed is
> necessarily so).
If you have already proved that your axiomatization is complete for
two-valued logic. That wasn't the case here, was it?
If I remember right the system presented in one of Copi's elementary
books was proved after the event to characterize a 52-valued system.
============== j-c ====== @ ====== purr . demon . co . uk ==============
Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
<http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
Peter_Smith
> Is a truth-table for that statement that shows it to be true in
> all combinations of T and F for p and q considered to be a valid
> proof of its truth?
If that means "a valid proof in deductive system S", the answer for
most systems S is, of course, trivially "no", since a proof-in-system-
S is typically defined otherwise (in terms of e.g. a sequence of axiom-
instances, or applications of rules of inference to previous items in
the sequence). That's trivial.
What I was commenting on was the unqualified claim that
>> Truth tables do not prove anything.
That is plainly over-stating the case. For of course, giving a truth-
table can prove that a wff is a tautology, and hence true. [If I set
students an exercise "prove ¬¬(P v ¬¬¬P) is a tautology" and they do a
correct truth-table, they get full marks! :-) ]
G. Frege
<ull...@math.okstate.edu> wrote:
>
> Can you tell us exactly what the axioms and rules
> of the system in the book are?
>
Sure.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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))
Rules of derivation:
- Substitution
- From S1 and S1 -> S2 derive S2. (MP)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
My point is that several distinguished claims by Nagel & Newman (made
in their book) are _false_ without explicitly stating the missing
definition _as part of the system described_.
This is especially unfortunate because they spend a whole chapter
(chapter V) to _rigorously prove_ that the system in question is
/consistent/. This proof relies on the (alleged) "theorem" 'p ->
(~p -> q)'. But this "theorem" is _not_ derivable in the system as
described in the book.*)
Actually, they write/claim (p. 50):
"Now, it happens that 'p -> (~p -> q)' (in words_ 'if p, then if
not-p, then q') is a theorem in the calculus. (We shall accept
this as a fact, without exhibiting the derivation.)"
Well, actually, it's NOT a fact, since 'p -> (~p -> q)' cannot be
derived in the system /as described/.
Hence imho the missing definition SHOULD be added to the text (or at
least mentioned in a foodnote).
F.
____________________
*) In chapter V Hilbert & Ackermannn's variant of Russell & Whitehead's
system for propositional logic (in PM) is introduced. Even the formation
rules for wffs are given. The ONLY thing that is missing is the
_crucial_ definition: A -> B is short for ~A v B.
G. Frege
>
> If it really is the case that
>
> The ONLY thing that is missing is the _crucial_ definition:
> A -> B is short for ~A v B (where A, B are wffs).
>
> which is something known to any first-year student, i.e. anyone who is
> likely to be tackling Nagel & Newman, then I put that down to a trivial
> oversight [...].
>
Sure. Actually, that even may be the explanation for this oversight.
It's just a simple fact anyone knows who has ever dealt with Russell and
Whitehead's system. Still the definition _is_ missing. And it shows, as
can be seen by the following post in sci.logic (2005):
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See?
Sincerely,
F.
G. Frege
>
> Is a truth-table for that statement that shows it to be true
> in all combinations of T and F for p and q considered to be
> a valid proof of its truth?
>
It's a valid (meta-)proof that the statement is question is a
_tautology_.
You might check the thread
"Proof of a certain theorem in “Gödel's Proof” by Nagel & Newman"
in this group.
F.
G. Frege
wrote:
>>
>> Is a truth-table for that statement that shows it to be true in all
>> combinations of T and F for p and q considered to be a valid
>> proof of its truth?
>>
> NO. Sorry I need to use capitals here.
>
> Something is a proof if there is a derivation of the theorem from
> the axioms and inference rules. A proof is very strict thing.
>
Right.
"As part of his predicate calculus, Frege developed a strict definition
of a 'proof'. In essence, he defined a proof to be any finite sequence
of well-formed statements such that each statement in the sequence
either is an axiom or follows from previous members by a valid rule of
inference. A proof of the statement B from the premises A1,...,An is any
finite sequence of statements (with B the final statement in the
sequence) such that each member of the sequence: (a) is one of the
premises A1,...,An, or (b) is an axiom, or (c) follows from previous
members of the sequence by a rule of inference. This is essentially the
definition of a proof that logicians still use today." (Ed Zalta)
Though the problem is that many authors refer to meta-proofs as "proofs"
too...
In the present context (this thread) it might help to avoid confusion if
we call the proofs you have in mind here: /formal proofs/.
>
> Truth tables do not prove anything.
>
Right. If "proof" refers to a formal proof here. But of course a truth
table (meta-)proves/shows that the formula in question is a _tautology_.
>
> But you can say (if you really like them) they show it
>
> And if you are very philosophical you can follow Wittgenstein
> "Every tautology itself shows that it is a tautology." 6,127
>
Right.
6.1 The propositions of logic are tautologies.
6.113
It is the characteristic mark of logical propositions that
one can perceive in the symbol alone that they are true
[i.e. "logically true" --G.F.]
6.126
Whether a proposition belongs to logic can be calculated by
calculating the logical properties of the _symbol_.
And this we do when we prove a logical proposition. For without
troubling ourselves about a sense and a meaning, we form the
logical propositions out of others by mere _symbolic rules_.
We prove a logical proposition by creating it out of other logical
propositions by applying in succession certain operations, which
again generate tautologies out of the first. [...]
Naturally this way of showing that its propositions are tautologies
is quite unessential to logic. Because the propositions, from which
the proof starts, must show without proof that they are tautologies.
6.1262
Proof in logic is only a mechanical expedient to facilitate
the recognition of tautology, where it is complicated.
6.127 [...]
Every tautology itself shows that it is a tautology.
F.
P.S.
Of course, W's claims are only true for /propositional logic/.
G. Frege
>>
>> Something is a proof if there is a derivation of the theorem from
>> the axioms and inference rules. A proof is very strict thing.
>>
Right.
"As part of his predicate calculus, Frege developed a strict definition
of a 'proof'. In essence, he defined a proof to be any finite sequence
of well-formed statements such that each statement in the sequence
either is an axiom or follows from previous members by a valid rule of
inference. A proof of the statement B from the premises A1,...,An is any
finite sequence of statements (with B the final statement in the
sequence) such that each member of the sequence: (a) is one of the
premises A1,...,An, or (b) is an axiom, or (c) follows from previous
members of the sequence by a rule of inference. This is essentially the
definition of a proof that logicians still use today." (Ed Zalta)
>>
>> Truth tables do not prove anything.
>>
> Really?
>
Sure, if "proves" refers to a formal proof here. But of course a truth
table proves/shows that the formula in question is a _tautology_.
>
> Surely a truth-table demonstration that a wff is a tautology is a
> perfectly good proof that it is [logically] true [...].
>
Of course.
F.
G. Frege
<bo...@purr.demon.co.uk> wrote:
>>
>> Surely a truth-table demonstration that a wff is a tautology
>> is a perfectly good proof that it is [logically] true [...].
>>
> If you have already proved that your axiomatization is complete for
> two-valued logic.
>
No.
>
> That wasn't the case here, was it?
>
Right.
F.
G. Frege
>
> What I was commenting on was the unqualified claim that
>
> "Truth tables do not prove anything."
>
> That is plainly over-stating the case.
>
Yes. But I guess translogi had "formal proof" in mind here. ;-)
>
> For of course, giving a truth-table can prove that a wff is a
> tautology, and hence [logically] true. [If I set students an
> exercise "prove 洵(P v 洵星) is a tautology" and they do a
> correct truth-table, they get full marks! :-) ]
>
Of course. :-)
F.
G. Frege
> 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
>
Actually, they forgot to mention an important information concerning the
considered axiom system. There
A -> B
is _defined_ with
~A v B.
Axioms:
Definition:
Rules of derivation:
Theorem 1:
Theorem 2:
p -> p (Id)
Theorem 3:
p v ~p (TND)
Theorem 4:
p -> ~~p (DN)
Theorem 5:
qed.
~~~~~~~~~~~~~~
Theorem:
p -> (~p -> q)
Proof:
(27) p -> (~p -> q) MP 26,19
G. Frege
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
> 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))
>
> Rules of derivation:
>
> - Substitution
> - From S1 and S1 -> S2 derive S2. (MP)
>
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
> My point is that several relevant claims by Nagel & Newman (made
> in their book) are _false_ without explicitly stating the missing
> definition _as part of the system described_.
>
> This is especially unfortunate because they spend a whole chapter
> (chapter V) to _rigorously prove_ that the system in question is
> /consistent/. This proof relies on the (alleged) "theorem" 'p ->
> (~p -> q)'. But this "theorem" is _not_ derivable in the system as
> described in the book.*)
>
> Actually, they write/claim (p. 50):
>
> "Now, it happens that 'p -> (~p -> q)' (in words_ 'if p, then if
> not-p, then q') is a theorem in the calculus. (We shall accept
> this as a fact, without exhibiting the derivation.)"
>
Though '~p -> (p -> q)' would do as well; and the derivation of the
latter is extremely simple (in the system described in the book
augmented with the definition: S1 -> S2 =df ~S1 v S2, where S1 and S2
are wffs).
Theorem:
~p -> (p -> q)
Proof:
(1) p -> ( p v q) Ax. 1
(2) ~p -> (~p v q) Subst. 1 [p/~p]
(3) ~p -> (p -> q) Df. 2
F.
David C. Ullrich
>On Thu, 01 Nov 2007 06:42:09 -0600, David C. Ullrich
><ull...@math.okstate.edu> wrote:
>
>>
>> Can you tell us exactly what the axioms and rules
>> of the system in the book are?
>>
>Sure.
>
>~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>
>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))
>
>Rules of derivation:
>
> - Substitution
> - From S1 and S1 -> S2 derive S2. (MP)
>
>~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Now I'm puzzled. Do they explicitly state what the
primitives are?
From your description of the system it _looks_ like
the primitives are v and ->. If so then it makes
no sense to say that the definition of p->q
is missing - _if_ in fact -> is a primitive then
we need a definition of ~. I don't suppose there's
a definition of ~ in terms of v and -> given?
What _are_ the primitives?
>My point is that several distinguished claims by Nagel & Newman (made
>in their book) are _false_ without explicitly stating the missing
>definition _as part of the system described_.
>
>This is especially unfortunate because they spend a whole chapter
>(chapter V) to _rigorously prove_ that the system in question is
>/consistent/. This proof relies on the (alleged) "theorem" 'p ->
>(~p -> q)'. But this "theorem" is _not_ derivable in the system as
>described in the book.*)
>
>Actually, they write/claim (p. 50):
>
> "Now, it happens that 'p -> (~p -> q)' (in words_ 'if p, then if
> not-p, then q') is a theorem in the calculus. (We shall accept
> this as a fact, without exhibiting the derivation.)"
>
>Well, actually, it's NOT a fact, since 'p -> (~p -> q)' cannot be
>derived in the system /as described/.
>
>Hence imho the missing definition SHOULD be added to the text (or at
>least mentioned in a foodnote).
>
>
>F.
>
>____________________
>
>*) In chapter V Hilbert & Ackermannn's variant of Russell & Whitehead's
>system for propositional logic (in PM) is introduced. Even the formation
>rules for wffs are given. The ONLY thing that is missing is the
>_crucial_ definition: A -> B is short for ~A v B.
************************
David C. Ullrich
G. Frege
<ull...@math.okstate.edu> wrote:
>>
>> 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))
>>
>> Rules of derivation:
>>
>> - Substitution
>> - From S1 and S1 -> S2 derive S2. (MP)
>>
> Now I'm puzzled. Do they explicitly state what the
> primitives are?
>
No. Imho the presentation (in the book) is (slightly) screwed up here.
Look, David, they present a variant of Russell and Whitehead's system
(in the PM) namely (part of) the system presented by Hilbert and
Ackermann in "Grundzüge der theoretischen Logik", Berlin: Springer-
Verlag, 1928.
See:
http://www.math.uwaterloo.ca/~snburris/htdocs/WWW/PDF/hilbert.pdf
In this system (as well as in Russell and Whitehead's original system)
the primitives are ~ and v.
Hence I claimed:
"[What] is missing is the _crucial_ information that
'A -> B' means '~A v B' (where A, B are wffs)."
To which Peter Smith responded:
"...which is something known to any first-year student, i.e. anyone who
is likely to be tackling Nagel & Newman [...]."
Well, fine.
Still it's part of the discription of the system. For exmple, Burris
simply writes:
"Their formal system is the following:
[...]
4. Connectives: v and ~. (X -> Y means ~X v Y)."
>
> From your description of the system [presented in the book] it
> _looks_ like the primitives are v and ->.
>
Yes. And that's exactly the problem.
>
> If so then it makes no sense to say that the definition of p -> q
> is missing.
>
Right. Now it DOES make sense to say that the definition of p -> q is
missing (since this is a fact), hence by modus tollens we get: v and ->
are not the primitives of the system. :-)
Sincerely,
F.
P.S. Note that the system described by Nagel & Newman closely mirrors
(part of) the system stated by Gödel in his famous proof:
"...
2.1 Definitions
The basic signs of system P are the following:
I. Constant: "~" (not), "v" (or), [...], "(", ")" (parentheses).
:
The following formulae (I through V) are called axioms (they are written
with the help of the abbreviations (defined in the usual manner) ^, ->,
[...] and using the customary conventions for leaving out parentheses):
:
II. Every formula obtained by inserting arbitrary formulae for p, q, r
in the following schemata. We call these proposition axioms.
1. p v p -> p
2. p -> p v q
3. p v q -> q v p
4. (p -> q) -> (r v p -> r v q)
..."
(Kurt Gödel, On formally undecidable propositions of Principia
Mathematica and related systems I.)
You see, _Gödel_ clearly states (concerning the axioms):
they are written with the help of the abbreviations
(defined in the usual manner) ..., ->, ...
G. Frege
>>>
>>> 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))
>>>
>>> Rules of derivation:
>>>
>>> - Substitution
>>> - From S1 and S1 -> S2 derive S2. (MP)
>>>
>> Now I'm puzzled. Do they explicitly state what the
>> primitives are?
>>
>No. Imho the presentation (in the book) is (slightly) screwed up here.
>
> Look, David, they present a variant of Russell and Whitehead's system
> (in the PM) namely (part of) the system presented by Hilbert and
> Ackermann in "Grundzüge der theoretischen Logik", Berlin: Springer-
> Verlag, 1928.
>
> See:
> http://www.math.uwaterloo.ca/~snburris/htdocs/WWW/PDF/hilbert.pdf
>
> In this system (as well as in Russell and Whitehead's original system)
> the primitives are ~ and v.
>
You will find a modern treatment of this system in Halmos' and Givant's
"Logic as Algebra" (1998).
There (p. 15f) you will find the following statements:
"As [an] abbreviation, we introduce a new connective. It is denoted by
the symbol
->
and it is defined, whenever x and y are sentences, by saying that
(x -> y)
means
((~x) v y)."
Well, right.
And it's exactly this information which is missing in Nagel & Newman's
"Gödel's Proof".
F.
G. Frege
>>
>> From your description of the system [presented in the book] it
>> _looks_ like the primitives are v and ->.
>>
> Yes. [...]
>
But that's not Nagel & Newman's fault. In another thread I just wrote:
"Actually, it already WAS criticized by scholars of logic that Russell
does not stick to the primitives of the system (i.e. 'v' and '~') when
formulating his axioms."
And it shows...
F.
Mitch
> wrote:
> > Is a truth-table for that statement that shows it to be true in all
> > combinations of T and F for p and q considered to be a valid
> > proof of its truth?
>
>
> NO Sorry i need to use capitals here.
> Something is a proof if there is a derrivation of the theorem from
> the axioms and inference rules.
> A proof is very strict thing.
>
> Truth tables do not prove anything.
It sounds like you're actually not joking here.
> But you can say (if you really like them) they show it
>
> And if you are very philosophical you can follow Wittgenstein
> "Every tautology itself shows that it is a tautology" 6,127
> and
> "What can be shown, cannot be said." 4.1212
But here it sounds like you -are- kidding, it sounds like you are
quoting Wittgenstein sarcastically. or maybe that's my reading.
Very confusing.
To be explicit:
- Truth tables are a perfectly sound and adequate proof method for
propositional calculus.
- Wittgenstein, however fascinating his words might be, should not be
considered an authority on formal logical methods.
Mitch
translogi
Sorry i am a bit sarcastic on Wittgenstein.
(I am not a big fan of him, and his logic in my opinion is illogical,)
6.1203 In order to recognize an expression as a tautology, in cases
where no generality-sign occurs in it, one can employ the following
intuitive method:
Do try to solve a litle bit more complex tautology by it...
And i do think that truthtables do not prove anything.
(But they are handy to check if you are right)
Why use two valued logic if it is nowhere explicitly stated that we
are using two valued logic?
Intuitionistic logic does not comply to them.
ect ect.
But i still have to learn to do it the Hilbert style way.
translogi
Do you also teach intuitionistic logic? (just joking it isn't a
tautology in that system that is why, but i know that you know that.)
Alan Smaill
> On Nov 1, 11:10 pm, Peter_Smith <ps...@cam.ac.uk> wrote:
>> It was asked:
>>
>> > Is a truth-table for that statement that shows it to be true in
>> > all combinations of T and F for p and q considered to be a valid
>> > proof of its truth?
>>
>> If that means "a valid proof in deductive system S", the answer for
>> most systems S is, of course, trivially "no", since a proof-in-system-
>> S is typically defined otherwise (in terms of e.g. a sequence of axiom-
>> instances, or applications of rules of inference to previous items in
>> the sequence). That's trivial.
>>
>> What I was commenting on was the unqualified claim that
>>
>> >> Truth tables do not prove anything.
>>
>> That is plainly over-stating the case. For of course, giving a truth-
>> table can prove that a wff is a tautology, and hence true. [If I set
>> students an exercise "prove 洵(P v 洵星) is a tautology" and they do a
>> correct truth-table, they get full marks! :-) ]
>
> Do you also teach intuitionistic logic? (just joking it isn't a
> tautology in that system that is why, but i know that you know that.)
isn't it?
--
Alan Smaill
G. Frege
wrote:
>
> 6.1203 In order to recognize an expression as a tautology, in cases
> where no generality-sign occurs in it, one can employ the following
> intuitive method:
>
> Do try to solve a little bit more complex tautology by it...
>
Don't be unjust. Wittgenstein also introduced truth tables in his
Tractatus. (Of course the method described in 6.1203 is impractical in
general.)
>
> And I do think that truth tables do not prove anything.
>
Again, of course a TT DOES prove something (at meta level): it may (or
may not) prove that the formula in question is a tautology.
Look [assume a classical context]:
(Meta-)Theorem: The formula "p v ~p" is a tautology.
(Meta-)Proof: via TT.
>
> Why use two valued logic if it is nowhere explicitly stated that we
> are using two valued logic?
>
It's called /classical/ logic.
translogi
> translogi <wilem...@googlemail.com> writes:
> > On Nov 1, 11:10 pm, Peter_Smith <ps...@cam.ac.uk> wrote:
> >> It was asked:
>
> >> > Is a truth-table for that statement that shows it to be true in
> >> > all combinations of T and F for p and q considered to be a valid
> >> > proof of its truth?
>
> >> If that means "a valid proof in deductive system S", the answer for
> >> most systems S is, of course, trivially "no", since a proof-in-system-
> >> S is typically defined otherwise (in terms of e.g. a sequence of axiom-
> >> instances, or applications of rules of inference to previous items in
> >> the sequence). That's trivial.
>
> >> What I was commenting on was the unqualified claim that
>
> >> >> Truth tables do not prove anything.
>
> >> That is plainly over-stating the case. For of course, giving a truth-
> >> table can prove that a wff is a tautology, and hence true. [If I set
> >> correct truth-table, they get full marks! :-) ]
>
> > Do you also teach intuitionistic logic? (just joking it isn't a
> > tautology in that system that is why, but i know that you know that.)
>
> isn't it?
>
> --
>
> - Show quoted text -
In intuitionistic logic (A v ~A) is not a theorem
neither is ~~A -> A
neither is ((A -> B) & (~A -> B)) -> B
and there is also a fourth from that also is not a theorem.
(they are all interchangable)
A -> ~~A is a theorem
A -> (~A -> B ) is also a theorem (but not in minimal logic)
G. Frege
wrote:
>
> In intuitionistic logic [...]
>
Relevance for the present thread?
Jan Burse
> On Fri, 02 Nov 2007 21:32:38 -0000, translogi <wile...@googlemail.com>
> wrote:
>
>> In intuitionistic logic [...]
>>
> Relevance for the present thread?
>
>
> F.
>
G. Frege
wrote:
>>>
>>> In intuitionistic logic [...]
>>>
>> Relevance for the present thread?
>>
> Subset of classical logic. Don't be shy.
>
But we are not interested in a subset of classical logic (at least not
in the present thread).
Nagel & Newman promised to state a complete system for (classical)
propositional logic.
Alan Smaill
> On Nov 2, 7:25 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> translogi <wilem...@googlemail.com> writes:
>> > On Nov 1, 11:10 pm, Peter_Smith <ps...@cam.ac.uk> wrote:
>> >> It was asked:
>>
>> >> > Is a truth-table for that statement that shows it to be true in
>> >> > all combinations of T and F for p and q considered to be a valid
>> >> > proof of its truth?
>>
>> >> If that means "a valid proof in deductive system S", the answer for
>> >> most systems S is, of course, trivially "no", since a proof-in-system-
>> >> S is typically defined otherwise (in terms of e.g. a sequence of axiom-
>> >> instances, or applications of rules of inference to previous items in
>> >> the sequence). That's trivial.
>>
>> >> What I was commenting on was the unqualified claim that
>>
>> >> >> Truth tables do not prove anything.
>>
>> >> That is plainly over-stating the case. For of course, giving a truth-
>> >> table can prove that a wff is a tautology, and hence true. [If I set
>> >> students an exercise "prove 洵(P v 洵星) is a tautology" and they do a
>> >> correct truth-table, they get full marks! :-) ]
>>
>> > Do you also teach intuitionistic logic? (just joking it isn't a
>> > tautology in that system that is why, but i know that you know that.)
>>
>> isn't it?
>>
> In intuitionistic logic (A v ~A) is not a theorem
> neither is ~~A -> A
> neither is ((A -> B) & (~A -> B)) -> B
> and there is also a fourth from that also is not a theorem.
>
> (they are all interchangable)
>
>
>
> A -> ~~A is a theorem
> A -> (~A -> B ) is also a theorem (but not in minimal logic)
right, but the formula in question is not (A v ~A), it is
(equivalent to) ~~(A v ~A);
and that is intuitionistically provable.
--
Alan Smaill
translogi
> translogi <wilem...@googlemail.com> writes:
> > On Nov 2, 7:25 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> >> translogi <wilem...@googlemail.com> writes:
> >> > On Nov 1, 11:10 pm, Peter_Smith <ps...@cam.ac.uk> wrote:
> >> >> It was asked:
>
> >> >> > Is a truth-table for that statement that shows it to be true in
> >> >> > all combinations of T and F for p and q considered to be a valid
> >> >> > proof of its truth?
>
> >> >> If that means "a valid proof in deductive system S", the answer for
> >> >> most systems S is, of course, trivially "no", since a proof-in-system-
> >> >> S is typically defined otherwise (in terms of e.g. a sequence of axiom-
> >> >> instances, or applications of rules of inference to previous items in
> >> >> the sequence). That's trivial.
>
> >> >> What I was commenting on was the unqualified claim that
>
> >> >> >> Truth tables do not prove anything.
>
> >> >> That is plainly over-stating the case. For of course, giving a truth-
> >> >> table can prove that a wff is a tautology, and hence true. [If I set
> >> >> correct truth-table, they get full marks! :-) ]
>
> >> > Do you also teach intuitionistic logic? (just joking it isn't a
> >> > tautology in that system that is why, but i know that you know that.)
>
> >> isn't it?
>
> > In intuitionistic logic (A v ~A) is not a theorem
> > neither is ~~A -> A
> > neither is ((A -> B) & (~A -> B)) -> B
> > and there is also a fourth from that also is not a theorem.
>
> > (they are all interchangable)
>
> > A -> ~~A is a theorem
> > A -> (~A -> B ) is also a theorem (but not in minimal logic)
>
> right, but the formula in question is not (A v ~A), it is
> (equivalent to) ~~(A v ~A);
> and that is intuitionistically provable.
>
> --
>
> - Show quoted text -
No it isn't.
If it was it would be a theorem
(maybe you can prove)
(~~(A v ~A)) --> ( ~~(A v ~~~A))
but ~~(A v ~A) no please show it.
(and i will point out the error)
David C. Ullrich
>On Fri, 02 Nov 2007 07:57:13 -0600, David C. Ullrich
><ull...@math.okstate.edu> wrote:
>
>>>
>>> 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))
>>>
>>> Rules of derivation:
>>>
>>> - Substitution
>>> - From S1 and S1 -> S2 derive S2. (MP)
>>>
>> Now I'm puzzled. Do they explicitly state what the
>> primitives are?
>>
>No. Imho the presentation (in the book) is (slightly) screwed up here.
>
>Look, David, they present a variant of Russell and Whitehead's system
>(in the PM) namely (part of) the system presented by Hilbert and
>Ackermann in "Grundzüge der theoretischen Logik", Berlin: Springer-
>Verlag, 1928.
>
>See:
>http://www.math.uwaterloo.ca/~snburris/htdocs/WWW/PDF/hilbert.pdf
>
>In this system (as well as in Russell and Whitehead's original system)
>the primitives are ~ and v.
Are both the following true in those _other_ systems?
(i) It's explicitly stated that the primitives are ~ and v.
(ii) The axioms use nothing but -> and v.
Just curious.
>Hence I claimed:
>
> "[What] is missing is the _crucial_ information that
> 'A -> B' means '~A v B' (where A, B are wffs)."
>
>To which Peter Smith responded:
>
>"...which is something known to any first-year student, i.e. anyone who
>is likely to be tackling Nagel & Newman [...]."
>
>Well, fine.
>
>Still it's part of the discription of the system. For exmple, Burris
>simply writes:
>
> "Their formal system is the following:
>
> [...]
>
> 4. Connectives: v and ~. (X -> Y means ~X v Y)."
Does Burris state explicitly that this is the system being
used in Nagel&Newman?
>>
>> From your description of the system [presented in the book] it
>> _looks_ like the primitives are v and ->.
>>
>Yes. And that's exactly the problem.
>
>>
>> If so then it makes no sense to say that the definition of p -> q
>> is missing.
>>
>Right. Now it DOES make sense to say that the definition of p -> q is
>missing (since this is a fact), hence by modus tollens we get: v and ->
>are not the primitives of the system. :-)
This is a very curious attitude. You say that they don't explicitly
state what the primitives are (which if true is certainly a bad
thing).
Given that the axioms mention nothing but v and -> it's very hard
to see why you'd conclude that the primitives are not just v and ->.
I've seen your many references to _other_ systems where the
primitives are something else. So what?
>Sincerely,
>F.
>
>
>P.S. Note that the system described by Nagel & Newman closely mirrors
>(part of) the system stated by Gödel in his famous proof:
Does Godel explicitly state that he's describing the system
used by Nagel&Newman?
>"...
>
>2.1 Definitions
>
>The basic signs of system P are the following:
>
>I. Constant: "~" (not), "v" (or), [...], "(", ")" (parentheses).
>
>:
>
>The following formulae (I through V) are called axioms (they are written
>with the help of the abbreviations (defined in the usual manner) ^, ->,
>[...] and using the customary conventions for leaving out parentheses):
>
>:
>
>II. Every formula obtained by inserting arbitrary formulae for p, q, r
>in the following schemata. We call these proposition axioms.
>
>1. p v p -> p
>2. p -> p v q
>3. p v q -> q v p
>4. (p -> q) -> (r v p -> r v q)
>
>..."
>
>(Kurt Gödel, On formally undecidable propositions of Principia
>Mathematica and related systems I.)
>
>You see, _Gödel_ clearly states (concerning the axioms):
>
> they are written with the help of the abbreviations
> (defined in the usual manner) ..., ->, ...
************************
David C. Ullrich
G. Frege
<ull...@math.okstate.edu> wrote:
>
> Are both the following true in those [...] systems?
>
> (i) It's explicitly stated that the primitives are ~ and v.
>
Yes.
>
> (ii) The axioms use nothing but -> and v.
>
Yes.
"Actually, it already WAS criticized by scholars of logic that
Russell & Whitehead did not stick to the primitives of the
system (i.e. 'v' and '~') when formulating his axioms."
And it shows...
>
> You say that they don't explicitly state what the primitives are
> (which if true is certainly a bad thing).
>
Right, hence I claimed "Imho the presentation (in the book) is
(slightly) screwed up here."
>
> Given that the axioms mention nothing but v and -> it's very hard
> to see why you'd conclude that the primitives are not just v and ->.
>
Actually, it's in no way "hard": Because they aren't.
Here's a question for _you_:
How would you define "~" using "v" and "->"?
Moreover:
My point is that several *relevant* claims by Nagel & Newman (made
in their book) are _false_ without explicitly stating the missing
definition _as part of the system described_.
This is especially unfortunate because they spend a whole chapter
(chapter V) to _rigorously prove_ that the system in question is
/consistent/. This proof relies on the (alleged) "theorem" 'p ->
(~p -> q)'. But this "theorem" is _not_ derivable in the system as
described in the book.
Actually, they write/claim (p. 50):
"Now, it happens that 'p -> (~p -> q)' (in words_ 'if p, then if
not-p, then q') is a theorem in the calculus. (We shall accept
this as a fact, without exhibiting the derivation.)"
Well, actually, it's NOT a fact, since 'p -> (~p -> q)' cannot be
derived in the system /as described/.
>
> I've seen your many references to _other_ systems where the
> primitives are something else. So what?
>
There is only ONE system in question here: Hilbert & Ackermann's
simplification of Russell and Whitehead's system (which subsequently was
used by GÖDEL (sic!) in his proof).
The PROBELM obviously is that Nagel & Newman (slightly) screwed up the
presentation OF THIS SYSTEM.
Especially, the forgot to mention the *CRUCIAL* fact that
A -> B
means
~A v B
for any formulas A, B.
F.
G. Frege
>
> Two Laws of Logic Books
>
> 1. There are always, ALWAYS, typos/thinkos
>
Right, for example at page 114 in their book (2001) Nagel & Newman state
"It was not until 1899 that the arithmetic of cardinal numbers
was axiomatized, by the Italian mathematician Giuseppe Peano."
But of course the correct year is 1889:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In 1889 Peano published his famous axioms, called Peano axioms, which
defined the natural numbers in terms of sets. These were published in a
pamphlet /Arithmetices principia, nova methodo exposita/ which,
according to [H. C. Kennedy] were:
... at once a landmark in the history of mathematical logic
and of the foundations of mathematics.
J. J. O'Connor and E. F. Robertson, The MacTutor History of Mathematics
archive.
http://www-groups.dcs.st-and.ac.uk/~history/Biographies/Peano.html
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jack Campin - bogus address
>>> Relevance for the present thread?
>> Subset of classical logic. Don't be shy.
> But we are not interested in a subset of classical logic (at least not
> in the present thread).
> Nagel & Newman promised to state a complete system for (classical)
> propositional logic.
The issue is whether their axiomatization really *does* characterize
classical propositional logic rather than some subsystem, isn't it?
If it can't prove the equivalence of (A -> B) and (~A v B), that isn't
at all obvious.
============== j-c ====== @ ====== purr . demon . co . uk ==============
Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
<http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
G. Frege
<bo...@purr.demon.co.uk> wrote:
>
> The issue is whether their axiomatization really *does* characterize
> classical propositional logic rather than some subsystem, isn't it?
>
No, that's not the issue. It doesn't.*) Contrary to their claim.
F.
___________
*) Proof is left as an exercise.
G. Frege
Should read:
>
> "Actually, it already WAS criticized by scholars of logic that
> Russell & Whitehead did not stick to the primitives of the
> system (i.e. 'v' and '~') when formulating their axioms."
> ~~~~~
>>
>> Given that the axioms mention nothing but v and -> it's very hard
>> to see why you'd conclude that the primitives are not just v and ->.
>>
Is it? Did you TRY to DERIVE anything in this system (as given)?
Obviously not. :-/
Hint: You won't _see_ it by (just) looking at the axioms.
This is something that is "hidden"; especially, when
there is not the least hint that A -> B actually means
(is defined as) ~A v B in this system.
Ok, here's the system again _as stated in the book_:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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))
Rules of derivation:
- Substitution
- From S1 and S1 -> S2 derive S2. (MP)
[ No definitions. Though the connectives allowed
for usage in a wff are "~", "v", "->", and ".".]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Please derive
p -> p
as a theorem.
Thanks.
Jan Burse
> 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.
Isn't it that the actual calculus is exchangeable,
and the Gödel proof should still goes through?
Anyway, I think there is a definition, sort of, that
A->B equals ~A v B. But it is totally scrambled in
the english translation I find on the internet, and
I don't have the german original at hand:
Remark to Axiom V:
(http://www.whitenationalism.com/etext/godel/godel3.htm)
A formula c is called an immediate consequence of a and b, if a is
the formula (~(b)) v (c), or an immediate consequenee of a, if c
is the formula v forall (a), where v denotes any given variable.
I guess this should read:
A formula c is called an immediate consequence of b in a, if a is
the formula (~(b)) v (c), or an immediate consequence of b in d,
if d is the formula forall v (a), where v denotes any given
variable.
Actually another translation isn't really better:
Remark to Axiom V here:
(http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf)
A formula c is called the immediate consequence of a and b (of a)
if a is the formula ~b v c (or if c is the formula forall v . a,
where v is any variable).
I guess this should read:
A formula c is called the immediate consequence of b in a
if a is the formula ~b v c (or if a is the formula forall v . ~b v
c, where v is any variable).
The first translation includes a foot note:
24 The rule of substitution becomes superfluous, since we have
already dealt with all possible substitutions in the axioms
themselves (as is also done in J. v. Neumann, 'Zur Hilbertschen
Beweistheorie', Math. Zeitschr. 26, 1927).
Which is available online:
http://www.gdz-cms.de/dms/load/img/?IDDOC=82643
There are the following open questions (for me):
- Isn't the definition of immediate consequence a very sloppy
mish mash of |- and ->?
- Does Gödel work with a consequence relation that automatically
all quantifies the premisses or does it allow a communication
between the variables in the premisse and the consequence.
(Has consequences on the deduction theorem etc..)?
- Does the v. Neuman reference help in an understanding
of Godel or is Hilbert & Ackerman enough?
- If the hypotheses stands that the calculus is exchangeable,
would it make sense to rework Gödel with another more modern
calculus?
Bye
Jan Burse
> There are the following open questions (for me):
- Isn't there already a publication by Gödel himself
or by others that clarified things?
Bye
G. Frege
wrote:
>
> Isn't it that the actual calculus is exchangeable,
> and the Gödel proof should still goes through?
>
Of course - if the calculus is strong enough. Remember the title of the
proof:
"On Formally Undecidable Propositions of Principia Mathematica
and Related Systems I."
~~~~~~~~~~~~~~~~~~~
>
> Anyway, I think there is a definition, sort of, that A->B
> equals ~A v B.
>
No, it's not _explicitly_ stated. But Gödel _refers_ to that definition;
he writes:
"The basic signs of system P are the following:
I. Constant: "~" (not), "v" (or), [...], "(", ")" (parentheses).
:
The following formulae (I through V) are called axioms (they are written
with the help of the abbreviations (defined in the usual manner) ^, ->,
[...] and using the customary conventions for leaving out parentheses):
[...]"
(Kurt Gödel, On formally undecidable propositions of Principia
Mathematica and related systems I.)
So, you see, the primitive connectives (in the system he considers) are
'v' and '~'. While '->' is just (introduced as) an "abbreviation
(defined in the usual manner)".
~~~~~~~~~~~~~~~~~~~~~~~~~~~
The usual manner for '->', of course is
A -> B =df ~A v B
in this system.
>
> A formula c is called an immediate consequence of a and b, if a is
> the formula (~(b)) v (c),
>
Using the mentioned abbreviation (etc.) this reads:
> A formula c is called an immediate consequence of a and b, if a is
> the formula b -> c.
>
With other words, c is an immediate consequence of b -> c and b.
>
> The first translation includes a foot note:
>
> 24) The rule of substitution becomes superfluous, since we have
> already dealt with all possible substitutions in the axioms
> themselves (as is also done in J. v. Neumann, 'Zur Hilbertschen
> Beweistheorie', Math. Zeitschr. 26, 1927).
>
Right. The idea is that we do not need /Substitution/ as a rule of
derivation if we adopt axiom schemata instead of axioms proper. (It
was von Neumann who came up with this idea.)
Gödel:
"The following formulae (I through V) are called axioms (they are
written with the help of the abbreviations (defined in the usual manner)
^, ->, [...] and using the customary conventions for leaving out
parentheses):
:
II. Every formula obtained by inserting arbitrary formulae for p, q, r
in the following schemata. We call these propositional axioms.
1. p v p -> p
2. p -> p v q
3. p v q -> q v p
4. (p -> q) -> (r v p -> r v q)
..."
(Kurt Gödel, On formally undecidable propositions of Principia
Mathematica and related systems I.)
So the axioms are not the axiom schemata 1.-4. but the formulas that
result from these formulas "by inserting arbitrary formulae for p, q,
r".
You will see that I also adopted this feature in the system used in my
post "Proof of a certain theorem in “Gödel's Proof” by Nagel & Newman".
>
> There are the following open questions (for me):
>
> - Isn't the definition of immediate consequence a very sloppy
> mish mash of |- and ->?
>
No. Actually, this notion is used to define the /class of provable
formulae/.
"The /class of provable formulae/ is defined as the smallest class of
formulae that contains the axioms and is closed under the relation
„immediate consequence“."
I guess, this is meant the following way:
Definitions:
C(a, b, c) :<=> a = b -> c
"c is an immediate consequence of a and b."
closed(X) :<=> AaAbAc(a e X & b e X & C(a, b, c) => c e X)
"X is closed under the relation „immediate consequence“."
Now if T is the /class of provable formulae/, we have:
AXIOMS c T & closed(T) &
AX(AXIOMS c X & closed(X) => T c X)
This means that all axioms are in T and if the formulas b -> c and b are
in T, then the formula c is in T too. Actually, T contains _exactly_ the
axioms and all formulas that can be derived from those axioms in
finitely many steps using the rule of derivation MP. (/Substitution/ is
not part of the system, as already mentioned.)
(For simplicity I only considered the propositional part here.)
>
> - Does Gödel work with a consequence relation that automatically
> all quantifies the premisses or does it allow a communication
> between the variables in the premisse and the consequence.
> (Has consequences on the deduction theorem etc..)?
>
In the system considered by Gödel _there are no_ "premisses" - better
call them _assumptions_ to avoid confusion. There are no assumptions.
(Hence no "communication" has to be considered, and no Dth.)
>
> - Does the v. Neumann reference help in an understanding
> of Godel or is Hilbert & Ackermann enough?
>
No. Hilbert & Ackermann is enough.
>
> - If the hypotheses stands that the calculus is exchangeable,
> would it make sense to rework Gödel with another more modern
> calculus?
>
Yes. It has been done. (See references below.)
>
> - Isn't there already a publication by Gödel himself
> or by others that clarified things?
>
Sure. There are many books concerning Gödel's proof. You might check,
for example:
Raymond Smullyan: Gödel's Incompleteness Theorems. Oxford Logic Guides.
Oxford University Press, 1992.
Torkel Franzén: Gödel's Theorem: An Incomplete Guide to its Use and
Abuse. A.K. Peters, 2005.
Peter Smith, An Introduction to Gödel's Theorems. Cambridge
Introductions to Philosophy. Cambridge University Press, 2007.
Reference:
http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems
G. Frege
<ull...@math.okstate.edu> wrote:
>
> I don't suppose there's a definition of ~ in terms of v and -> given?
>
I don't think that it's possible to define ~ in terms of v and ->, since
{v, ->} is not functionally complete.
G. Frege
>>
>> _If_ in fact -> is a primitive then we need a definition of ~.
>>
Right, but I don't think this is possible _if_ the primitives (as you
seem to suggest*) are just v and ->.
>>
>> I don't suppose there's a definition of ~ in terms of v and -> given?
>>
> I don't think that it's possible to define ~ in terms of v and ->, since
> {v, ->} is not functionally complete.
>
Intuitively, I'd “argue” (well, it's just an ad hoc consideration) the
following way.
~p
is a (truth-)function of a single variable, namely "p". Hence the only
"relevant" variable that occurs in the definiens (the defining
expression) is "p". ("relevant" here means that the [value of the]
defined term "depends" from the [value of the] variable.)
This means that the defining expression is "effectively" build up with
"->" and/or "v" and "p". But p -> p = T for any assignment of F/T to p,
and p v p = p. Moreover p -> T = T, T -> p = p, p v T = T, T v p = T.
Hence all that can be "achieved" with a formula X build up this way is X
= p or X = T.
But then ~p cannot be define this way.
In other words, {v, ->} is not functionally complete.
F.
________________________
*) "Given that the axioms mention nothing but v and -> it's very hard
to see why you'd conclude that the primitives are not just v and ->."
--
Mitch
> Wittgenstein also introduced truth tables in his
> Tractatus.
Frege, Peirce, and Schroeder hold priority to the concept of truth
functionals (late 1800's). Post and Lukasiewicz first used the tabular
form of turth tables. Wittgenstein is responsible for popularizing the
truth table, and I suspect only for philosophers. Where the electrical
engineers got it, I don't know (and I don't think it was
Wittgenstein).
> (Of course the method described in 6.1203 is impractical in
> general.)
Currently, for all known decision methods for propositional calculus,
it is not known if any are not impractical (infeasible, exponential
time) on all inputs of a given size.
Mitch
Newberry
> 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.
>
> 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.)"
>
> 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))
>
>
> S1 -> S2 =df ~S1 v S2
>
> Rules of derivation:
>
> - Substitution
> - From S1 and S1 -> S2 derive S2. (MP)
>
> 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)
>
>
> (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?
G. Frege
>>
>> Wittgenstein also introduced truth tables in his Tractatus.
>>
> Frege, Peirce, and Schroeder hold priority to the concept of truth
> functionals (late 1800's). Post and Lukasiewicz first used the tabular
> form of turth tables. Wittgenstein is responsible for popularizing the
> truth table, and I suspect only for philosophers.
>
Try to get that straight:
"The pattern of reasoning that the truth table tabulates was Frege's,
Peirce's, and Schröder's by 1880. The tables have been prominent in
literature since 1920 (Lukasiewicz, Post, Wittgenstein)."
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(W.V.O. Quine, Methods of Logic)
>>>
>>> "6.1203 In order to recognize an expression as a tautology,
>>> in cases where no generality-sign occurs in it, one can
>>> employ the following intuitive method: [...]"
>>>
>>> Do try to solve a litle bit more complex tautology by it...
>>>
>> Of course the method described in 6.1203 is impractical in
>> general.
>>
> Currently [bla bla bla]
>
Shut up, idiot.
G. Frege
wrote:
>
> This may be a bit off topic but it is on Nagel/Newman.
>
Yes, it's "off topic" (in the current thread). So why don't you just
start a new thread? :-o
Alan Smaill
> On Nov 2, 11:18 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
>> translogi <wilem...@googlemail.com> writes:
>> > In intuitionistic logic (A v ~A) is not a theorem
>> > neither is ~~A -> A
>> > neither is ((A -> B) & (~A -> B)) -> B
>> > and there is also a fourth from that also is not a theorem.
>>
>> > (they are all interchangable)
>>
>> > A -> ~~A is a theorem
>> > A -> (~A -> B ) is also a theorem (but not in minimal logic)
>>
>> right, but the formula in question is not (A v ~A), it is
>> (equivalent to) ~~(A v ~A);
>> and that is intuitionistically provable.
>>
> No it isn't.
> If it was it would be a theorem
> (maybe you can prove)
> (~~(A v ~A)) --> ( ~~(A v ~~~A))
I can show ~A <-> ~~~A, so yes.
> but ~~(A v ~A) no please show it.
> (and i will point out the error)
Glivenko's theorem says that any propositional statement
of the form ~P is intuitionistically provable iff it is a classical
tautology. (special case of theorem 3.1 in Mints' Short Intro
to IL).
If you disagree, by all means provide a counter-model.
--
Alan Smaill
David C. Ullrich
>On Sat, 03 Nov 2007 06:24:09 -0600, David C. Ullrich
><ull...@math.okstate.edu> wrote:
>
>>
>> Are both the following true in those [...] systems?
>>
>> (i) It's explicitly stated that the primitives are ~ and v.
>>
>Yes.
>
>>
>> (ii) The axioms use nothing but -> and v.
>>
>Yes.
>
> "Actually, it already WAS criticized by scholars of logic that
> Russell & Whitehead did not stick to the primitives of the
> system (i.e. 'v' and '~') when formulating his axioms."
>
> And it shows...
>
>>
>> You say that they don't explicitly state what the primitives are
>> (which if true is certainly a bad thing).
>>
>Right, hence I claimed "Imho the presentation (in the book) is
>(slightly) screwed up here."
>
>>
>> Given that the axioms mention nothing but v and -> it's very hard
>> to see why you'd conclude that the primitives are not just v and ->.
>>
>Actually, it's in no way "hard": Because they aren't.
>
> Here's a question for _you_:
> How would you define "~" using "v" and "->"?
Yes, I realized later that that's not possible.
************************
David C. Ullrich
G. Frege
<ull...@math.okstate.edu> wrote:
>>>
>>> Given that the axioms mention nothing but v and -> it's very hard
>>> to see why you'd conclude that the primitives are not just v and ->.
>>>
>> Actually, it's in no way "hard": Because they aren't. [Can't be!]
>>
>> Here's a question for _you_:
>> How would you define "~" using "v" and "->"?
>>
> Yes, I realized later that that's not possible.
>
Fine. Now, did I succeed in convincing you that there's indeed something
(namely a certain definition) missing in the book?
You know:
>>
>> My point is that several distinguished claims by Nagel & Newman (made
>> in their book) are _false_, given the system /as described/.
>>
>> This is especially unfortunate because they spend a whole chapter
>> (chapter V) to _rigorously prove_ that the system in question is
>> /consistent/. This proof relies on the (alleged) "theorem" 'p ->
>> (~p -> q)'. But this "theorem" is _not_ derivable in the system as
>> described in the book.
>>
>> Actually, they write/claim (p. 50):
>>
>> "Now, it happens that 'p -> (~p -> q)' (in words: 'if p, then if
>> not-p, then q') is a theorem in the calculus. (We shall accept
>> this as a fact, without exhibiting the derivation.)"
>>
>> Well, actually, it's NOT a fact, since 'p -> (~p -> q)' cannot be
>> derived in the system /as described/.
>>
Remedy: add the comment:
A -> B
means (is defined with)
~A v B.
If you can think of an _alternative_ "solution", tell me.
G. Frege
>>
>> I've seen your many references to _other_ systems where the
>> primitives are something else. So what?
>>
> There is only ONE system in question here: Hilbert & Ackermann's
> simplification of Russell and Whitehead's system (which subsequently
> was used by Gödel (sic!) in his proof).
>
Hint: "If it walks like a duck and quacks like a duck, you can be
reasonably sure it is a duck." :-)
>
> The PROBELM obviously is that Nagel & Newman (slightly) screwed up the
> presentation OF THIS SYSTEM.
>
> Especially, the forgot to mention the *CRUCIAL* fact that
>
> A -> B
>
> means
>
> ~A v B
>
> for any formulas A, B.
>
Now you will find a modern treatment of this system in Halmos' and
Givant's "Logic as Algebra" (1998). There (on p. 15) they make the
following statement:
"As abbreviation, we introduce a new connective. It is denoted by
the symbol
->
and is defined, whenever x and y are sentences, by saying that
(x -> y)
means
((~x) v y)."
It's exactly this information that is missing in Nagel & Newman's
"Gödel's Proof".
Daryl McCullough
>> right, but the formula in question is not (A v ~A), it is
>> (equivalent to) ~~(A v ~A);
>> and that is intuitionistically provable.
>No it isn't.
>If it was it would be a theorem
It certainly is a theorem.
Note the following:
Lemma: If X -> Y, then ~Y -> ~X.
Proof: Assume the three assumptions (1) X->Y, (2) ~Y, (3) X
From (1) and (3) we derive Y. From (2) we get ~Y. So these
three assumptions are contradictory (they allow you to derive
Y & ~Y). So from assumptions (1) and (2) we can derive ~X.
(To derive ~X, you only need to show that assuming X leads
to a contradiction). Now, we use the fact that if assuming
~Y allows you to prove ~X, then without assuming ~Y, you
can prove ~Y -> ~X. Therefore, we have
Assuming (X->Y), one can derive ~Y -> ~X.
Now, let's apply this in the case where
Y = (A v ~A).
Now, certainly A -> (A v ~A). Therefore, using
the lemma we just proved, we can derive
~(A v ~A) -> ~A
Similarly, ~A -> (A v ~A). So again using
the lemma, we can derive
~(A v ~A) -> ~~A
Putting these two together, we have:
~(A v ~A) -> ~A & ~~A
Since ~A & ~~A is a contradiction, we have:
From ~(A v ~A), we can derive a contradiction.
If we can derive a contradiction from X, then that's
a proof of ~X. Therefore, we've proved
~~(A v ~A)
--
Daryl McCullough
Ithaca, NY
Jan Burse
>> A formula c is called an immediate consequence of a and b, if a is
>> the formula (~(b)) v (c),
>>
> Using the mentioned abbreviation (etc.) this reads:
>
>> A formula c is called an immediate consequence of a and b, if a is
>> the formula b -> c.
>>
Ok, this would expresse the (one step) MP-Rule of the hilbert
style calculus Gödel uses. And then doing it multi step, gives
the provability consequence relation.
Fine, Tx.
Frederick Williams
>
> On Mon, 05 Nov 2007 07:36:33 -0600, David C. Ullrich
> <ull...@math.okstate.edu> wrote:
>
> >>>
> >>> Given that the axioms mention nothing but v and -> it's very hard
> >>> to see why you'd conclude that the primitives are not just v and ->.
> >>>
> >> Actually, it's in no way "hard": Because they aren't. [Can't be!]
> >>
> >> Here's a question for _you_:
> >> How would you define "~" using "v" and "->"?
> >>
> > Yes, I realized later that that's not possible.
> >
> Fine. Now, did I succeed in convincing you that there's indeed something
> (namely a certain definition) missing in the book?
The book is a pot boiler and one shouldn't expect too much of it.
--
Remove "antispam" and ".invalid" for e-mail address.
"He that giveth to the poor lendeth to the Lord, and shall be repaid,"
said Mrs Fairchild, hastily slipping a shilling into the poor woman's
hand.
translogi
OOps
You and Alan were right.
Burying my head deep under a stack of logic books...
Sorry
G. Frege
Williams"@antispamhotmail.co.uk.invalid> wrote:
>>
>> Now, did I succeed in convincing you that there's indeed something
>> (namely a certain definition) missing in the book?
>>
> The book is a pot boiler and one shouldn't expect too much of it.
>
Well...
"Despite its shortcomings, Nagel and Newman's book should be recognized
as a classic piece of expository literature. It can still be recommended
as an excellent introduction to the background of Gödel's incompleteness
theorem and to the philosophical issues to which Gödel’s result is
connected. Some of its technical exposition is flawed; some of its
philosophical claims are suspect. But it is notoriously difficult to say
something philosophically sensible in this area, and there are now a
number of excellent introductory presentations of the incompleteness
theorems, written for people with only a modicum of logical background,
containing reasonably complete proofs. Nagel and Newman's book can most
profitably be read preparatory to, or in conjunction with, one of these.
Its greatest merits are that it conveys the intellectual landscape in
which Gödel's paper appeared, the general nature of the ideas involved
in that paper, and something of the significance of the conclusions
he reached. The book is an excellent point of departure. After reading
it, one will want to learn more."
(Gödel's Proof, Reviewed by Timothy McCarthy, Notices of the AMS, March
2004. Source: http://www.ams.org/notices/200403/rev-mccarthy.pdf)
Completely agree with Timothy McCarthy's concluding remarks.
G. Frege
>
> Finally we may put all those proofs together. [...]
>
The derivation of the theorem is much simpler if we adopt axiom schemas
instead of axioms proper:
Axiom schemas:
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))
Definition:
A -> B =df ~A v B
Theorem:
p -> (~p -> q) (ECQ)
(1) (~p v ~p) -> ~p Ax. 1
(2) ((~p v ~p) -> ~p) -> ((~~p v (~p v ~p)) -> (~~p v ~p)) Ax. 4
(3) (~~p v (~p v ~p)) -> (~~p v ~p) MP 2,1
(4) ~p -> (~p v ~p) Ax. 2
(5) ~~p v (~p v ~p) Df. 4
(6) ~~p v ~p MP 3,5
(7) (~~p v ~p) -> (~p v ~~p) Ax. 3
(8) ~p v ~~p MP 7,6
(9) ~~p -> (~~p v q) Ax. 2
(10) ~~p -> (~p -> q) Df. 9
(11) (~~p -> (~p -> q)) -> ((~p v ~~p) -> (~p v (~p -> q))) Ax. 4
(12) (~p v ~~p) -> (~p v (~p -> q)) MP 11,10
(13) ~p v (~p -> q) MP 12,8
(14) p -> (~p -> q) Df. 13
G. Frege
wrote:
Some remarks.
Kontext:
"prove ~~(P v ~~~P)"
"[This formula] is equivalent to ~~(P v ~P);
and that is intuitionistically provable."
(Alan Smaill)
>
> No it isn't.
>
No?
>
> If it was [the following] would be a theorem
> ~~(P v ~P) -> ~~(P v ~~~P)
>
Right. That's a theorem in intuitionistic calculus.
>
> ~~(P v ~P)
>
Again, a theorem in intuitionistic calculus.
Proof?
Well, let's see. I'll use the system of natural deduction for
intuitionistic logic (NJ) introduced by Gentzen.
1 (1) ~(P v ~P) A
2 (2) P A
2 (3) P v ~P 2 vI
1,2 (4) _|_ 1,3 ~E
1 (5) ~P 2,4 ~I
1 (6) P v ~P 5 vI
1 (7) _|_ 1,6 ~E
(8) ~~(P v ~P) 1,7 ~I
With other words,
|-- ~~(P v ~P)
NJ
Great. Now how about
~~(P v ~~~P)
?
1 (1) ~(P v ~~~P) A
2 (2) P A
2 (3) P v ~~~P 2 vI
1,2 (4) _|_ 1,3 ~E
1 (5) ~P 2,4 ~I
6 (6) ~~P A
1,6 (7) _|_ 5,6 ~E
1 (8) ~~~P 6,7 ~I
1 (9) P v ~~~P 8 vI
1 (10) _|_ 1,9 ~E
(11) ~~(P v ~~~P) 1,10 ~I
With other words,
|-- ~~(P v ~~~P)
NJ
Now, since P -> (Q -> P) is a theorem of intuitionistic calculus, any
two theorems are equivalent, with other words,
if |-- X and |-- Y, then |-- X -> Y and |-- Y -> X.
NJ NJ NJ NJ
Let's first show
|-- P -> (Q -> P).
NJ
1 (1) P A
2 (2) Q A
1,2 (3) P & Q 1,2 &I
1,2 (4) P 3 &E
1 (5) Q -> P 2,4 ->I
(6) P -> (Q -> P) 1,5 ->I
Fine.
Now assume that |-- X and |-- Y.
NJ NJ
With |-- Y -> (X -> Y) and |-- X -> (Y -> X) [just shown]
NJ NJ
and applications of MP, we get |-- X -> Y and |-- Y -> X.
NJ NJ
qed.
For example:
We have (already shown)
|-- ~~(P v ~~~P)
NJ
and
|-- ~~(P v ~P)
NJ
Now we may write down the following proof
(1) ~~(P v ~~~P) TI (theorem introduction)
(2) (~~(P v ~~~P)) -> (~~(P v ~P) -> ~~(P v ~~~P)) TI
(3) ~~(P v ~P) -> ~~(P v ~~~P) 1,2 ->E (MP)
With other words,
|-- ~~(P v ~P) -> ~~(P v ~~~P)
NJ
(as required).
And we may write down the proof
(1) ~~(P v ~P) TI (theorem introduction)
(2) (~~(P v ~P)) -> (~~(P v ~~~P) -> ~~(P v ~P)) TI
(3) ~~(P v ~~~P) -> ~~(P v ~P) 1,2 ->E (MP)
With other words,
|-- ~~(P v ~~~P) -> ~~(P v ~P)
NJ
This finally proves Alan Smaill's claim
"[~~(P v ~~~P)] is equivalent to ~~(P v ~P);
and that is intuitionistically provable."
F.
"Unproven statements carry little weight in the world of mathematics."
(Amir D. Aczel)
G. Frege
wrote:
>>
>> ~~(A v ~A) certainly is a theorem.
>>
>> Note the following:
>>
>> Lemma: If X -> Y, then ~Y -> ~X.
>>
>> Proof: Assume the three assumptions (1) X -> Y, (2) ~Y, (3) X.
>> From (1) and (3) we derive Y. From (2) we get ~Y. So these
>> three assumptions are contradictory (they allow you to derive
>> Y & ~Y). So from assumptions (1) and (2) we can derive ~X.
>> (To derive ~X, you only need to show that assuming X leads
>> to a contradiction.) Now, we use the fact that if assuming
>> ~Y allows you to prove ~X, then without assuming ~Y, you
>> can prove ~Y -> ~X. [Dth. --G. F.] Therefore, we have
>>
>> Assuming X -> Y, one can derive ~Y -> ~X.
>>
The argument in the system of natural deduction for intuitionistic logic
(NJ) due to Gentzen.
1 (1) X -> Y A
2 (2) ~Y A
3 (3) X A
1,3 (4) Y 1,2 ->E
1,2,3 (5) _|_ 2,4 ~E
1,2 (6) ~X 3,5 ~I
1 (7) ~Y -> ~X 2,6 ->I
With other words,
X -> Y |- ~Y -> ~X. (Contra)
>>
>> Now, let's apply this in the case where
>> Y = (A v ~A).
>>
>> Now, certainly A -> (A v ~A). Therefore, using
>> the lemma we just proved, we can derive
>>
>> ~(A v ~A) -> ~A (*)
>>
>> Similarly, ~A -> (A v ~A). So again using
>> the lemma, we can derive
>>
>> ~(A v ~A) -> ~~A (**)
>>
Now assume ~(A v ~A), then we can derive
~A
(from (*)) as well as
~~A
(from (**)) and hence
~A & ~~A,
which is a contradiction. With other words,
>>
>> from ~(A v ~A), we can derive a contradiction.
>>
>> If we can derive a contradiction from X, then that's
>> a proof of ~X. Therefore, we've proved
>>
>> ~~(A v ~A).
>>
Argument from above:
1 (1) A A
1 (2) A v ~A 1 vI
(3) A -> A v ~A 1,2 ->I
(4) ~(A v ~A) -> ~A 3 SI "Contra" (sequent intro)
5 (5) ~A A
5 (6) A v ~A 5 vI
(7) ~A -> A v ~A 5,6 ->I
(8) ~(A v ~A) -> ~~A 7 SI "Contra" (sequent intro)
9 (9) ~(A v ~A) A
9 (10) ~A 4,9 ->E
9 (11) ~~A 8,9 ->E
9 (12) _|_ 10,11 ~E
(13) ~~(A v ~A) 9,12 ~I
F.
G. Frege
A typo...
>>>
>>> Assuming X -> Y, one can derive ~Y -> ~X.
>>>
>
> The argument in the system of natural deduction for intuitionistic logic
> (NJ) due to Gentzen.
>
> 1 (1) X -> Y A
> 2 (2) ~Y A
> 3 (3) X A
> 1,3 (4) Y 1,3 ->E <----- corrected
> 1,2,3 (5) _|_ 2,4 ~E
> 1,2 (6) ~X 3,5 ~I
> 1 (7) ~Y -> ~X 2,6 ->I
>
> With other words,
>
> X -> Y |- ~Y -> ~X. (Contra)
>
F.
Frederick Williams
And now you have reason to agree with this bit: "Some of its technical
exposition is flawed;..."!
G. Frege
Williams"@antispamhotmail.co.uk.invalid> wrote:
>
> And now you have reason to agree with this bit: "Some of its technical
> exposition is flawed"!
>
Indeed. B u t Timothy McCarthy also writes:
"...Chapter 5 presents an example of a successful absolute consistency
proof which is “finitistic” in the relevant sense: the authors show that
a formulation of sentential logic is consistent by showing that every
provable formula is a tautology (essentially by induction on the
length of proofs). In general, the exposition in the first five chapters
of the book is clear, concise, and correct, and especially helpful to
the beginner." ~~~~~~~
?!
Now, my point is that Chapter 5 does NOT present an example of a
successful absolute consistency proof, since a crucial definition is
missing. The proof relies on the (alleged) "theorem" 'p -> (~p -> q)'.
But this "theorem" is _not_ derivable in the system as described in the
book.
Nagel & Newman write/claim (p. 50):
"Now, it happens that 'p -> (~p -> q)' (in words: 'if p, then if
not-p, then q') is a theorem in the calculus. (We shall accept
this as a fact, without exhibiting the derivation.)"
Well, actually, it's NOT a fact, since 'p -> (~p -> q)' cannot be
derived in the system /as described/.
Hence imho the missing definition SHOULD be added to the text (or at
least mentioned in a footnote). - It's that simple.
This certainly would contribute to the worth of this book for the
beginner. After all, the missing definition seems to cause troubles to
people who REALLY try to follow (i.e. check) the argument:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
G. Frege
<sma...@SPAMinf.ed.ac.uk> wrote:
>
> I can show ~A <-> ~~~A [...]
>
|- ~A -> ~~~A
1 (1) ~A A
2 (2) ~~A A
1,2 (3) _|_ 1,2 ~E
1 (4) ~~~A 2,3 ~I
(5) ~A -> ~~~A 1,4 ->I
|- ~~~A -> ~A
1 (1) ~~~A A
2 (2) A A
3 (3) ~A A
2,3 (4) _|_ 2,3 ~E
2 (5) ~~A 3,4 ~I
1,2 (6) _|_ 1,5 ~E
1 (7) ~A 2,6 ~I
(8) ~~~A -> ~A 1,7 ->I
Hence we have
~A <-> ~~~A.