×

Unification in intuitionistic logic. (English) Zbl 0930.03009

Summary: We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding the De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

MSC:

03B35 Mechanization of proofs and logical operations
03B20 Subsystems of classical logic (including intuitionistic logic)
06D20 Heyting algebras (lattice-theoretic aspects)
08B30 Injectives, projectives
03B55 Intermediate logics
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Handbook of philosophical logic III pp 225–339– (1986)
[2] Logic Group Preprint Series 161 (1996)
[3] A proof theory for general unification (1991) · Zbl 0746.03011
[4] Semantical investigations in Heyting intuitionistic logic (1981)
[5] Logics containing K4, Part II 50 pp 619–651– (1985) · Zbl 0574.03008
[6] Logics containing K4, Part I 34 pp 31–42– (1974)
[7] The decidability of dependency in intuitionistic propositional logic 60 pp 498–504– (1995)
[8] Logic: from foundations to applications pp 187–213– (1996)
[9] The L. E. J. Brouwer centenary symposium pp 51–64– (1982)
[10] Transactions of the American Mathematical Society 148 pp 549–559– (1970)
[11] Handbook of logic in artificial intelligence and logic programming pp 41–125– (1993)
[12] Journal of Symbolic Computation 7 pp 207–274– (1989)
[13] Contemporary Mathematics 131 pp 645–656– (1992)
[14] Rules of inference with parameters for intuitionistic logic 57 pp 912–923– (1992)
[15] Soviet Math, Dokl 33 pp 428–431– (1986)
[16] On an interpretation of second order quantification in first order intuitionistic propositional logic 57 pp 33–52– (1992)
[17] Journal of Symbolic Computation 7 pp 275–293– (1989)
[18] A sheaf representation and duality for finitely presented Heyting algebras 60 pp 911–939– (1995)
[19] Journal of Logic and Computation 7 pp 733–752– (1997)
[20] Quaderno n. 58/96 (1996)
[21] Mathematical Reports of the Academy of Sciences of Canada XIV pp 240–244– (1992)
[22] Algebra Universalis 3 pp 94–97– (1973)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.