On the admissible rules of intuitionistic propositional logic (Q2732279)

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:NEWLINENEWLINENEWLINEAxiom schemes:NEWLINENEWLINE\hskip 17mm \((A\to r\vee s)\vee t\vartriangleright(A\to r)\vee (A\to s)\vee (A\to p_1)\vee\cdots\vee\)NEWLINENEWLINE\hskip 17mm\qquad \(\vee(A\to p_n)\vee t\) for \(A= \bigwedge^n_{i=1} (p_i\to q_i)\),NEWLINENEWLINE\hskip 17mm \(A\vartriangleright B\quad\) where \((A\to B)\) is intuitionistically vaild.NEWLINENEWLINENEWLINERules:NEWLINENEWLINE\hskip 17mm \({C\vartriangleright A, C\vartriangleright B\over C\vartriangleright A\wedge B},\quad {A\vartriangleright B, B\vartriangleright C\over A\vartriangleright C}\).NEWLINENEWLINENEWLINEA 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 NEWLINE\[NEWLINEu\preceq u_1,\dots, u_n\wedge\forall u'\succ u\;(u_i\preceq u'\text{ for some }i\in \{1,\dots, n\}).NEWLINE\]NEWLINE It is shown that the following are equivalent:NEWLINENEWLINENEWLINEa) \(A|\mskip-6mu\sim B\).NEWLINENEWLINENEWLINEb) \(A\vartriangleright B\) is derivable.NEWLINENEWLINENEWLINEc) In every AR-model, \(A\) valid implies \(B\) valid.