zbMATH — the first resource for mathematics

Solvability of logical equations in the modal system Grz and in intuitionistic logic. (Russian) Zbl 0729.03014
By a logical equation we understand an expression of the form \(A(x_ i,p_ j)\equiv_{\lambda}B(x_ i,p_ j)\), where A, B are formulas, \(x_ i\) are variables, \(p_ j\) are metavariables (or parameters), \(\lambda\) is some logic. A tuple \(\psi_ i\) is called a solution of this equation in the logic \(\lambda\) iff \(A(\psi_ i,p_ j)\) is equivalent to \(B(\psi_ i,p_ j)\) in the logic \(\lambda\). A particular case of logical equations is the so-called substitution problem: to recognize for any formula \(A(x_ i,p_ j)\) whether there is a tuple \(\psi_ i\) of formulas such that \(A(\psi_ i,p_ j)\in \lambda\). In this paper, an algorithm is found, which recognizes solvability of logical equations in the modal system Grz and in Int, and constructs some solution for solvable equations. This solves the substitution problem for Grz and Int.
Reviewer: V.V.Rybakov

03B45 Modal logic (including the logic of norms)
03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: EuDML