- Submit
-
Browse
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- More
Switch to: References
Citations of:
On the interpretation of intuitionistic number theory
Journal of Symbolic Logic 10 (4):109-124 (1945)
Add citations
You must login to add citations.
|
|
|
An extension of intuitionism to empirical discourse, a project most seriously taken up by Dummett and Tennant, requires an empirical negation whose strength lies somewhere between classical negation (‘It is unwarranted that. . . ’) and intuitionistic negation (‘It is refutable that. . . ’). I put forward one plausible candidate that compares favorably to some others that have been propounded in the literature. A tableau calculus is presented and shown to be strongly complete. |
|
|
According to Weyl, “‘inexhaustibility’ is essential to the infinite”. However, he distinguishes two kinds of inexhaustible, or merely potential, domains: those that are “extensionally determinate” and those that are not. This article clarifies Weyl's distinction and explains its enduring logical and philosophical significance. The distinction sheds lights on the contemporary debate about potentialism, which in turn affords a deeper understanding of Weyl. |
|
|
We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...) |
|
|
A variant of realizability for Heyting arithmetic which validates Church’s thesis with uniqueness condition, but not the general form of Church’s thesis, was introduced by Lifschitz (Proc Am Math Soc 73:101–106, 1979). A Lifschitz counterpart to Kleene’s realizability for functions (in Baire space) was developed by van Oosten (J Symb Log 55:805–821, 1990). In that paper he also extended Lifschitz’ realizability to second order arithmetic. The objective here is to extend it to full intuitionistic Zermelo–Fraenkel set theory, IZF. The machinery (...) |
|
|
This paper is a survey of results concerning the disjunction property, Halldén-completeness, and other related properties of intermediate prepositional logics and normal modal logics containing S4. |
|
|
|
|
|
MICHAEL DUMMETT, Elements of intuitionism. With the assistance of Robert Minio. Oxford: Oxford University Press, 1977. xii + 466 pp. No price stated. |
|
|
The purpose of this paper is to present a paraconsistent formal system and a corresponding intended interpretation according to which true contradictions are not tolerated. Contradictions are, instead, epistemically understood as conflicting evidence, where evidence for a proposition A is understood as reasons for believing that A is true. The paper defines a paraconsistent and paracomplete natural deduction system, called the Basic Logic of Evidence, and extends it to the Logic of Evidence and Truth. The latter is a logic of (...) |
|
|
The standard presentation of topological spaces relies heavily on (naïve) set theory: a topology consists of a set of subsets of a set (of points). And many of the high-level tools of set theory are required to achieve just the basic results about topological spaces. Concentrating on the mathematical structures, category theory offers the possibility to look synthetically at the structure of continuous transformations between topological spaces addressing specifically how the fundamental notions of point and open come about. As a (...) |
|
|
We present a general notion of realizability encompassing both standard Kleene style realizability over partial combinatory algebras and Kleene style realizability over more general structures, including all partial cartesian closed categories. We shown how the general notion of realizability can be used to get models of dependent predicate logic, thus obtaining as a corollary (the known result) that the category Equ of equilogical spaces models dependent predicate logic. Moreover, we characterize when the general notion of realizability gives rise to a (...) |
|
|
We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how (...) |
|
|
|
|
|
|
|
|
We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t: F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a (...) |
|
|
In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) |
|
|
|
|
|
A semantics for quantified modal logic is presented that is based on Kleene's notion of realizability. This semantics generalizes Flagg's 1985 construction of a model of a modal version of Church's Thesis and first-order arithmetic. While the bulk of the paper is devoted to developing the details of the semantics, to illustrate the scope of this approach, we show that the construction produces (i) a model of a modal version of Church's Thesis and a variant of a modal set theory (...) |
|
|
We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm {B}$, $\Delta (\mathrm {B})$, and $\Sigma (\mathrm {B})$ of formulas of modal arithmetic and study basic properties of them. Then, we prove several implications between the properties. In particular, among other things, we prove that for any consistent recursively enumerable extension T of $\mathbf {PA}(\mathbf {K})$ with $T \nvdash \Box \bot $, the $\Sigma (\mathrm {B})$ -disjunction property, the (...) |
|
|
Realizability notions in mathematical logic have a long history, which can be traced back to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations of intuitionistic logic. Kleene’s initial realizability laid the ground for more sophisticated notions such as Kreisel’s modified realizability and various modern approaches. In this context, our work aligns with the lineage of realizability strategies that emphasize the accumulation, rather than the propagation of precise witnesses. In this paper, we introduce a new notion (...) |
|
|
Games, Norms, and Reasons: Logic at the Crossroads provides an overview of modern logic focusing on its relationships with other disciplines, including new interfaces with rational choice theory, epistemology, game theory and informatics. This book continues a series called "Logic at the Crossroads" whose title reflects a view that the deep insights from the classical phase of mathematical logic can form a harmonious mixture with a new, more ambitious research agenda of understanding and enhancing human reasoning and intelligent interaction. The (...) |
|
|
This volume is dedicated to Leo Esakia's contributions to the theory of modal and intuitionistic systems. Consisting of 10 chapters, written by leading experts, this volume discusses Esakia’s original contributions and consequent developments that have helped to shape duality theory for modal and intuitionistic logics and to utilize it to obtain some major results in the area. Beginning with a chapter which explores Esakia duality for S4-algebras, the volume goes on to explore Esakia duality for Heyting algebras and its generalizations (...) |
|
|
|
|
|
|
|
|
A variant of the notion of symmetric constructive realizability is introduced where the information about the symmetric constructive truth or falsity of an arithmetical formula is expressed by a single natural number. The methods of transformations of such a realization to the realizations of known kinds and those of reverse transformations are given. The formal arithmetical system based on such a realizability is investigated. |
|
|
When Kleene extended his recursive realizability interpretation from intuitionistic arithmetic to analysis, he was forced to use more than recursive functions to interpret sequences and conditional constructions. In fact, he used what classically appears to be the full continuum. We describe here a generalization to higher type of Kleene's realizability, one case of which, -realizability, uses general recursive functions throughout, both to realize theorems and to interpret choice sequences. -realizability validates a version of the bar theorem and the usual continuity (...) |
|
|
We define a variant of the standard Kripke semantics for intuitionistic logic, motivated by the connection between constructive logic and the Medvedev lattice. We show that while the new semantics is still complete, it gives a simple and direct correspondence between Kripke models and algebraic structures such as factors of the Medvedev lattice. |
|
|
Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever ϕϕ is provable, there is a formula χχ such that ϕ∧χϕ∧χ is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has (...) |
|
|
Truth-maker analyses construe truth as existence of proof, a well-known example being that offered by Wittgenstein in theTractatus. The paper subsumes the intuitionistic view of truth as existence of proof under the general truth-maker scheme. Two generic constraints on truth-maker analysis are noted and positioned with respect to the writings of Michael Dummett and theTractatus. Examination of the writings of Brouwer, Heyting and Weyl indicates the specific notions of truth-maker and existence that are at issue in the intuitionistic truth-maker analysis, (...) |
|
|
|
|
|
§1. The origins of recursion theory. In dedicating a book to Steve Kleene, I referred to him as the person who made recursion theory into a theory. Recursion theory was begun by Kleene's teacher at Princeton, Alonzo Church, who first defined the class of recursive functions; first maintained that this class was the class of computable functions ; and first used this fact to solve negatively some classical problems on the existence of algorithms. However, it was Kleene who, in his (...) |
|
|
ABSTRACTAIan Rumfitt's new book presents a distinctive and intriguing philosophy of logic, one that ultimately settles on classical logic as the uniquely correct one–or at least rebuts some prominent arguments against classical logic. The purpose of this note is to evaluate Rumfitt's perspective by focusing on some themes that have occupied me for some time: the role and importance of model theory and, in particular, the place of counter-arguments in establishing invalidity, higher-order logic, and the logical pluralism/relativism articulated in my (...) |
|
|
|
|
|
This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a (...) |
|
|
It is proved in this paper that the predicate logic of each complete constructive arithmetic theory T having the existential property is Π1T-complete. In this connection, the techniques of a uniform partial truth definition for intuitionistic arithmetic theories is used. The main theorem is applied to the characterization of the predicate logic corresponding to certain variant of the notion of realizable predicate formula. Namely, it is shown that the set of irrefutable predicate formulas is recursively isomorphic to the complement of (...) |
|
|
The study of propositional realizability logic was initiated in the 50th of the last century. Some interesting results were obtained in the 60-70th. but many important problems in this area are still open. Now interest to these problems from new generation of researchers is observed. This survey contains an exposition of the results on propositional realizability logic and corresponding techniques. Thus reading this paper can be the start point in exploring and development of constructive logic. |
|
|
A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs and from the viewpoint of (...) |
|
|
This little gem is stated unbilled and proved in the last two lines of §2 of the short note Kleene [1938]. In modern notation, with all the hypotheses stated explicitly and in a strong form, it reads as follows:Second Recursion Theorem. Fix a set V ⊆ ℕ, and suppose that for each natural number n ϵ ℕ = {0, 1, 2, …}, φn: ℕ1+n ⇀ V is a recursive partial function of arguments with values in V so that the standard (...) |
|
|
Realizabilities are powerful tools for establishing consistency and independence results for theories based on intuitionistic logic. Troelstra discovered principles ECT 0 and GC 1 which precisely characterize formal number and function realizability for intuitionistic arithmetic and analysis, respectively. Building on Troelstra's results and using his methods, we introduce the notions of Church domain and domain of continuity in order to demonstrate the optimality of “almost negativity” in ECT 0 and GC 1 ; strengthen “double negation shift” DNS 0 to DNS (...) |
|
|
|
|
|
|
|
|
We describe a variety of sets internal to models of intuitionistic set theory that (1) manifest some of the crucial behaviors of potentially infinite sets as described in the foundational literature going back to Aristotle, and (2) provide models for systems of predicative arithmetic. We close with a brief discussion of Church’s Thesis for predicative arithmetic. |
|
|
Straightforwardly and strictly intuitionistic inferences show that the Brouwer– Heyting–Kolmogorov interpretation, in the presence of a formulation of the recognition principle, entails the validity of the Law of Testability: that the form ¬ f V ¬¬ f is valid. Therefore, the BHK and recognition, as described here, are inconsistent with the axioms both of intuitionistic mathematics and of Markovian constructivism. This finding also implies that, if the BHK and recognition are suitably formulated, then Brouwer’s original weak counterexample reasoning was fallacious. (...) |
|
|
We define here a notion of internal copy and of weak internal copy of a category. We will then determine some families of categories having an internal copy or a weak internal copy. We will consider categories of definable classes of first-order theories and we will see that the notion of internal copy is related to the notion of numerical existence property. |
|
|
We use formal semantic analysis based on new constructions to study abstract realizability, introduced by Läuchli in 1970, and expose its algebraic content. We claim realizability so conceived generates semantics-based intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning.Well-known semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the completeness proofs for these semantics (...) |
|
|
In the literature, predicativism is connected not only with the Vicious Circle Principle but also with the idea that certain totalities are inherently potential. To explain the connection between these two aspects of predicativism, we explore some approaches to predicativity within the modal framework for potentiality developed in Linnebo (2013) and Linnebo and Shapiro (2019). This puts predicativism into a more general framework and helps to sharpen some of its key theses. |
|
|
The notion of potential infinity dominated in mathematical thinking about infinity from Aristotle until Cantor. The coherence and philosophical importance of the notion are defended. Particular attention is paid to the question of whether potential infinity is compatible with classical logic or requires a weaker logic, perhaps intuitionistic. |
|
|
We give natural examples of factors of the Muchnik lattice which capture intuitionistic propositional logic , arising from the concepts of lowness, 1-genericity, hyperimmune-freeness and computable traceability. This provides a purely computational semantics for IPC. |
|
|
Skvortsova showed that there is a factor of the Medvedev lattice which captures intuitionistic propositional logic. However, her factor is unnatural in the sense that it is constructed in an ad hoc manner. We present a more natural example of such a factor. We also show that the theory of every non-trivial factor of the Medvedev lattice is contained in Jankov’s logic, the deductive closure of IPC plus the weak law of the excluded middle ¬p∨¬¬p\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} (...) |
|
|
Let \ be a class of formulas. We say that a theory T in classical logic has the \-disjunction property if for any \ sentences \ and \, either \ or \ whenever \. First, we characterize the \-disjunction property in terms of the notion of partial conservativity. Secondly, we prove a model theoretic characterization result for \-disjunction property. Thirdly, we investigate relationships between partial disjunction properties and several other properties of theories containing Peano arithmetic. Finally, we investigate unprovability of (...) |
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-5ff6c685cb-rskd8 uwo