Heyting formal system

Heyting calculus

The name given to three formal systems of constructive logic, proposed by A. Heyting . The first system is Heyting, or intuitionistic, propositional calculus, which is a formalization of the principles of constructive propositional logic; the second is Heyting, or intuitionistic, predicate calculus, which is a formalization of constructive predicate logic; the third is Heyting, or intuitionistic, arithmetic, which is a formalization of the principles of the elementary constructive theory of numbers. These systems were originally conceived as formalizations of parts of intuitionistic logic and mathematics.

The logical Heyting formal systems (propositional calculus and predicate calculus) are obtained from the ordinary versions of the corresponding classical systems with a full set ( $ \wedge , \lor , \supset , \neg , \forall , \exists $) of logical connectives (cf. Logical calculus) by replacing the "non-constructive postulate" (this is usually the law of the excluded middle $ A \lor \neg A $ or the law of double negation (cf. Double negation, law of) $ \neg \neg A \supset A $) by the law of contradiction (cf. Contradiction, law of) $ ( A \wedge \neg A) \supset B $. This is also the method by which Heyting arithmetic is obtained from classical formal arithmetic (cf. Arithmetic, formal). Gentzen (sequential) systems (cf. Gentzen formal system) for Heyting formal systems usually differ from the corresponding classical systems by the following restriction: All sequents (cf. Sequent (in logic)) involved in a derivation are one-succedent.

Heyting formal systems are sound with respect to (different versions of) the constructive understanding of mathematical statements: in particular, formulas that are deducible in these systems are recursively realizable and have a true Gödel interpretation. Heyting formal systems permit intuitionistic methods (cf. Intuitionism) of operation with logical connectives containing a constructive problem: The deducibility of a formula such as $ \exists x A ( x) $( or of the form $ A \lor B $) implies the deducibility of the formula $ A( t) $ for some $ t $( or, respectively, of one of the formulas $ A $ or $ B $). In the case of arithmetic the formulas under consideration must be closed. Markov's rule is also true: The deducibility of a closed formula $ \neg \neg \exists x R ( x) $, where $ R $ is a primitive recursive formula, implies the deducibility of $ R( N) $ for some $ N $.

Heyting arithmetic satisfies the conditions of the Gödel incompleteness theorem. In this system it is not possible to deduce the Markov principle $ \neg \neg \exists x R \supset \exists x R $ for some primitive recursive formula $ R $, even though the principle is true both for the constructive understanding of statements in the sense of Markov–Shanin and in the Gödel interpretation. The incompleteness of logical Heyting formal systems with respect to the realizability interpretation follows from the existence of a non-deducible but realizable propositional formula. The question of the completeness of Heyting propositional calculus relative to the Gödel interpretation remains (1989) an open question.

Any formula that is deducible in a Heyting formal system is also deducible in the corresponding classical system. The converse statement has been disproved by means of an example (the law of the excluded middle); however, there is an interpretation of the classical systems in Heyting formal systems in which the formulas remain unchanged if they are considered up to equivalence in the classical system and which preserves not merely the deducibility of the formulas but also the structure of proofs: Any derivation of a formula $ A $ from a list $ \Gamma $ in the classical system is readily transformed to yield a derivation of the formula $ A ^ {-} $ from the list $ \Gamma ^ {-} $ in the corresponding Heyting formal system. Here $ A ^ {-} $ denotes the result of insertion of $ \neg \neg $ in front of all subformulas of the formula $ A $( in the case of propositional calculus it is sufficient to insert $ \neg \neg $ in front of the formula $ A $ alone). Thus, formulas of the type $ A ^ {-} $ are classically deducible if and only if they are deducible in a Heyting formal system; this is a proof of relative consistency with respect to classical systems. An interpretation of Heyting formal systems in classical systems with preservation of the structure of proofs is not possible, but there is an interpretation of Heyting formal systems in classical systems with an additional connective $ \square $( "deducible" ).

In predicate calculus all connectives are independent. In arithmetic $ \neg $ can be expressed in terms of $ \supset $, while $ \lor $ can be expressed in terms of $ \exists , \wedge , \supset $. One can construct a logical connective in terms of which all other connectives can be expressed, namely, $ ( ( ( p \lor q) \wedge r) \lor ( \neg p \wedge ( r \equiv \forall x \exists y s ( x,y) ))) $. The set-theoretic theory of models for a Heyting formal system involves the use of intensional models, in which the truth of a statement is not determined once and for all, but depends on the "moment of time" considered. Pseudo-Boolean algebras (cf. Pseudo-Boolean algebra) are used in the study of the Heyting propositional calculus.

In modern proof theory Heyting formal systems are mainly studied as parts of systems including stronger principles of constructive mathematics (Markov's principle, realizability) or of intuitionistic mathematics (Brouwer's continuity principle, bar induction, etc.).

References

[1a]	A. Heyting, "Die formalen Regeln der intuitionistischen Logik" Sitzungsber. Deutsch. Akad. Wiss. Phys.-Math. Kl. , 16 : 1 (1930) pp. 42–56; 57–71
[1b]	A. Heyting, "Die formalen Regeln der intuitionistischen Mathematik" Sitzungsber. Deutsch. Akad. Wiss. Phys.-Math. Kl. , 16 : 10–12 (1930) pp. 158–169
[2]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3]	H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963)
[4]	M.C. Fitting, "Intuitionistic logic, model theory and forcing" , North-Holland (1969)

Comments

Pseudo-Boolean algebras are also called Heyting algebras.

The intensional models mentioned above are commonly called Kripke models; they were introduced by S. Kripke [a1] (though a similar idea had been proposed by E.W. Beth [a2]). They can be seen as a special case of sheaf models (cf. [a3], [a4]).

References

[a1]	S.A. Kripke, "Semantic analysis of intuitionistic logic, I" J.N. Crossley (ed.) M.A.E. Dummett (ed.) , Formal systems and recursive functions , North-Holland (1965) pp. 92–130
[a2]	E.W. Beth, "Semantic construction of intuitionistic logic" Med. Kon. Nederl. Akad. Weten. Afd. Letterkunde , 19 (1956) pp. 357–388
[a3]	M.P. Fourman, J.M.E. Hyland, "Sheaf models for analysis" M.P. Fourman (ed.) C.J. Mulvey (ed.) D.S. Scott (ed.) , Applications of sheaves , Lect. notes in math. , 753 , Springer (1979) pp. 280–301
[a4]	M.P. Fourman, D.S. Scott, "Sheaves and logic" M.P. Fourman (ed.) C.J. Mulvey (ed.) D.S. Scott (ed.) , Applications of sheaves , Lect. notes in math. , 753 , Springer (1979) pp. 302–401
[a5]	M.A.E. Dummett, "Elements of intuitionism" , Oxford Univ. Press (1977)
[a6]	A.S. Troelstra, D. van Dalen, "Constructivism in mathematics, an introduction" , 1 , North-Holland (1988)
[a7]	M.J. Beeson, "Foundations of constructive mathematics" , Springer (1985)
[a8]	S.C. Kleene, R.E. Vesley, "The foundations of intuitionistic mathematics: especially in relation to recursive functions" , North-Holland (1965)