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:
- $(p\vee p)\supset p$,
- $p\supset (p\vee q)$,
- $(p\vee q)\supset (q\vee p)$, and
- $(p\supset q)\supset ((p\vee r)\supset(q\vee r))$.