Structuring Co-constructive Logic for Proofs and Refutations

Logica Universalis 10 (1):67-97 (2016)

James Trafford
University For The Creative Arts
This paper considers a topos-theoretic structure for the interpretation of co-constructive logic for proofs and refutations following Trafford :22–40, 2015). It is notoriously tricky to define a proof-theoretic semantics for logics that adequately represent constructivity over proofs and refutations. By developing abstractions of elementary topoi, we consider an elementary topos as structure for proofs, and complement topos as structure for refutation. In doing so, it is possible to consider a dialogue structure between these topoi, and also control their relation such that classical logic is simulated where proofs and refutations are conclusive.
Keywords Constructive logic  category theory  topos  intuitionistic  co-intuitionistic
Categories (categorize this paper)
DOI 10.1007/s11787-016-0138-z
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 45,305
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Meaning Approached Via Proofs.Dag Prawitz - 2006 - Synthese 148 (3):507-524.
Structure in Mathematics and Logic: A Categorical Perspective.S. Awodey - 1996 - Philosophia Mathematica 4 (3):209-237.
Why Conclusions Should Remain Single.Florian Steinberger - 2011 - Journal of Philosophical Logic 40 (3):333-355.
Constructible Falsity.David Nelson - 1949 - Journal of Symbolic Logic 14 (1):16-26.

View all 23 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Explicit Provability and Constructive Semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
Linearizing Intuitionistic Implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
A Type Theory With Mixed Constructivity And Assignments.James Sasaki - 1997 - Logic Journal of the IGPL 5 (3):67-104.
Axioms for Classical, Intuitionistic, and Paraconsistent Hybrid Logic.Torben Braüner - 2006 - Journal of Logic, Language and Information 15 (3):179-194.
Constructive Sheaf Semantics.Erik Palmgren - 1997 - Mathematical Logic Quarterly 43 (3):321-327.
Strongly Uniform Bounds From Semi-Constructive Proofs.Philipp Gerhardy & Ulrich Kohlenbach - 2006 - Annals of Pure and Applied Logic 141 (1):89-107.


Added to PP index

Total views
11 ( #717,276 of 2,279,934 )

Recent downloads (6 months)
3 ( #399,799 of 2,279,934 )

How can I increase my downloads?


My notes

Sign in to use this feature