Writing out unifiers for formulas with coefficients in intuitionistic logic.

*(English)*Zbl 1277.03004Propositional formulas using two sorts of propositional letters (variables and coefficients) are considered. It is supposed that every substitution \(\varepsilon\) maps every coefficient \(p\) into itself, i.e., \(\varepsilon(p)=p\). A formula \(\varphi\) is unifiable in a logic \(L\) if there is a substitution \(\varepsilon\) (a unifier) such that \(\varepsilon(\varphi)\in L\). A unifier more general than a given unifier \(\varepsilon\) is defined in a natural way. A set of unifiers BU for a given formula is called complete if for every unifier \(\sigma\) there exists a unifier in BU which is more general than \(\sigma\). The problem of recognizing formulas unifiable in the intuitionistic logic Int was solved by the author in [J. Symb. Log. 57, No. 3, 912–923 (1992; Zbl 0788.03007)]. Now this result is extended to the algorithm writing out a finite complete set of unifiers for every unifiable formula. A similar result for the formulas without coefficients was obtained by S. Ghilardi in [J. Symb. Log. 64, No. 2, 859–880 (1999; Zbl 0930.03009)]. The author shows how to transfer the main result to the logic of the weak principle of excluded middle (obtained by adding the axiom \(\neg x\lor\neg\neg x\) to Int).

Reviewer: Valery Plisko (Moskva)

##### MSC:

03B20 | Subsystems of classical logic (including intuitionistic logic) |