Structuring Co-constructive Logic for Proofs and Refutations
Logica Universalis 10 (1):67-97 (2016)
Abstract
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.Author's Profile
DOI
10.1007/s11787-016-0138-z
Links
PhilArchive
External links
(no proxy)
Setup an account with your affiliations in order to access resources via your University's proxy server
Through your library
- Sign in / register and customize your OpenURL resolver
- Configure custom resolver
My notes
Similar books and articles
Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
On some peculiar aspects of the constructive theory of point-free spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.Linda Postniece - unknown
Topos based semantic for constructive logic with strong negation.Barbara Klunder & B. Klunder - 1992 - Mathematical Logic Quarterly 38 (1):509-519.
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.
Replacement versus collection and related topics in constructive Zermelo–Fraenkel set theory.Michael Rathjen - 2005 - Annals of Pure and Applied Logic 136 (1-2):156-174.
On the computational content of intuitionistic propositional proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
Strongly uniform bounds from semi-constructive proofs.Philipp Gerhardy & Ulrich Kohlenbach - 2006 - Annals of Pure and Applied Logic 141 (1):89-107.
Analytics
Added to PP
2016-02-06
Downloads
18 (#614,279)
6 months
1 (#448,551)
2016-02-06
Downloads
18 (#614,279)
6 months
1 (#448,551)
Historical graph of downloads
Author's Profile
Citations of this work
Is ‘No’ a Force-Indicator? Yes, Sooner or Later!Fabien Schang & James Trafford - 2017 - Logica Universalis 11 (2):225-251.
References found in this work
From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s.Paolo Mancosu (ed.) - 1997 - Oxford, England: Oxford University Press.
From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920s.Paolo Mancosu (ed.) - 1997 - Oxford, England: Oxford University Press USA.
Structure in mathematics and logic: A categorical perspective.S. Awodey - 1996 - Philosophia Mathematica 4 (3):209-237.
