-
Views
-
Cite
Cite
Ruan V B Carvalho, Anjolina G de Oliveira, Ruy J G B de Queiroz, Propositional intuitionistic multiple-conclusion calculus via proof graphs, Logic Journal of the IGPL, Volume 27, Issue 1, February 2019, Pages 33–59, https://doi.org/10.1093/jigpal/jzy017
Close - Share Icon Share
Abstract
How to verify if a classical proof is also intuitionistic? Gentzen’s natural deduction (ND) only requires no occurrence of the law of the excluded middle or the elimination of double negation rule in an intuitionistic derivation. His sequent calculus achieves the same result by restricting the number of formulas on the right-hand side to at most one, which removes its multiple-conclusion feature that is important for the calculus’ symmetry. There are approaches today that take this into account and present solutions for multiple-conclusion sequent calculi for intuitionistic logic, but while giving us some useful insights on what constitutes an intuitionistic system, they inherit the bureaucracy from Gentzen’s formalism. Here we separate intuitionistic logic from classical in non-sequential derivations by adopting a geometric perspective. We propose an intuitionistic version for n-graphs, a system defined by de Oliveira (2001, PhD Thesis, Universidade Federal de Pernambuco, Recife, Brazil) as a symmetric multiple-conclusion natural deduction for propositional classical logic.
