Propositional Calculus - Equivalence To Equational Logics

Equivalence To Equational Logics

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.

Classical propositional calculus as described above is equivalent to Boolean algebra, while intuitionistic propositional calculus is equivalent to Heyting algebra. The equivalence is shown by translation in each direction of the theorems of the respective systems. Theorems of classical or intuitionistic propositional calculus are translated as equations of Boolean or Heyting algebra respectively. Conversely theorems of Boolean or Heyting algebra are translated as theorems of classical or propositional calculus respectively, for which is a standard abbreviation. In the case of Boolean algebra can also be translated as, but this translation is incorrect intuitionistically.

In both Boolean and Heyting algebra, inequality can be used in place of equality. The equality is expressible as a pair of inequalities and . Conversely the inequality is expressible as the equality, or as . The significance of inequality for Hilbert-style systems is that it corresponds to the latter's deduction or entailment symbol . An entailment

is translated in the inequality version of the algebraic framework as

Conversely the algebraic inequality is translated as the entailment

.

The difference between implication and inequality or entailment or is that the former is internal to the logic while the latter is external. Internal implication between two terms is another term of the same kind. Entailment as external implication between two terms expresses a metatruth outside the language of the logic, and is considered part of the metalanguage. Even when the logic under study is intuitionistic, entailment is ordinarily understood classically as two-valued: either the left side entails, or is less-or-equal to, the right side, or it is not.

Similar but more complex translations to and from algebraic logics are possible for natural deduction systems as described above and for the sequent calculus. The entailments of the latter can be interpreted as two-valued, but a more insightful interpretation is as a set, the elements of which can be understood as abstract proofs organized as the morphisms of a category. In this interpretation the cut rule of the sequent calculus corresponds to composition in the category. Boolean and Heyting algebras enter this picture as special categories having at most one morphism per homset, i.e., one proof per entailment, corresponding to the idea that existence of proofs is all that matters: any proof will do and there is no point in distinguishing them.