Journal of Philosophical Logic 25 (5):559 - 565 (1996)
Let S be a deductive system such that S-derivability (⊦s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and ⊦s, it follows constructively that the K-completeness of ⊦s implies MP(S), a form of Markov's Principle. If ⊦s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if ⊦s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when ⊦s is many-one complete, MP(S) implies the usual Markov's Principle MP. An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implies MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP. These results give extensions of the theorem of Gödel and Kreisel (in ) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Godel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article
|Keywords||intuitionistic logic completeness Markov's principle Kripke and Beth semantics|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
Krivine's Intuitionistic Proof of Classical Completeness.Stefano Berardi & Silvio Valentini - 2004 - Annals of Pure and Applied Logic 129 (1-3):93-106.
Intuitionistic Completeness of First-Order Logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.
Similar books and articles
Kripke Incompleteness of Predicate Extensions of the Modal Logics Axiomatized by a Canonical Formula for a Frame with a Nontrivial Cluster.Tatsuya Shimura - 2000 - Studia Logica 65 (2):237-247.
Combining Derivations and Refutations for Cut-Free Completeness in Bi-Intuitionistic Logic.Linda Postniece - unknown
The Logic of First Order Intuitionistic Type Theory with Weak Sigma- Elimination.M. D. G. Swaen - 1991 - Journal of Symbolic Logic 56 (2):467-483.
A Syntactic Embedding of Predicate Logic Into Second-Order Propositional Logic.Morten H. Sørensen & Paweł Urzyczyn - 2010 - Notre Dame Journal of Formal Logic 51 (4):457-473.
Kripke Semantics, Undecidability and Standard Completeness for Esteva and Godo's Logic MTL∀.Franco Montagna & Hiroakira Ono - 2002 - Studia Logica 71 (2):227-245.
A Free IPC is a Natural Logic: Strong Completeness for Some Intuitionistic Free Logics.Carl J. Posy - 1982 - Topoi 1 (1-2):30-43.
On Some Kripke Complete and Kripke Incomplete Intermediate Predicate Logics.Dmitrij Skvortsov - 1998 - Studia Logica 61 (2):281-292.
A New Semantics for Intuitionistic Predicate Logic.Yuichi Komori - 1986 - Studia Logica 45 (1):9 - 17.
Intuitionistic Completeness for First Order Classical Logic.Stefano Berardi - 1999 - Journal of Symbolic Logic 64 (1):304-312.
Added to index2009-01-28
Total downloads20 ( #245,919 of 2,163,726 )
Recent downloads (6 months)1 ( #348,043 of 2,163,726 )
How can I increase my downloads?