G4. Propositional Logic
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 zerothorder logic (in contrast to firstorder 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.
 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 \()\)
 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)\).
 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.
 Definition^{1}: \(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.
 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.

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