On the intuitionistic equivalential calculus.
Robert E. Tax · Notre Dame Journal of Formal Logic · 1973
CCpqCCqpEpq.We define IE to be the equivalential fragment of ICE.We now construct a Gentzen system GCE corresponding to ICE: A sequent of GCE is to be any expression of the form P l9 . .., P n -* Q, where P l9 . .., P n , and Q are wffs of ICE, and n -0.An axiom of GCE is to be any sequent of the form P -> P.There are nine rules of inference, as follows (where Γ and Δ represent arbitrary sequences, possibly empty, of wffs of ICE):