Perhaps the simplest formal system for zeroeth order logic is the Nicod system. As its language it uses the subset of our language for zeroeth order logic consisting of those lists where \({ ⊼ }\), whose truth table is
\[ \begin{array}{cc|c} P & Q & ( P ⊼ Q ) \cr \hline f & f & t \cr f & t & t \cr t & f & t \cr t & t & f \end{array} \]
is the only logical operator appearing. There’s no loss of expressiveness involved in this restriction since we can write \({ ( P ∧ Q ) }\) as \({ [ ( P ⊼ Q ) ⊼ ( P ⊼ Q ) ] }\), \({ ( P ∨ Q ) }\) as \({ [ ( P ⊼ P ) ⊼ ( Q ⊼ Q ) ] }\), and \({ ( ¬ P ) }\) as \({ ( P ⊼ P ) }\). All the other operators were expressed in terms of \({ ∧ }\), \({ ∨ }\) and \({ ¬ }\) so they can be expressed by first converting the expression into one involving those three operators and then converting them as above.
The Nicod system has a single axiom, \[ ( ( p ⊼ ( q ⊼ r ) ) ⊼ ( ( s ⊼ ( s ⊼ s ) ) ⊼ ( ( u ⊼ q ) ⊼ ( ( p ⊼ u ) ⊼ ( p ⊼ u ) ) ) ) ) . \] There is also only one rule of inference, that from two statements of the form \({ P }\) and \({ [ P ⊼ ( Q ⊼ R ) ] }\) we can derive the statement \({ R }\).
We can use truth table method to show that, no matter which of the 32 possible ways of assigning truth values to the variables \({ p }\), \({ q }\), \({ r }\), \({ s }\), and \({ u }\) we choose, the statement \[ ( ( p ⊼ ( q ⊼ r ) ) ⊼ ( ( s ⊼ ( s ⊼ s ) ) ⊼ ( ( u ⊼ q ) ⊼ ( ( p ⊼ u ) ⊼ ( p ⊼ u ) ) ) ) ) . \] will always evaluate to true, i.e. that it is a tautology.
It is also possible to show that the rule of inference of the system has the property that if applied to tautologies it leads to a tautology. This follows from the truth table \[ \begin{array}{ccc|c|c} P & Q & R & ( Q ⊼ R ) & [ P ⊼ ( Q ⊼ R ) ] \cr \hline f & f & f & t & t \cr f & f & t & t & t \cr f & t & f & t & t \cr f & t & t & f & t \cr t & f & f & t & f \cr t & f & t & t & f \cr t & t & f & t & f \cr t & t & t & f & t \end{array} \]
There is only one case in which both \({ P }\) and \({ [ P ⊼ ( Q ⊼ R ) ] }\) are true and in that case \({ R }\) is also true.
It follows that any theorem must be a tautology, since we start from an axiom which is true in any interpretation which assigns to the operator ⊼ the meaning described by its truth table given earlier and the rules of inference can only produce true statements from true statements. In other words any interpretation which assigns to the operator ⊼ the meaning described by the truth table above and assigns any truth values whatever to its variables is a sound interpretation of the Nicod system. We say that a system is “sound” if the intended interpretation or interpretations are sound. The Nicod system is sound in this
We could add a second rule of inference, the rule of substitution discussed earlier. More explicitly, from any statement we can derive another statement by replacing each occurrence of one of the variables with an expression. In fact we can do this for each variable in the statement. Any proof which uses the rule of substitution can be converted into one in the original system by repeating the proof of the statement into which we want to substitute, but making all of the substitutions everywhere in that proof. So the system with this extra rule has the same set of theorems as the original system. Rules like this are called derived rules of inference. Strictly speaking, whenever we us a derived rule of inference the result is a semi-formal proof rather than a formal proof.
An alternative formal system for the propositional calculus is due to Łukasiewicz. It uses the subset of our general language for zeroeth order logic where the only logical operators are \({ ¬ }\) and \({ ⊃ }\). There is no loss of expressiveness since \({ ( P ∧ Q ) }\) has the same meaning as \({ \{ ¬ [ P ⊃ ( ¬ Q ) ] \} }\) and \({ ( P ∨ Q ) }\) has the same meaning as \({ [ ( ¬ P ) ⊃ Q ] }\).
The axioms are \[ [ p ⊃ ( q ⊃ p ) ] , \] \[ \{ [ p ⊃ ( q ⊃ r ) ] ⊃ [ ( p ⊃ q ) ⊃ ( p ⊃ r ) ] \} , \] and \[ \{ [ ( ¬ p ) ⊃ ( ¬ q ) ] ⊃ ( q ⊃ p ) \} . \] The rules of inference are the rule of substitution and a rule, known by the curious name of “modus ponens” which allows us to derive \({ Q }\) from \({ P }\) and \({ ( P ⊃ Q ) }\).
The system as introduced by Łukasiewicz differs in one respect from that described above. Łukasiewicz used prefix notation in place of infix notation. He was, in fact, the first person to introduce prefix notation, and to notice that it allows one to dispense with parentheses. Łukasiewicz also used \({ N }\) and \({ C }\) in place of \({ \neg }\) and \({ ⊃ }\).
A direct proof of the soundness Łukasiewicz’s system is slightly more complicated than a proof the soundness of Nicod’s, because the system is larger and more complicated, but it can be done by the same method, using truth tables.
Because Łukasiewicz’s system contains the \({ ¬ }\) operator we can also discuss consistency, which is the requirement that for any statement \({ P }\) at most one of \({ P }\) and \({ ( ¬ P ) }\) is a theorem. In other words the system is free from contradictions. Unlike soundness, consistency is purely a property of the system, not the system and its interpretation. A small bit of interpretation is smuggled in because it’s only the interpretation which tells us that the pair \({ P }\) and \({ ( ¬ P ) }\) form a contradiction but this is really the only aspect of the interpretation which is needed to discuss consistency. If you believe that \({ P }\) and \({ ( ¬ P ) }\) can’t simultaneously be true then consistency follows from soundness because if they can’t both be true then they can’t both be tautologies and every theorem is a tautology.
For humans, proofs in Łukasiewicz’s system are easier to read, write and check than in Nicod’s system. This doesn’t mean they are easy. Here is a proof of the theorem \({ ( p ⊃ p ) }\), which we can easily check is a tautology by considering the two possible values of \({ p }\):
\[ \begin{array}{l@{\quad}l} 1 & ( p ⊃ ( q ⊃ p ) ) \cr 2 & ( ( p ⊃ ( q ⊃ r ) ) ⊃ ( ( p ⊃ q ) ⊃ ( p ⊃ r ) ) ) \cr 3 & ( p ⊃ ( ( q ⊃ p ) ⊃ p ) ) \cr 4 & ( ( p ⊃ ( ( q ⊃ p ) ⊃ p ) ) ⊃ ( ( p ⊃ ( q ⊃ p ) ) ⊃ ( p ⊃ p ) ) ) \cr 5 & ( p ⊃ ( q ⊃ p ) ) ⊃ ( p ⊃ p ) ) \cr 6 & ( p ⊃ p ) \end{array} \]
Statements 1 and 2 are axioms. Statement 3 follows from 1 by substituting \({ ( q ⊃ p ) }\) for \({ q }\). Statement 4 follows from 2 by substituting \({ ( q ⊃ p ) }\) for \({ q }\) and \({ p }\) for \({ r }\). Statement 5 follows from 3 and 4 by modus ponens. Statement 6 follows from 1 and 5 by modus ponens. More interesting theorems have, as you might expect, even longer proofs.
Proving the completeness of Łukasiewicz’s system is easier than proving that of Nicod’s, but I still won’t do it.