The actual question

I am currently reading Gödel's Proof by Nagel and Newman. Chapter V deals with the formalization and consistency of a simple system of formal logic.

On page 50, after giving the rules of the system (see below), the authors state, without giving a proof, that

$p \supset (\thicksim p \supset q)$ is a theorem in the calculus

It seems like this should be relatively easy to prove, but I can't see how. I feel I may be missing something important because there are I see no rules or axioms concerning negation (or conjunction for that matter), which there probably should be.

Can anyone give the complete proof ?

Rules of the formal calculus defined in the book

I call formula any syntaxically valid string, and theorem any formula that can be derived from the axioms. The book does not always clearly make this distinction, so the rules I give here are somewhat rephrased.

The rules of the system are essentially defined as follows:

  • Letters, and $\thicksim$, $\vee$, $\cdot$, $\supset$, $($, $)$ are the only allowed symbols in formulas;
  • If $S$ and $S'$ are formulas, then $\thicksim (S)$, $(S) \vee (S')$, $(S) \cdot (S')$, and $(S) \supset (S')$ are formulas;

  • Rule of substitution: in a theorem, one can uniformly replace a variable with a formula and obtain another theorem;

  • Rule of detachement: if $S$ and $S\supset S'$ are theorems, $S'$ is a theorem;

  • Axioms: the following formulas are theorems:

    1. $(p\vee p)\supset p$,
    2. $p\supset (p\vee q)$,
    3. $(p\vee q)\supset (q\vee p)$, and
    4. $(p\supset q)\supset ((p\vee r)\supset(q\vee r))$.
  • $\begingroup$ See Alfred North Whitehead & Bertrand Russell, Principia Mathematica to *56 (2nd ed - 1927); page 12 for the def : $p \supset q \overset{def}{=} \lnot p \lor q$, and page 104 for the proof of *2.21 : $\lnot p \supset (p \supset q)$, by subst of $\lnot p$ in place of $p$ into Ax.2 [$p \supset (p \lor q)$] followed by *2.24 : $p \supset (\lnot p \supset q)$. $\endgroup$ – Mauro ALLEGRANZA Nov 5 '15 at 7:27

Their system seems to be missing a crucial link between '$\supset$', '$\vee$' and '$\sim$'. If they gave an additional axiom $(\sim\!p \vee q) \supset (p \supset q)$, or defined $\supset$ as $(\sim\!p \vee q)$, then the formula would be derivable. See this thread discussing the omission. (The first quoted assertion there is false, though: of course $p \supset p$ can be derived: it follows from axioms 2. (substituting $p$ for $q$) and 1., then using detachment.)

| cite | improve this answer | |

Nagel and Newman almost surely discuss the propositional calculus of Principia Mathematica (without one of the axioms of the book which years after the book got written got found to come as derivable from the other axioms). In the system of Principia Mathematica and using the notational scheme you did, ⊃ doesn't actually exist as a primitive concept, but rather (p) ⊃ (q) abbreviates ~(p) ∨ (q).

I will switch to Polish notation in the following. I will also use $\vdash$ instead of saying something like "is a theorem".

The rules of the system remain the same, except

  1. Only lower case letters, N, A, K, and C come as allowed in formulas.
  2. If $\alpha$ and $\beta$ qualify as formulas, so do N$\alpha$, A$\alpha$$\beta$, K$\alpha$$\beta$, C$\alpha$$\beta$.
  3. The rule of detachment correspondingly becomes if $\vdash$$\alpha$, $\vdash$AN$\alpha$$\beta$, then $\vdash$$\beta$.

The axioms also now correspondingly become:

  1. ANAppp.
  2. ANpApq.
  3. ANApqAqp.
  4. ANANpqANAprAqr.

Here's a parenthesized Polish notation proof generated by Prover9 with 'P' standing for $\vdash$:

% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.01) seconds.
% Length of proof is 13.
% Level of proof is 5.
% Maximum clause weight is 15.
% Given clauses 10.

1 P(A(N(x),A(N(N(x)),y))) # label(non_clause) # label(goal).  [goal].
2 -P(A(N(x),y)) | -P(x) | P(y).  [assumption].
3 P(A(N(A(x,x)),x)).  [assumption].
4 P(A(N(x),A(x,y))).  [assumption].
5 P(A(N(A(x,y)),A(y,x))).  [assumption].
6 P(A(N(A(N(x),y)),A(N(A(x,z)),A(y,z)))).  [assumption].
7 -P(A(N(c3),A(N(N(c3)),c4))).  [deny(1)].
8 P(A(N(A(x,y)),A(A(x,z),y))).  [hyper(2,a,6,a,b,4,a)].
9 P(A(N(A(A(x,x),y)),A(x,y))).  [hyper(2,a,6,a,b,3,a)].
10 P(A(A(N(x),y),A(x,z))).  [hyper(2,a,8,a,b,4,a)].
11 P(A(A(x,y),A(N(x),z))).  [hyper(2,a,5,a,b,10,a)].
12 P(A(x,A(N(x),y))).  [hyper(2,a,9,a,b,11,a)].
13 $F.  [resolve(12,a,7,a)].

============================== end of proof ==========================
| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.