A Graphical Deep Inference System for Intuitionistic Logic

Ahti-Veikko Pietarinen, Minghui Ma


A graphical approach to intuitionistic propositional logic is presented.
The system GrIn is a deep inference system and is formulated in terms
of Peirce’s existential graphs. GrIn is shown to be sound and complete with respect to the class of all Heyting algebras. The system GrIn is shown to be equivalent to the Gentzen sequent calculus G3ip via translations between intuitionistic graphs and intuitionistic formulæ. We also discuss the intuitionistic interpretation of logical constants proposed by the graphical approach.


  • There are currently no refbacks.