A new technique for proving realisability and consistency theorems using finite paraconsistent models of cut‐free logic

Mathematical Logic Quarterly 52 (6):540-554 (2006)
  Copy   BIBTEX


A new technique for proving realisability results is presented, and is illustrated in detail for the simple case of arithmetic minus induction. CL is a Gentzen formulation of classical logic. CPQ is CL minus the Cut Rule. The basic proof theory and model theory of CPQ and CL is developed. For the semantics presented CPQ is a paraconsistent logic, i.e. there are non-trivial CPQ models in which some sentences are both true and false. Two systems of arithmetic minus induction are introduced, CL-A and CPQ-A based on CL and CPQ, respectively. The realisability theorem for CPQ-A is proved: It is shown constructively that to each theorem A of CPQ-A there is a formula A *, a so-called “realised disjunctive form of A ”, such that variables bound by essentially existential quantifiers in A * can be written as recursive functions of free variables and variables bound by essentially universal quantifiers. Realisability is then applied to prove the consistency of CL-A, making use of certain finite non-trivial inconsistent models of CPQ-A



    Upload a copy of this work     Papers currently archived: 92,347

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Symmetric and dual paraconsistent logics.Norihiro Kamide & Heinrich Wansing - 2010 - Logic and Logical Philosophy 19 (1-2):7-30.
Real Analysis in Paraconsistent Logic.Maarten McKubre-Jordens & Zach Weber - 2012 - Journal of Philosophical Logic 41 (5):901-922.
The basic constructive logic for absolute consistency.José M. Méndez & Gemma Robles - 2009 - Journal of Logic, Language and Information 18 (2):199-216.
A Paraconsistentist Approach to Chisholm's Paradox.Marcelo Esteban Coniglio & Newton Marques Peron - 2009 - Principia: An International Journal of Epistemology 13 (3):299-326.
Inconsistent models of arithmetic part I: Finite models. [REVIEW]Graham Priest - 1997 - Journal of Philosophical Logic 26 (2):223-235.
The basic constructive logic for negation-consistency.Gemma Robles - 2008 - Journal of Logic, Language and Information 17 (2):161-181.
Minimally inconsistent LP.Graham Priest - 1991 - Studia Logica 50 (2):321 - 331.
Measuring coherence using LP-models.Carlos A. OLLER - 2004 - Journal of Applied Logic 2 (4):451-455.
Paraconsistency Everywhere.Greg Restall - 2002 - Notre Dame Journal of Formal Logic 43 (3):147-156.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
The basic constructive logic for a weak sense of consistency.Gemma Robles & José M. Méndez - 2008 - Journal of Logic, Language and Information 17 (1):89-107.


Added to PP

21 (#742,032)

6 months
8 (#370,917)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations