zbMATH — the first resource for mathematics

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)