Section 1.4 - An Axiom System for the Propositional Calculus

Oh crap! Axiomatic theory is something. The foundation of theory, here, is syntactic, that is based entirely on the symbols and the arrangement of those symbols in an expression. It seemed okay at first, but they the axioms of propositional calculus hit, and smoke started coming out of my ears. I mean, do we really need to prove "if B then B"?

Concepts and Vocabulary

  • Formal Theory: A thing these four parts
    1. Expression: Sequences produced from a countable set of symbols.
    2. Well-Formed Formulas (wfs): A subset of the possible expressions\ldots the special ones.
    3. Axioms: A subset of expressions\ldots the really special ones.
    4. Rules of Inference: Mappings from one or more expressions to one expression.
  • Axiomatic Theory: A formal theory where there is a mechanism to determine if an expression is an axiom.
  • Follow From: A statement to connect the input variables, of a rule of inference, to the output.
  • Direct Consequence of: Same as follow from.
  • Proof: A sequence (those sequences again) of well formed formulas where each member is either an axiom or a direct consequence of preceding expressions.
  • Theorem: The last expressions in a proof.
  • Decidable: A theory defined so there is a mechanism to determine if a theorem can be proven.
  • Undecidable: The opposite of decidable.
  • Consequence: Connecting word to say an expression is the theorem of some proof that can include hypotheses. $\Gamma\vdash\mathscr{C}$, $\mathscr{C}$ is the theorem to a proof where the elements of the set $\Gamma$ are allowed in addition to the normal axioms.
  • Proof (or deduction) of $\mathscr{C}$ From $\Gamma$: Same as consequence.
  • Hypotheses of Premises: Members of $\Gamma$ above.
  • Primitive Connectives: $\Rightarrow$, $\neg$
  • Statement Letters: Variables
  • Ideas from the footnote on page 29.
    • Object Language: The collection of well formed formulas used in a formal theory.
    • Metalanguage: The language used to make arguments about an object language.
    • Metaproof: A proof in metalanguage.
    • Metatheorems: Theorems resulting from a metaproof...Oh, that's what a proposition is!!!!
    • Metamathemtaics: The study of object and mathematical languages.
  • Consistent: An axiomatic system that cannot prove something true and false at the same time.
  • Absolutely Consistent: A theory where not all well formed formulas are theorems.

Formal Axiomatic Theory L

  1. Symbols: $\neg$, $\Rightarrow$, (, ), and the letters $A_i$ for integer values of $i$.
  2. Well Formed Formulas:
    1. All statement letters.
    2. $(\neg B)$ and $(B\Rightarrow C)$, when $B$ and $C$ are well formed formulas.
  3. Axioms:
    • (A1) $(\mathscr{B}\Rightarrow(\mathscr{C}\Rightarrow\mathscr{B}))$
    • (A2) $((\mathscr{B}\Rightarrow(\mathscr{C}\Rightarrow\mathscr{D}))\Rightarrow((\mathscr{B}\Rightarrow\mathscr{C})\Rightarrow(\mathscr{B}\Rightarrow\mathscr{D})))$
    • (A3) $(((\neg\mathscr{C})\Rightarrow(\neg\mathscr{B}))\Rightarrow(((\neg\mathscr{C})\Rightarrow\mathscr{B})\Rightarrow\mathscr{C}))$
  4. Rules of Inference: Modus ponens; $\mathscr{B},(\mathscr{B}\Rightarrow\mathscr{C})\vdash\mathscr{C}$.


  • Proposition 1.8 Ugh...$\vdash_L\mathscr{B}\Rightarrow\mathscr{B}$ for all wfs $\mathscr{B}$.
  • Proposition 1.9 (Deduction Theorem) If $\Gamma,\mathscr{B}\vdash\mathscr{C}$, then $\Gamma\vdash\mathscr{B}\Rightarrow\mathscr{C}$.
  • Proposition 1.10
    1. $\mathscr{B}\Rightarrow\mathscr{C},\mathscr{C}\Rightarrow\mathscr{D}\vdash\mathscr{B}\Rightarrow\mathscr{D}$
    2. $\mathscr{B}\Rightarrow(\mathscr{C}\Rightarrow\mathscr{D}),\mathscr{C}\vdash\mathscr{B}\Rightarrow\mathscr{D}$
  • Proposition 1.11 For any wfs $\mathscr{B}$ and $\mathscr{C}$, the following wfs are theorems of $L$.
    1. $\neg\neg\mathscr{B}\Rightarrow\mathscr{B}$
    2. $\mathscr{B}\Rightarrow\neg\neg\mathscr{B}$
    3. $\neg\mathscr{B}\Rightarrow(\mathscr{B}\Rightarrow\mathscr{C})$
    4. $(\neg\mathscr{C}\Rightarrow\neg\mathscr{B})\Rightarrow(\mathscr{B}\Rightarrow\mathscr{C})$
    5. $\mathscr{B}\Rightarrow\mathscr{C})\Rightarrow(\neg\mathscr{C}\Rightarrow\neg\mathscr{B})$
    6. $\mathscr{B}\Rightarrow(\neg\mathscr{C}\Rightarrow\neg(\mathscr{B}\Rightarrow\mathscr{C}))$
    7. $(\mathscr{B}\Rightarrow\mathscr{C})\Rightarrow((\neg\mathscr{B}\Rightarrow\mathscr{C})\Rightarrow\mathscr{C})$
  • Proposition 1.12 Every theorem in L is a tautology.
  • Proposition 1.13 $B'_1,\ldots,B'_k\vdash\mathscr{B}'$
  • Proposition 1.14 (Completeness Theorem) All tautologies are theorems.
  • Proposition 1.15 Expressions involving $\neg,\Rightarrow,\land,\vee,$ and $\Leftrightarrow$ are tautologies if their $\neg,\Rightarrow$ counterpart is a theorem in L.
  • Proposition 1.16 The system L is consistent.
< Previous