Unification in intuitionistic logic.

*(English)*Zbl 0930.03009Summary: 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 |

##### Keywords:

variety of Heyting algebras; finitary unification type; De Morgan law; unitary unification type; finitely presented projective algebras
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.