zbMATH — the first resource for mathematics

On the admissible rules of intuitionistic propositional logic. (English) Zbl 0986.03013
For \(A\), \(B\) propositional formulas, \(A|\mskip-6mu\sim B\) means that for each substitution \(\sigma\), \(\sigma(A)\) intuitionistically valid implies \(\sigma(B)\) intuitionistically valid. The author introduces the expression \(A\vartriangleright B\) for propositional formulas \(A\), \(B\), and defines the following system of derivations for such expressions:
Axiom schemes:
\((A\to r\vee s)\vee t\vartriangleright(A\to r)\vee (A\to s)\vee (A\to p_1)\vee\cdots\vee\)
    \(\vee(A\to p_n)\vee t\) for \(A= \bigwedge^n_{i=1} (p_i\to q_i)\),
\(A\vartriangleright B\quad\) where \((A\to B)\) is intuitionistically vaild.
\({C\vartriangleright A, C\vartriangleright B\over C\vartriangleright A\wedge B},\quad {A\vartriangleright B, B\vartriangleright C\over A\vartriangleright C}\).
A Kripke model is called AR-model, if for every finite set \(\{u_1,\dots, u_n\}\) of nodes, there is a node \(u\) such that \[ u\preceq u_1,\dots, u_n\wedge\forall u'\succ u\;(u_i\preceq u'\text{ for some }i\in \{1,\dots, n\}). \] It is shown that the following are equivalent:
a) \(A|\mskip-6mu\sim B\).
b) \(A\vartriangleright B\) is derivable.
c) In every AR-model, \(A\) valid implies \(B\) valid.
Reviewer: A.Tauts (Tallinn)

03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI
[1] Admissibility of Logical Inference Rules (1997) · Zbl 0872.03002
[2] Journal of Soviet Mathematics 6 (1976)
[3] Concerning formulas of the types A B C, A (Ex)B(x) in intuitionistic formal systems 25 pp 27– (1960)
[4] Constructivism in Mathmatics I (1988)
[5] Logics containing KA, part I 34 pp 31– (1974)
[6] Mathematics of the USSR, Sbornik 31 pp 314– (1977)
[7] Logics containing KA, part II 50 pp 619– (1985)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.