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.

  1. Alphabet:
    • 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 \()\)
  2. Grammar:
    • 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)\).
  3. 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.
  4. Axioms:
    • \((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.

  1. 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. ↩