Ishihara's problem of decidable variables asks which class of decidable propositional variables is sufficient to warrant classical theorems in intuitionistic logic. We present several refinements to the class proposed by Ishii for this problem, which also allows the class to cover Glivenko's logic. We also treat the extension of the problem to minimal logic, suggesting a couple of new classes.

Since the publication of the Remarks on the Foundations of Mathematics, Wittgenstein’s interpreters have endeavored to reconcile his general constructivist/anti-realist attitude towards mathematics with his confessed anti-revisionary philosophy. In this article, the author revisits the issue and presents a solution. The basic idea consists in exploring the fact that the so-called “non-constructive results” could be interpreted so that they do not appear non-constructive at all. The author substantiates this solution by showing how the translation of mathematical results, given by the (...) possibility of translation between logics, can be seen as a tool for partially implementing the solution Wittgenstein had in mind. (shrink)

ABSTRACT Theories of sets such as Zermelo Fraenkel set theory are usually presented as the combination of two distinct kinds of principles: logical and set-theoretic principles. The set-theoretic principles are imposed ‘on top’ of first-order logic. This is in agreement with a traditional view of logic as universally applicable and topic neutral. Such a view of logic has been rejected by the intuitionists, on the ground that quantification over infinite domains requires the use of intuitionistic rather than classical logic. In (...) the following, I consider constructive set theories, which use intuitionistic rather than classical logic, and argue that they manifest a distinctive interdependence or an entanglement between sets and logic. In fact, Martin-Löf type theory identifies fundamental logical and set-theoretic notions. Remarkably, one of the motivations for this identification is the thought that classical quantification over infinite domains is problematic, while intuitionistic quantification is not. The approach to quantification adopted in Martin-Löf’s type theory is subtly interconnected with its predicativity. I conclude by recalling key aspects of an approach to predicativity inspired by Poincaré, which focuses on the issue of correct quantification over infinite domains and relate it back to Martin-Löf type theory. (shrink)

Consistency with the formal Church’s thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin From sets and types to topology and analysis: practicable foundations for constructive mathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, (...) completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory à la Martin-Löf, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Löf’s type theory, called \, where mTT can be easily interpreted. Then to show the consistency of \ with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints \ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment \ we interpret consists of first order intensional Martin-Löf’s type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors -rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of \ correctly. In particular the universe of \ is modelled by means of \-fixpoints following a technique due first to Aczel and used by Feferman and Beeson. (shrink)

This is a survey of the concept of continuity. Efforts to explicate continuity have produced a plurality of philosophical conceptions of continuity that have provably distinct expressions within contemporary mathematics. I claim that there is a divide between the conceptions that treat the whole continuum as prior to its parts, and those conceptions that treat the parts of the continuum as prior to the whole. Along this divide, a tension emerges between those conceptions that favor philosophical idealizations of continuity and (...) those that are more readily available for mathematico-scientific use. (shrink)

I proffer a success argument for classical logical consequence. I articulate in what sense that notion of consequence should be regarded as the privileged notion for metaphysical inquiry aimed at uncovering the fundamental nature of the world. Classical logic breeds necessitism. I use necessitism to produce problems for both ontological naturalism and atheism.

This paper contains five observations concerning the intended meaning of the intuitionistic logical constants: (1) if the explanations of this meaning are to be based on a non-decidable concept, that concept should not be that of `proof"; (2) Kreisel"s explanations using extra clauses can be significantly simplified; (3) the impredicativity of the definition of → can be easily and safely ameliorated; (4) the definition of → in terms of `proofs from premises" results in a loss of the inductive character of (...) the definitions of ∨ and ∃ and (5) the same occurs with the definition of ∀ in terms of `proofs with free variables". (shrink)

Computationalism holds that our grasp of notions like ‘computable function’ can be used to account for our putative ability to refer to the standard model of arithmetic. Tennenbaum's Theorem has been repeatedly invoked in service of this claim. I will argue that not only do the relevant class of arguments fail, but that the result itself is most naturally understood as having the opposite of a reference-fixing effect — i.e., rather than securing the determinacy of number-theoretic reference, Tennenbaum's Theorem points (...) towards a sense in which portions of our computational vocabulary should be regarded as model-relative. (shrink)

In classical logic, the proposition expressed by a sentence is construed as a set of possible worlds, capturing the informative content of the sentence. However, sentences in natural language are not only used to provide information, but also to request information. Thus, natural language semantics requires a logical framework whose notion of meaning does not only embody informative content, but also inquisitive content. This paper develops the algebraic foundations for such a framework. We argue that propositions, in order to embody (...) both informative and inquisitive content in a satisfactory way, should be defined as non-empty, downward closed sets of possibilities, where each possibility in turn is a set of possible worlds. We define a natural entailment order over such propositions, capturing when one proposition is at least as informative and inquisitive as another, and we show that this entailment order gives rise to a complete Heyting algebra, with meet, join, and relative pseudo-complement operators. Just as in classical logic, these semantic operators are then associated with the logical constants in a first-order language. We explore the logical properties of the resulting system and discuss its significance for natural language semantics. We show that the system essentially coincides with the simplest and most well-understood existing implementation of inquisitive semantics, and that its treatment of disjunction and existentials also concurs with recent work in alternative semantics. Thus, our algebraic considerations do not lead to a wholly new treatment of the logical constants, but rather provide more solid foundations for some of the existing proposals. (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.

Toisaalta ennennäkemätön äärettömien joukko-opillisten menetelmien hyödyntäminen sekä toisaalta epäilyt niiden hyväksyttävyydestä ja halu oikeuttaa niiden käyttö ovat ratkaisevasti muovanneet vuosisatamme matematiikkaa ja logiikkaa. Tämän kehityksen vaikutus nykyajan filosofiaan on myös ollut valtaisa; merkittävää osaa siitä ei voi edes ymmärtää tuntematta sen yhteyttä tähän matematiikan ja logiikan vallankumoukseen. Lähestymistapoja, jotka tavalla tai toisella hyväksyvät äärettömän matematiikan ja perinteisten logiikan sääntöjen (erityisesti kolmannen poissuljetun lain) soveltamisen myös sen piirissä, on tullut tavaksi kutsua klassiseksi matematiikaksi ja logiikaksi erotuksena nämä hylkäävistä radikaaleista intuitionistisista ja (...) konstruktivistisista opeista. (shrink)

This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. -/- Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in its entirety, but not half-accepted. Therefore, our beliefs about reality, bivalence, choice and consistency should all be aligned.

If mathematics is regarded as a science, then the philosophy of mathematics can be regarded as a branch of the philosophy of science, next to disciplines such as the philosophy of physics and the philosophy of biology. However, because of its subject matter, the philosophy of mathematics occupies a special place in the philosophy of science. Whereas the natural sciences investigate entities that are located in space and time, it is not at all obvious that this is also the case (...) with respect to the objects that are studied in mathematics. In addition to that, the methods of investigation of mathematics differ markedly from the methods of investigation in the natural sciences. Whereas the latter acquire general knowledge using inductive methods, mathematical knowledge appears to be acquired in a different way, namely, by deduction from basic principles. The status of mathematical knowledge also appears to differ from the status of knowledge in the natural sciences. The theories of the natural sciences appear to be less certain and more open to revision than mathematical theories. For these reasons mathematics poses problems of a quite distinctive kind for philosophy. Therefore philosophers have accorded special attention to ontological and epistemological questions concerning mathematics. (shrink)

This paper presents a defense of Epistemic Arithmetic as used for a formalization of intuitionistic arithmetic and of certain informal mathematical principles. First, objections by Allen Hazen and Craig Smorynski against Epistemic Arithmetic are discussed and found wanting. Second, positive support is given for the research program by showing that Epistemic Arithmetic can give interesting formulations of Church's Thesis.

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules,ex falso quodlibetor double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, (...) including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward. (shrink)

This paper discusses the general problem of translation functions between logics, given in axiomatic form, and in particular, the problem of determining when two such logics are "synonymous" or "translationally equivalent." We discuss a proposed formal definition of translational equivalence, show why it is reasonable, and also discuss its relation to earlier definitions in the literature. We also give a simple criterion for showing that two modal logics are not translationally equivalent, and apply this to well-known examples. Some philosophical morals (...) are drawn concerning the possibility of having two logical systems that are "empirically distinct" but are both translationally equivalent to a common logic. (shrink)

To what extent can constructive mathematics based on intuitionistc logic recover the mathematics needed for spacetime physics? Certain aspects of this important question are examined, both technical and philosophical. On the technical side, order, connectivity, and extremization properties of the continuum are reviewed, and attention is called to certain striking results concerning causal structure in General Relativity Theory, in particular the singularity theorems of Hawking and Penrose. As they stand, these results appear to elude constructivization. On the philosophical side, it (...) is argued that any mentalist-based radical constructivism suffers from a kind of neo-Kantian apriorism. It would be at best a lucky accident if objective spacetime structure mirrored mentalist mathematics. the latter would seem implicitly committed to a Leibnizian relationist view of spacetime, but is it doubtful if implementation of such a view would overcome the objection. As a result, an anti-realist view of physics seems forced on the radical constructivist. (shrink)

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.

The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using (...) appropriate embeddings ; it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding LK into LJ brings to the fore the latter's defects for these `deconstructive purposes'. (shrink)

It is shown constructively that a strongly extensional function of bounded variation on an interval is regulated, in a sequential sense that is classically equivalent to the usual one.

The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

In this paper we give axiom systems for classical and intuitionistic hybrid logic. Our axiom systems can be extended with additional rules corresponding to conditions on the accessibility relation expressed by so-called geometric theories. In the classical case other axiomatisations than ours can be found in the literature but in the intuitionistic case no axiomatisations have been published. We consider plain intuitionistic hybrid logic as well as a hybridized version of the constructive and paraconsistent logic N4.

is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.

N. Kamide introduced a pair of classical and constructive logics, each with a peculiar type of negation: its double negation behaves as classical and intuitionistic negation, respectively. A consequence of this is that the systems prove contradictions but are non-trivial. The present paper aims at giving insights into this phenomenon by investigating subsystems of Kamide’s logics, with a focus on a system in which the double negation behaves as the negation of minimal logic. We establish the negation inconsistency of the (...) system and embeddability of contradictions from other systems. In addition, we attempt at an informational interpretation of the negation using the dimathematical framework of H. Wansing. (shrink)

Sortal concepts are at the center of certain logical discussions and have played a significant role in solutions to particular problems in philosophy. Apart from logic and philosophy, the study of sortal concepts has found its place in specific fields of psychology, such as the theory of infant cognitive development and the theory of human perception. In this monograph, different formal logics for sortal concepts and sortal-related logical notions are characterized. Most of these logics are intensional in nature and possess, (...) in addition, a bidimensional character. That is, they simultaneously represent two different logical dimensions. In most cases, the dimensions are those of time and natural necessity, and, in other cases, those of time and epistemic necessity. Another feature of the logics in question concerns second-order quantification over sortal concepts, a logical notion that is also represented in the logics. Some of the logics adopt a constant domain interpretation, others a varying domain interpretation of such quantification. Two of the above bidimensional logics are philosophically grounded on predication sortalism, that is, on the philosophical view that predication necessarily requires sortal concepts. Another bidimensional logic constitutes a logic for complex sortal predicates. These three sorts of logics are among the important novelties of this work since logics with similar features have not been developed up to now, and they might be instrumental for the solution of philosophically significant problems regarding sortal predicates. The book assumes a modern variant of conceptualism as a philosophical background. For this reason, the approach to sortal predicates is in terms of sortal concepts. Concepts, in general, are here understood as intersubjective realizable cognitive capacities. The proper features of sortal concepts are determined by an analysis of the main features of sortal predicates. Posterior to this analysis, the sortal-related logical notions represented in the above logics are discussed. There is also a discussion on the extent to which the set-theoretic formal semantic systems of the book capture different aspects of the conceptualist approach to sortals. These different semantic frameworks are also related to realist and nominalist approaches to sortal predicates, and possible modifications to them are considered that might represent those alternative approaches. (shrink)

The dissertation provides an analysis and elaboration of Michael Dummett's proof-theoretic notions of validity. Dummett's notions of validity are contrasted with standard proof-theoretic notions and formally evaluated with respect to their adequacy to propositional intuitionistic logic.

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 (...) remained open until now whether EP holds for the most well known constructive set theory, CZF. In this paper we show that EP fails for CZF. (shrink)

This paper addresses the problem of upgrading functional information to knowledge. Functional information is defined as syntactically well-formed, meaningful and collectively opaque data. Its use in the formal epistemology of information theories is crucial to solve the debate on the veridical nature of information, and it represents the companion notion to standard strongly semantic information, defined as well-formed, meaningful and true data. The formal framework, on which the definitions are based, uses a contextual version of the verificationist principle of truth (...) in order to connect functional to semantic information, avoiding Gettierization and decoupling from true informational contents. The upgrade operation from functional information uses the machinery of epistemic modalities in order to add data localization and accessibility as its main properties. We show in this way the conceptual worthiness of this notion for issues in contemporary epistemology debates, such as the explanation of knowledge process acquisition from information retrieval systems, and open data repositories. (shrink)

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, $$\widehat{{\textrm{ID}}}{}_{1}^{{\textrm{i}}}{}$$ ID ^ 1 i, over Heyting arithmetic ($${\textrm{HA}}$$ HA ), originally proved in full generality by Arai (Ann Pure Appl Log 162:807–815, 2011. https://doi.org/10.1016/j.apal.2011.03.002). The proof embeds $$\widehat{{\textrm{ID}}}{}_{1}^{{\textrm{i}}}{}$$ ID ^ 1 i into the corresponding theory over Beeson’s logic of partial terms and then uses two consecutive interpretations, a realizability interpretation of this theory into the subtheory generated by almost negative fixpoints, and (...) a direct interpretation into Heyting arithmetic with partial terms using a hierarchy of satisfaction predicates for almost negative formulae. It concludes by applying van den Berg and van Slooten’s result (Indag Math 29:260–275, 2018. https://doi.org/10.1016/j.indag.2017.07.009) that Heyting arithmetic with partial terms plus the schema of self realizability for arithmetic formulae is conservative over $${\textrm{HA}}$$ HA. (shrink)

Alongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum’s Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko’s Theorem. The Jacobson radical in fact turns out to coincide with the classical deductive closure. As a by-product we obtain a possible interpretation in logic of the axioms-as-rules conservation criterion for a multi-conclusion Scott-style entailment (...) relation over a single-conclusion one. (shrink)

This article is about Avicenna’s account of syllogisms comprising opposite premises. We examine the applications and the truth conditions of these syllogisms. Finally, we discuss the relation between these syllogisms and the principle of non-contradiction.

Different formal tools are useful for different purposes. For example, when it comes to modelling degrees of belief, probability theory is a better tool than classical logic; when it comes to modelling the truth of mathematical claims, classical logic is a better tool than probability theory. In this paper I focus on a widely used formal tool and argue that it does not provide a good model of a phenomenon of which many think it does provide a good model: I (...) shall argue that while supervaluationism may provide a model of probability of truth, or of assertability, it cannot provide a good model of truth -- supertruth cannot be truth. The core of the argument is that an adequate model of truth must render certain connectives truth-functional (at least in certain circumstances) -- and supervaluationism does not do so (in those circumstances). (shrink)

In a recent paper, Wigglesworth claims that syntactic criteria of theoretical equivalence are not appropriate for settling questions of equivalence between logical theories, since such criteria judge classical and intuitionistic logic to be equivalent; he concludes that logicians should use semantic criteria instead. However, this is an artefact of the particular syntactic criterion chosen, which is an implausible criterion of theoretical equivalence. Correspondingly, there is nothing to suggest that a more plausible syntactic criterion should not be used to settle questions (...) of equivalence between different logical theories; such a criterion is exhibited and shown to judge classical and intuitionistic logic to be inequivalent. (shrink)

The glueing of (sequentially, pointwise, or uniformly) continuous functions that coincide on the intersection of their closed domains is examined in the light of Bishop-style constructive analysis. This requires us to pay attention to the way that the two domains intersect.

Brouwer’s view on induction has relatively recently been characterised as one on which it is not only intuitive (as expected) but functional, by van Dalen. He claims that Brouwer’s ‘Ur-intuition’ also yields the recursor. Appealing to Husserl’s phenomenology, I offer an analysis of Brouwer’s view that supports this characterisation and claim, even if assigning the primary role to the iterator instead. Contrasts are drawn to accounts of induction by Poincaré, Heyting, and Kreisel. On the phenomenological side, the analysis provides an (...) alternative to that in Tieszen’s Mathematical Intuition, and confirms a view of Gödel on his Dialectica Interpretation. (shrink)

We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$. Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$. In addition, we show that this conservation theorem is optimal in the (...) sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. (shrink)

Historically, it was the interpretations of intuitionist logic in the modal logic S4 that inspired the standard Kripke semantics for intuitionist logic. The inspiration of this paper is the interpretation of intuitionist logic in the non-normal modal logic S3: an S3 model structure can be 'looked at' as an intuitionist model structure and the semantics for S3 can be 'cashed in' to obtain a non-normal semantics for intuitionist propositional logic. This non-normal semantics is then extended to intuitionist quantificational logic.

The well-known algebraic semantics and topological semantics for intuitionistic logic (Int) is here extended to Wansing's bi-intuitionistic logic (2Int). The logic 2Int is also characterised by a quasi-twist structure semantics, which leads to an alternative topological characterisation of 2Int. Later, notions of Fregean negation and of unilateralisation are proposed. The logic 2Int is extended with a ‘Fregean negation’ connective ∼, obtaining 2Int∼, and it is showed that the logic N4⋆ (an extension of Nelson's paraconsistent logic) results to be the unilateralisation (...) of 2Int∼ via ∼. The logic 2Int∼ is also characterised by a Kripke-style semantics, a twist structure semantics and a topological semantics. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

In this paper we introduce a notation system for the infinitary derivations occurring in the ordinal analysis of KP + Π₃-Reflection due to Michael Rathjen. This allows a finitary ordinal analysis of KP + Π₃-Reflection. The method used is an extension of techniques developed by Wilfried Buchholz, namely operator controlled notation systems for RS∞-derivations. Similarly to Buchholz we obtain a characterisation of the provably recursive functions of KP + Π₃-Reflection as <-recursive functions where < is the ordering on Rathjen's ordinal (...) notation system J(K). Further we show a conservation result for $\Pi _{2}^{0}$-sentences. (shrink)

We provide a fine‐grained analysis on the relation between König's lemma, weak König's lemma, and the decidable fan theorem in the context of constructive reverse mathematics. In particular, we show that double negated variants of König's lemma and weak König's lemma are equivalent to double negated variants of the general decidable fan theorem and the binary decidable fan theorem, respectively, over a nearly intuitionistic system containing a weak countable choice only. This implies that the general decidable fan theorem is not (...) equivalent to the binary decidable fan theorem in the absence of a strong countable choice. In addition, we introduce a principle which fills the gap between König's lemma and weak König's lemma, and show that König's lemma is equivalent to weak König's lemma plus this principle. We also solve several problems arising from the investigation. (shrink)

In [17], we introduced an extensional variant of generic realizability [22], where realizers act extensionally on realizers, and showed that this form of realizability provides inner models of $\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and $\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory), that further validate $\mathsf {AC}_{\mathsf {FT}}$ (the axiom of choice in all finite types). In this paper, we show that extensional generic realizability validates several choice principles for dependent types, all exceeding $\mathsf {AC}_{\mathsf {FT}}$. We then show that adding (...) such choice principles does not change the arithmetic part of either $\mathsf {CZF}$ or $\mathsf {IZF}$. (shrink)

On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, and that (...) standard models of formal deduction are not well-equipped to support such evaluations. I discuss a model of proof that is used in the automated deduction community, and show that this model does better in that respect. (shrink)

Strong negation is a well-known alternative to the standard negation in intuitionistic logic. It is defined virtually by giving falsity conditions to each of the connectives. Among these, the falsity condition for implication appears to unnecessarily deviate from the standard negation. In this paper, we introduce a slight modification to strong negation, and observe its comparative advantages over the original notion. In addition, we consider the paraconsistent variants of our modification, and study their relationship with non-constructive principles and connexivity.