A graphical deep inference system for intuitionistic logic

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)73-114
Number of pages42
JournalLogique et Analyse
Volume245
DOIs
Publication statusPublished - Jan 1 2019

Fingerprint

Intuitionistic Logic
Inference
Sequent Calculus
Existential Graphs
Graph
Logical Constant
Gentzen
Sound
Propositional Logic
Algebra

Keywords

  • Charles Peirce
  • Deep inference
  • Graphical logic
  • Intuitionistic logic

ASJC Scopus subject areas

  • Philosophy

Cite this

A graphical deep inference system for intuitionistic logic. / Minghui, Ma; Pietarinen, ahti Veikko.

In: Logique et Analyse, Vol. 245, 01.01.2019, p. 73-114.

Research output: Contribution to journalArticle

@article{fa7f9582aa5244549a7163f762742cf1,
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’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}",
year = "2019",
month = "1",
day = "1",
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 Belge de Recherche de Logique)",

}

TY - JOUR

T1 - A graphical deep inference system for intuitionistic logic

AU - Minghui, Ma

AU - Pietarinen, ahti Veikko

PY - 2019/1/1

Y1 - 2019/1/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 - http://www.scopus.com/inward/record.url?scp=85066258215&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85066258215&partnerID=8YFLogxK

U2 - 10.2143/LEA.245.0.3285706

DO - 10.2143/LEA.245.0.3285706

M3 - Article

AN - SCOPUS:85066258215

VL - 245

SP - 73

EP - 114

JO - Logique et Analyse

JF - Logique et Analyse

SN - 0024-5836

ER -