## 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

### MSC:

 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