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.