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 (...) would also work for extensions of IZF with large set axioms. In addition to separating Church’s thesis with uniqueness condition from its general form in intuitionistic set theory, we also obtain several interesting corollaries. The interpretation repudiates a weak form of countable choice, ACω,ω, asserting that a countable family of inhabited sets of natural numbers has a choice function. ACω,ω is validated by ordinary Kleene realizability and is of course provable in ZF. On the other hand, a pivotal consequence of ACω,ω, namely that the sets of Cauchy reals and Dedekind reals are isomorphic, remains valid in this interpretation. Another interesting aspect of this realizability is that it validates the lesser limited principle of omniscience. (shrink)

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.

The period in the foundations of mathematics that started in 1879 with the publication of Frege's Begriffsschrift and ended in 1931 with Gödel's Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I can reasonably be called the classical period. It saw the development of three major foundational programmes: the logicism of Frege, Russell and Whitehead, the intuitionism of Brouwer, and Hilbert's formalist and proof-theoretic programme. In this period, there were also lively exchanges between the various schools culminating in (...) the famous Hilbert-Brouwer controversy in the 1920s. -/- The purpose of this anthology is to review the programmes in the foundations of mathematics from the classical period and to assess their possible relevance for contemporary philosophy of mathematics. What can we say, in retrospect, about the various foundational programmes of the classical period and the disputes that took place between them? To what extent do the classical programmes of logicism, intuitionism and formalism represent options that are still alive today? These questions are addressed in this volume by leading mathematical logicians and philosophers of mathematics. (shrink)

In the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of large subsystems of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that provide computational procedures (...) only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility. (shrink)

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.

Skvortsova showed that there is a factor of the Medvedev lattice which captures intuitionistic propositional logic (IPC). 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 $${\neg p \vee \neg \neg (...) p}$$. This answers a question by Sorbi and Terwijn. (shrink)

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 (...) proof-theoretic semantics. (shrink)

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 (...) byproduct of this, one may look at the different approaches to topology from an external perspective and compare them in a unified way. Technically, the category of sober topological spaces can be seen as consisting of (co)algebraic structures in the exact completion of the elementary category of sets and relations. Moreover, the same abstract construction of taking the exact completion, when applied to the category of topological spaces and continuous functions produces an extension of it which is cartesian closed. In other words, there is one general mathematical construction that, when applied to a very elementary category, generates the category of topological spaces and continuous functions, and when applied to that category produces a very suitable category where to deal with all sorts functions spaces. Yet, via such free constructions it is possible to give a new meaning to Marshall Stone’s dictum: “always topologize” as the category of sets and relations is the most natural way to give structure to logic and the category of topological spaces and continuous functions is obtained from it by a good mix of free – i.e. syntactic – constructions. (shrink)

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 (...) own recent *Varieties of logic*. (shrink)

There is an ambiguity in the concept of deductive validity that went unnoticed until the middle of the twentieth century. Sometimes an inference rule is called valid because its conclusion is a theorem whenever its premises are. But often something different is meant: The rule's conclusion follows from its premises even in the presence of other assumptions. In many logical environments, these two definitions pick out the same rules. But other environments are context-sensitive, and in these environments the second notion (...) is stronger. Sorting out this ambiguity has led to profound mathematical investigations with applications in complexity theory and computer science. The origins of this ambiguity and the history of its resolution deserve philosophical attention, because our understanding of logic stands to benefit from their details. I am eager to examine together with you, Crito, whether this argument will appear in any way different to me in my present circumstances, or whether it remains the same, whet... (shrink)

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.

We put together several observations on constructive negation. First, Russell anticipated intuitionistic logic by clearly distinguishing propositional principles implying the law of the excluded middle from remaining valid principles. He stated what was later called Peirce’s law. This is important in connection with the method used later by Heyting for developing his axiomatization of intuitionistic logic. Second, a work by Dragalin and his students provides easy embeddings of classical arithmetic and analysis into intuitionistic negationless systems. In the last section, we (...) present in some detail a stepwise construction of negation which essentially concluded the formation of the logical base of the Russian constructivist school. Markov’s own proof of Markov’s principle (different from later proofs by Friedman and Dragalin) is described. (shrink)