A Graphical Deep Inference System for Intuitionistic Logic

Ma Minghui; Ahti Veikko Pietarinen

doi:10.2143/LEA.245.0.3285706

A Graphical Deep Inference System for Intuitionistic Logic

Ma Minghui
, Ahti Veikko Pietarinen

Academy of Chinese, History, Religion and Philosophy

Research output: Contribution to journal › Journal article › peer-review

22 Citations (Scopus)

Abstract

A graphical approach to intuitionistic propositional logic is presented. The system GrIn is a deep inference system and it 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. Moreover, the system GrIn is shown to be equivalent to the Gentzen sequent calculus G3ip via translations between intuitionistic graphs and intuitionistic formulas. We also discuss the intuitionistic interpretation of logical constants proposed by this graphical approach.

Original language	English
Pages (from-to)	73-114
Number of pages	42
Journal	Logique et Analyse
Volume	245
DOIs	https://doi.org/10.2143/LEA.245.0.3285706
Publication status	Published - Jan 2019

User-Defined Keywords

Charles Peirce
Deep inference
Graphical logic
Intuitionistic logic

Access to Document

10.2143/LEA.245.0.3285706

Cite this

@article{11f21faafdb8404eb5c8a44166926bd3,

title = "A Graphical Deep Inference System for Intuitionistic Logic",

abstract = "A graphical approach to intuitionistic propositional logic is presented. The system GrIn is a deep inference system and it is formulated in terms of Peirce{\textquoteright}s existential graphs. GrIn is shown to be sound and complete with respect to the class of all Heyting algebras. Moreover, the system GrIn is shown to be equivalent to the Gentzen sequent calculus G3ip via translations between intuitionistic graphs and intuitionistic formulas. We also discuss the intuitionistic interpretation of logical constants proposed by this graphical approach.",

keywords = "Charles Peirce, Deep inference, Graphical logic, Intuitionistic logic",

author = "Ma Minghui and Pietarinen, \{Ahti Veikko\}",

note = "Funding Information: The work of the first author is supported by the Chinese National Foundation for Social Sciences and Humanities (grant no. 16CZX049). The work of the second author is supported by the Academy of Finland (project 1270335), the Estonian Research Council (project PUT 1305) (Principle Investigator A.-V. Pietarinen), the Social Policy Grant of Nazarbayev University (2018–2019) and the Russian Academic Excellence Project “5-100”. We thank the reviewers of the present journal for helpful comments, suggestions and criticism that led to the revision of Theorem 1, among several other things. Publisher Copyright: {\textcopyright} 2019 by Peeters Publishers. All rights reserved.",

year = "2019",

month = jan,

doi = "10.2143/LEA.245.0.3285706",

language = "English",

volume = "245",

pages = "73--114",

journal = "Logique et Analyse",

issn = "0024-5836",

publisher = "Nationaal Centrum voor Navorsingen in de Logica (Centre National de Recherches de Logique)",

}

TY - JOUR

T1 - A Graphical Deep Inference System for Intuitionistic Logic

AU - Minghui, Ma

AU - Pietarinen, Ahti Veikko

N1 - Funding Information: The work of the first author is supported by the Chinese National Foundation for Social Sciences and Humanities (grant no. 16CZX049). The work of the second author is supported by the Academy of Finland (project 1270335), the Estonian Research Council (project PUT 1305) (Principle Investigator A.-V. Pietarinen), the Social Policy Grant of Nazarbayev University (2018–2019) and the Russian Academic Excellence Project “5-100”. We thank the reviewers of the present journal for helpful comments, suggestions and criticism that led to the revision of Theorem 1, among several other things. Publisher Copyright: © 2019 by Peeters Publishers. All rights reserved.

PY - 2019/1

Y1 - 2019/1

N2 - A graphical approach to intuitionistic propositional logic is presented. The system GrIn is a deep inference system and it 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. Moreover, the system GrIn is shown to be equivalent to the Gentzen sequent calculus G3ip via translations between intuitionistic graphs and intuitionistic formulas. We also discuss the intuitionistic interpretation of logical constants proposed by this graphical approach.

AB - A graphical approach to intuitionistic propositional logic is presented. The system GrIn is a deep inference system and it 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. Moreover, the system GrIn is shown to be equivalent to the Gentzen sequent calculus G3ip via translations between intuitionistic graphs and intuitionistic formulas. We also discuss the intuitionistic interpretation of logical constants proposed by this graphical approach.

KW - Charles Peirce

KW - Deep inference

KW - Graphical logic

KW - Intuitionistic logic

UR - https://www.scopus.com/pages/publications/85066258215

U2 - 10.2143/LEA.245.0.3285706

DO - 10.2143/LEA.245.0.3285706

M3 - Journal article

AN - SCOPUS:85066258215

SN - 0024-5836

VL - 245

SP - 73

EP - 114

JO - Logique et Analyse

JF - Logique et Analyse

ER -

A Graphical Deep Inference System for Intuitionistic Logic

Abstract

User-Defined Keywords

Access to Document

Other files and links

Fingerprint

Cite this