zbMATH — the first resource for mathematics

Writing out unifiers for formulas with coefficients in intuitionistic logic. (English) Zbl 1277.03004
Propositional 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).

03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI