Problems of admissibility and substitution, logical equations and restricted theories of free algebras. (English) Zbl 0691.03012

Logic, methodology and philosophy of science VIII, Proc. 8th Int. Congr., Moscow/USSR 1987, Stud. Logic Found. Math. 126, 121-139 (1989).
[For the entire collection see Zbl 0676.00003.]
For the reviewer, interesting results have been proved in this paper. A positive solution to Friedman’s 40th problem and a negative answer to Kusznetsov’s question are described.
Let \(A_ j\), B be formulas in the language of the intuitionistic propositional calculus H. Let \(p_ 1,...,p_ n\) be all letters occurring in these formulas and \(x_ 1,...,x_ n\) distinct variables. Expressions of the form \[ (1)\quad A_ 1(x_ 1,...,x_ n),...,A_ m(x_ 1,...,x_ n)/B(x_ 1,...,x_ n) \] are called rules of inference. The rule (1) is said to be admissible in H iff for all formulas \(B_ 1,...,B_ n\), \(A_ j(B_ 1,...,B_ n)\in H\), \(j=1,...,m\), imply \(B(B_ 1,...,B_ n)\in H\). The rule (1) is called derivable in H if from \(A_ 1,...,A_ m\) and the set of theorems of H one may derive B with the help of modus ponens. It is clear that derivability implies admissibility. Harrop’s rule (\(\neg p\supset (q\vee r))/(\neg p\supset q)\vee (\neg p\supset r)\) is an example of an admissible rule in H which is not derivable in H. The rule r is said to be a corollary of the rules \(r_ 1,...,r_ n\) in H iff the consequence of r is derivable from the premisses of r with the help of a theorem of H, the rules \(r_ 1,...,r_ n\) and modus ponens. A set B of admissible rules in H is called a basis for H if each admissible rule in H is the corollary of rules \(r_ 1,...,r_ n\) in B. Friedman posed the problem of finding an algorithm which recognizes the admissibility of rules in H. Kuznetsov asked whether H has a finite basis for the admissible rules. There is shown that the problem of admissibility in H for rules has an algorithm and that H has no finite bases. Similar results are obtained for the modal logics S4 and Grz \((=S4+\square (\square (p\to \square p)\to p)\to p)\). In fact, a result for H is obtained from a result for S4.
Reviewer: Y.Komori


03B55 Intermediate logics
03B45 Modal logic (including the logic of norms)
08B20 Free algebras
03B20 Subsystems of classical logic (including intuitionistic logic)


Zbl 0676.00003