×

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.
Rules:
\({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)

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.