We discussed in the previous section the ability to derive new tautologies from others using substitution and Modus Ponens.
We now aim to identify a group of axioms from which all tautologies can be derived.
The first is known as "Simplification". In words, this is "if it is cloudy, then if it is a Tuesday it is also cloudy."
\(\theta \rightarrow (\gamma \rightarrow \theta )\)
The second is called "Frege".
\((\alpha \rightarrow (\beta \rightarrow \gamma ))\rightarrow ((\alpha \rightarrow \beta )\rightarrow(\alpha \rightarrow \gamma ))\)
The third is "Transposition". Consider the statement "If there are no clouds in the sky, it is not raining." If this is true then it is also true that "If it is raining there are clouds in the sky."
\((\neg \theta \rightarrow \neg \gamma )\rightarrow (\gamma \rightarrow \theta )\)
These axioms are independent. That is, if you take one away, you cannot derive it from the others.
These axioms are also effective. One could define all true formulae as axioms, however this is not effective.
Soundness implies that all theories are true.
\(T\vdash A \Rightarrow T\vDash A\)
These axioms and the deduction rule are sound. We know that the axioms are tautologies, and we know that the inference rule is valid.
As the axioms are sound, the theories are consistent. That is, it is not possible for both \(\theta\) and \(\neg \theta\) to be theories.
Completeness implies that all true formulae are theories.
\(T\vDash A \Rightarrow T\vdash A\)
A definition is a conservative extension of the language. A definition statement, for example that a new symbol \(Z\) is always evaluated as false allows us to make additional statements, but it does not allow us to make additional statements in the original language.
An axiom allows us to generate additional statements in the original language, a definition does not.