Before moving on to other topics, it’s worth taking a look at a less trivial example of a formal system - one that’s capable of making somewhat interesting statements (when interpreted). This system also serves as a foundation on which other more complicated and powerful formal system are based. This is propositional logic - also known as: propositional calculus, sentential logic, sentential calculus, statement logic, and sometimes zeroth-order logic (in contrast to first-order predicate logic).
As we now know, a formal system consists of four parts. Below is the alphabet (along with the standard interpretation), grammar, transformation rules, and axioms of propositional logic.
- sentential variables: They are the letters, \(p\), \(q\), \(r\), etc. They may have “sentences” substituted for them (see ‘Rule of Substitution’ below).
- sentential connectives:
- \(\lnot\): short for not
- \(\lor\): short for or
- \(\supset\): short for if… then…, or implies
- \(\land\): short for and
- punctuation: \((\), and \()\)
- Each sentential variable counts as a formula
- If the letter \(S\) stands for a formula: \(\lnot (S)\) is a formula
- If the letters \(S_1\) and \(S_2\) stand for formulas, the following are also formulas:
- \((S_1) \lor (S_2)\).
- \((S_1) \supset (S_2)\).
- \((S_1) \land (S_2)\).
- Transformation rules:
- Rule of Substitution (for sentential variables): From a formula containing sentential variables, it is permissible to derive another formula by uniformly substituting formulas for the variables.
- Rule of Detachment (or Modus Ponens): From two formulas having the form \(S_1\) and \(S_1 \supset S_2\), the formula \(S_2\) and be derived.
- Definition1: \(S_1 \supset S_2\) is defined as \(\lnot S_1 \lor S_2\). Either may be substituted for the other within any formula to derive a new formula.
- Definition: \(S_1 \land S_2\) is defined as \(\lnot (\lnot S_1 \lor \lnot S_2)\). Either may be substituted for the other within any formula to derive a new formula.
- \((p \lor p) \supset p\).
- \(p \supset (p \lor q)\).
- \((p \lor q) \supset (q \lor p)\).
- \((p \supset q) \supset ((r \lor p) \supset (r \lor q))\).
One interesting property of propositional logic is that it can derive all tautologies. A tautology is a formula that is always true, regardless of the truth value substituted for any of the sentential variables. \(p \lor \lnot p\) is a tautology since it is true regardless of whether \(p\) is true or false.
This was not part of the formulation with Nagel and Newman’s “Godel’s Proof”, but I found it to be necessary after trying to derive ‘p ⊃ (~p ⊃ q)’, which they claimed was a theorem. After much frustration, I found the following (long) thread which agreed that their formulation was insufficient and suggested this as a minimal remedy. ↩