Propositional calculus

The following is an example of a very simple inference within the scope of propositional logic:

As propositional logic is not concerned with the structure of propositions beyond the point where they can't be decomposed any more by logical connectives, this inference can be restated replacing those atomic statements with statement letters, which are interpreted as variables representing statements:

The following outlines a standard propositional calculus. Many different formulations exist which are all more or less equivalent, but differ in the details of:

Repeated applications of these rules permits the construction of complex formulas. For example:

(For most logical systems, this is the comparatively "simple" direction of proof)

By the definition of provability, there are no sentences provable other than by being a member of G, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.

Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:

The first five are used for the satisfaction of the five conditions in stage III above, and the last three for proving the deduction theorem.

For the proof we may use the hypothetical syllogism theorem (in the form relevant for this axiomatic system), since it only relies on the two axioms that are already in the above set of eight theorems. The proof then is as follows:

We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. We use several lemmas proven here:

We also use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.

This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.

On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof inference rule which is part of the first version of propositional calculus introduced in this article.

has been demonstrated, then it is also possible to demonstrate the sequence

in fact, the validity of the converse of DT is almost trivial compared to that of DT:

The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, the axiom AND-1,

can be transformed by means of the converse of the deduction theorem into the inference rule

which is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.

The preceding alternative calculus is an example of a Hilbert-style deduction system. In the case of propositional systems the axioms are terms built with logical connectives and the only inference rule is modus ponens. Equational logic as standardly used informally in high school algebra is a different kind of calculus from Hilbert systems. Its theorems are equations and its inference rules express the properties of equality, namely that it is a congruence on terms that admits substitution.

It is possible to generalize the definition of a formal language from a set of finite sequences over a finite basis to include many other sets of mathematical structures, so long as they are built up by finitary means from finite materials. What's more, many of these families of formal structures are especially well-suited for use in logic.