Inference Rules of G4ip (LJT)

A, Γ A Axiom  false, Γ G false-L

(A being atomic)

\begin{matrix}B, C, Γ G \\ B&C, Γ G \end{matrix} &-L  \begin{matrix}Γ B & Γ C \\ Γ B&C \end{matrix} &-R
\begin{matrix}B, Γ G & C, Γ G \\ B∨C, Γ G \end{matrix} ∨-L \begin{matrix}Γ B \\ Γ B∨C \end{matrix} ∨-R_{1} \begin{matrix}Γ C \\ Γ B∨C \end{matrix} ∨-R_{2}
\begin{matrix}B, A, Γ G \\ A->B, A, Γ G \end{matrix} ->-L_{1}  \begin{matrix}B, Γ C \\ Γ B->C \end{matrix} ->-R

(A being atomic)

\begin{matrix}C->(D->B)Γ G \\ (C&D)->B, Γ G \end{matrix} ->-L_{2}
\begin{matrix}C->B, D->B, Γ G \\ (C∨D)->BΓ G \end{matrix} ->-L_{3}
\begin{matrix}D->B, Γ C->D & B, Γ G \\ (C->D)->BΓ G \end{matrix} ->-L_{4}
B<->C is defined as B->C&C->B

Figure 1: Inference rules for G4ip; see for example [Dyckhoff, 1992].

[Dyckhoff, 1992] Dyckhoff, R. Contraction-Free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic, 57(3):795–807.