In this paper, we provide a set-theoretic proof of the general representation theorem for MV-algebras, which was developed by Dubuc and Poveda in 2010. The theorem states that every MV-algebra is isomorphic to the MV-algebra of all global sections of its prime spectrum. We avoid using topos theory and instead rely on basic concepts from MV-algebras, topology and set theory.

My aim in this paper is to propose what seems to me a distinctive approach to set theoretic methodology. By ‘methodology’ I mean the study of the actual methods used by practitioners, the study of how these methods might be justified or reformed or extended. So, for example, when the intuitionist's philosophical analysis recommends a wholesale revision of the methods of proof used in classical mathematics, this is a piece of reformist methodology. In contrast with the intuitionist, I will (...) focus more narrowly on the methods of contemporary set theory, and, more importantly, I will certainly recommend no sweeping reforms. Rather, I begin from the assumption that the methodologist's job is to account for set theory as it is practiced, not as some philosophy would have it be. This credo lies at the very heart of the so-called ‘naturalism’ to be described here.A philosopher looking at set theoretic practice from the outside, so to speak, might notice any number of interesting methodological questions, beginning with the intuitionist's ‘why use classical logic?’, but this sort of question is not a live issue for most practicing set theorists. One central question on which the philosopher's and the practitioner's interests converge is this: what is the status of independent statements like the continuum hypothesis (CH)? A number of large questions arise in its wake: what criteria should guide the search for new axioms? For that matter, what reasons support our adoption of the old axioms? (shrink)

We give a simple game-theoretic proof of Silver's theorem that every analytic set is Ramsey. A set P of subsets of ω is called Ramsey if there exists an infinite set H such that either all infinite subsets of H are in P or all out of P. Our proof clarifies a strong connection between the Ramsey property of partitions and the determinacy of infinite games.

In this article we study several reduction principles in the context of Simpson’s set theory ATR0S\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ATR_{0}^{S}$$\end{document} and Kripke-Platek set theory KP (with infinity). Since ATR0S\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ATR_{0}^{S}$$\end{document} is the set-theoretic version of ATR0 there is a direct link to second order arithmetic and the results for reductions over ATR0S\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ATR_{0}^{S}$$\end{document} are as expected and more or less (...) straightforward. However, over KP we obtain several interesting new results and are lead to some open questions. (shrink)

We prove that if is an ω-model of weak weak König’s lemma and , is incomputable, then there exists , such that A and B are Turing incomparable. This extends a recent result of Kučera and Slaman who proved that if is a Scott set and , Aω, is incomputable, then there exists , Bω, such that A and B are Turing incomparable.

Building on early work by Girard ( 1987 ) and using closely related techniques from the proof theory of many-valued logics, we propose a sequent calculus capturing a hierarchy of notions of satisfaction based on the Strong Kleene matrices introduced by Barrio et al. (Journal of Philosophical Logic 49:93–120, 2020 ) and others. The calculus allows one to establish and generalize in a very natural manner several recent results, such as the coincidence of some of these notions with their (...) classical counterparts, and the possibility of expressing some notions of satisfaction for higher-level inferences using notions of satisfaction for inferences of lower level. We also show that at each level all notions of satisfaction considered are pairwise distinct and we address some remarks on the possible significance of this (huge) number of notions of consequence. (shrink)

We give a new proof of a theorem of Shelah which states that for every family of labeled trees, if the cardinality κ of the family is much larger (in the sense of large cardinals) than the cardinality λ of the set of labels, more precisely if the partition relation holds, then there is a homomorphism from one labeled tree in the family to another. Our proof uses a characterization of such homomorphisms in terms of games.

Let KP- be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V:= universe of sets) be a ▵0-definable set function, i.e. there is a ▵0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and $V \models \forall x \exists!y\varphi (x, y)$ . In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection (...) of those functions which are Σ1-definable in KP- + Σ1-Foundation + ∀ x ∃!yφ (x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of ▵0-Dependent Choices to the latter theory. (shrink)

This thesis is concerned with extending the underlying logical approach as well as the breadth of applications of the proof mining program to various (mostly previously untreated) areas of nonlinear analysis and optimization, with a particular focus being placed on topics which involve set-valued operators.For this, we extend the current logical methodology of proof mining by new systems and corresponding so-called logical metatheorems that cover these more involved areas of nonlinear analysis. Most of these systems crucially rely on (...) the use of intensional methods, treating sets with potentially high quantifier complexity in the defining matrix via characteristic functions and axioms that describe only their properties and do not completely characterize the elements of the sets.The applicability of all of these metatheorems is then substantiated by a range of case studies for the respective areas which in particular also highlight the naturalness of the use of intensional methods in the design of the corresponding systems.The first new area covered thereby is the theory of nonlinear semigroups induced by corresponding evolution equations for accretive operators. In that context, we present (besides an initial foray into the area from 2015) essentially the first applications of proof mining to the theory of partial differential equations. Concretely, we provide quantitative versions of four central results on the asymptotic behavior of solutions to such equations.The second new area unlocked in this thesis is that of the continuous dual of a Banach space and its norm (which are also approached via intensional methods). This in particular relies on a proof-theoretically tame treatment of suprema over (certain) bounded sets in this intensional context which is further exploited later on. These systems, which give access to this until now untreated fundamental notion from functional analysis, are then used to provide further substantial extensions to treat various notions from convex analysis like the Fréchet derivative of a convex function, Fenchel conjugates, Bregman distances, and monotone operators on Banach spaces in the sense of Browder.These systems are then utilized to provide applications in the context of Picard- and Halpern-style iterations of so-called Bregman strongly nonexpansive mappings where we provide both new quantitative and qualitative results.Lastly, we discuss the key notion of extensionality of a set-valued operator and its relation to set-theoretic maximality principles in more depth (which was already singled out—to some degree—in previous work). We thereby exhibit an issue arising with treating full extensionality in the context of these intensional approaches to set-valued operators and present useful fragments of the full extensionality statement where these issues are avoided.Corresponding to these fragments, we discuss a range of uniform continuity statements for set-valued operators beyond the usual notion involving the Hausdorff-metric. In particular, in that context, we utilize the previous tame treatment of suprema over bounded sets to also provide the first proof-theoretic treatment of that Hausdorff-metric in the context of systems for proof mining.The applicability of this treatment of the Hausdorff-metric is then in particular substantiated by a last case study where we provide quantitative information for a Mann-type iteration of set-valued mappings which are nonexpansive w.r.t. the Hausdorff-metric.The abstract was taken directly from the thesis.Abstract prepared by Nicholas Pischke, Technische Universität Darmstadt, Darmstadt, GermanyE-mail: [email protected]: https://doi.org/10.26083/tuprints-00026584. (shrink)

We present a semantic proof of Löb's theorem for theories T containing ZF. Without using the diagonalization lemma, we construct a sentence AUT T, which says intuitively that the predicate autological with respect to T (i.e. applying to itself in every model of T) is itself autological with respect to T. In effect, the sentence AUT T states I follow semantically from T. Then we show that this sentence indeed follows from T and therefore is true.

In this paper we show how Dummett-Prawitz-style proof-theoretic semantics has to be modified in order to cope with paradoxical phenomena. It will turn out that one of its basic tenets has to be given up, namely the definition of the correctness of an inference as validity preservation. As a result, the notions of an argument being valid and of an argument being constituted by correct inference rules will no more coincide. The gap between the two notions is accounted for (...) by introducing the distinction between sense and denotation in the proof-theoretic-semantic setting. (shrink)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a (...) technical point of view. (shrink)

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set (...) theories whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms. (shrink)

Gareth Evans proved that if two objects are indeterminately equal then they are different in reality. He insisted that this contradicts the assumption that there can be vague objects. However we show the consistency between Evans's proof and the existence of vague objects within classical logic. We formalize Evans's proof in a set theory without the axiom of extensionality, and we define a set to be vague if it violates extensionality with respect to some other set. There exist (...) models of set theory where the axiom of extensionality does not hold, so this shows that there can be vague objects. (shrink)

On some views, we can be sure that parties to a dispute over the logic of ‘exists’ are not talking past each other if they can characterise ‘exists’ as the only monadic predicate up to logical equivalence obeying a certain set of rules of inference. Otherwise, we ought to be suspicious about the reality of their disagreement. This is what we call a proof- theoretic argument. Pace some critics, who have tried to use proof-theoretic arguments to cast doubts (...) about the reality of disagreements about the logic of ‘exists’, we argue that proof-theoretic arguments can be deployed to establish the reality of several such disagreements. Along the way, we will also utilise this technique to establish similar results about some disagreements over the logic of identity. (shrink)

This paper is the second part of the syntactic demonstration of the Arithmetical Completeness of the modal system G, the first part of which is presented in [9]. Given a sequent S so that ⊢GL-LIN S, ⊬G S, and given its characteristic formula H = char(S), which expresses the non G-provability of S, we construct a canonical proof-tree T of ~ H in GL-LIN, the height of which is the distance d(S, G) of S from G. T is the (...) syntactic countermodel of S with respect to Gand is a tool of general interest in Provability Logic, that allows some classification in the set of the arithmetical interpretations. (shrink)

We perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic GI and global intuitionistic fuzzy logic GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for GI and GIF. Among other things, these calculi allows one to prove Herbrand’s theorem for suitable fragments of GI and GIF.

According to inferentialists the meaning of logical vocabulary is given by the rules of inference governing its use. In response to a challenge posed by Arthur Prior, inferentialists have typically argued that not all sets of rules can define a connective. The project of determining which sets of rules are acceptable definitions has come to be known as the project of finding a criterion of proof-theoretic harmony. One of the best-known proposals is Neil Tennant’s. His criterion of harmony relies (...) on the notions of the strength of a proposition and the strength of a rule. In this note, I argue that Tennant’s appeal to the notion of the strength of a rule gives rise to problems that make his account unsustainable. I also argue that the sort of consideration that gets Tennant into trouble applies, more generally, to other so-called ‘local’ accounts of harmony, and casts doubts on the idea that we can uniquely determine the harmonious counterpart of a given set of rules. (shrink)

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence (...) relation to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

A cut-free Gentzen sequent calculus for Ewald’s intuitionistic tense logic \ is established. By the proof-theoretic method, we prove that, for every set of strictly positive implications S, the classical tense logic \ is embedded into its intuitionistic analogue \ via Kolmogorov, Gödel–Genzten and Kuroda translations respectively. A sufficient and necessary condition for Glivenko type theorem in tense logics is established.

Looking at proof theory as an attempt to ‘code’ the general pattern of the logical steps of a mathematical proof, the question of what kind of rules can make the meaning of a logical connective completely explicit does not seem to have been answered satisfactorily. The lambda calculus seems to have been more coherent simply because the use of ‘λ’ together with its projection 'apply' is specified by what can be called a 'reduction' rule: β‐conversion. We attempt to (...) analyse the role of proof rules, making use of a set of formal rules designed to capture both the notions of proof theory and those of the lambda‐calculus: Martin‐Löf's Intuitionistic Type Theory. (shrink)

This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, (...) but the term itself was proposed by Schroeder-Heister in the 1980s. Proof-theoretic semantics explains the meaning of linguistic expressions in general and of logical constants in particular in terms of the notion of proof. This volume emerges from presentations at the Second International Conference on Proof-Theoretic Semantics in Tübingen in 2013, where contributing authors were asked to provide a self-contained description and analysis of a significant research question in this area. The contributions are representative of the field and should be of interest to logicians, philosophers, and mathematicians alike. (shrink)

In ordinal analysis of impredicative theories so-called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the collapsing functions as operating directly on admissible (...) sets also renders a new and perspicuous approach to well-ordering proofs possible. MSC: 03F15, 03F35. (shrink)

We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational account of proof-theoretic harmony. With every set of introduction rules a canonical (...) elimination rule, and with every set of elimination rules a canonical introduction rule is associated in such a way that the canonical rule is in harmony with the set of rules it is associated with. An example given by Hazen and Pelletier is used to demonstrate that there are significant connectives, which are characterized by their elimination rules, and whose introduction rule is the canonical introduction rule associated with these elimination rules. Due to the availabiliy of higher-level rules and propositional quantification, the means of expression of the framework developed are sufficient to ensure that the construction of canonical elimination or introduction rules is always possible and does not lead out of this framework. (shrink)

We characterize the proof-theoretic strength of systems of explicit mathematics with a general principle asserting the existence of least fixed points for monotone inductive definitions, in terms of certain systems of analysis and set theory. In the case of analysis, these are systems which contain the Σ12-axiom of choice and Π12-comprehension for formulas without set parameters. In the case of set theory, these are systems containing the Kripke-Platek axioms for a recursively inaccessible universe together with the existence of a (...) stable ordinal. In all cases, the exact strength depends on what forms of induction are admitted in the respective systems. (shrink)

Inquiry into the metaphysics of essence tends to be pursued in a realist and model-theoretic spirit, in the sense that metaphysical vocabulary is used in a metalanguage to model truth conditions for the object-language use of essentialist vocabulary. This essay adapts recent developments in proof-theoretic semantics to provide a nominalist analysis for a variety of essentialist vocabularies. A metalanguage employing explanatory inferences is used to individuate introduction and elimination rules for atomic sentences. The object-language assertions of sentences concerning essences (...) are then interpreted as devices for marking off structural features of the explanatory inferences that, under a given interpretation, constitute the contents of the atoms of the language. On this proposal, object-language essentialist vocabulary is mentioned in a proof-theoretic metalanguage that uses a vocabulary of explanation. The result is a nominalist interpretation of essence as a modality, understood in the grammatical sense as a modification of the copula, and a view of metaphysical inquiry that is closely connected to the explanatory commitments present in first-order inquiry into things like sets, chemicals, and organisms. This result illustrates that some of the presuppositions that have animated analytic metaphysics over the last few decades can be profitably substituted with more practice-oriented conceptions of the forms of reasoning at work in different domains of human knowledge. (shrink)

In this paper, we shall present a generalization of phrase structure grammar, in which all functional categories have type restrictions, that is, their argument types are specific domains. In ordinary phrase structure grammar, there is just one universal domain of individuals. The grammar does not make a distinction between verbs and adjectives in terms of domains of applicability. Consequently, it fails to distinguish between sentences like every line intersects every line, which is well typed, and every line intersects every point, (...) which is ill typed.Our generalization relates to ordinary phrase structure grammar in the same way as the higherlevel constructive type theory of Martin-Löf relates to the simple type theory of Church . Simple type theory has been used in linguistics and related with phrase structure grammar, especially in the tradition based on the work of Montague .Our definition of the grammar will be more formal than Montague's in the sense that we shall use a formal metalanguage, that of constructive type theory, for defining both the object language and its interpretation. The grammar, both syntax and semantics, is thus readily implementable in the type-theoretical proof system ALF . Inside type theory, a distinction can be made between the object language and the model, in other words, between syntactic and semantic types. It will turn out that the object language cannot be defined independently of the model, as in ordinary Tarski semantics. This is a direct consequence of introducing the typing restrictions.The grammar presented here can be seen as a formal linguistic elaboration of the work presented in Ranta 1991 and 1994. The organization of generative grammar as categorial grammar followed by sugaring should now look more familiar to the linguist, as the grammatical formalism on which sugaring operates is no longer full type theory but a set of phrase structure trees. (shrink)

Smullyan in [Smu61] identified the recursion theoretic essence of incompleteness results such as Gödel's first incompleteness theorem and Rosser's theorem. Smullyan showed that, for sufficiently complex theories, the collection of provable formulae and the collection of refutable formulae are effectively inseparable—where formulae and their Gödel numbers are identified. This paper gives a similar treatment for proof speed-up. We say that a formal system S1is speedable over another system S0on a set of formulaeAiff, for each recursive functionh, there is a (...) formulaαinAsuch that the length of the shortest proof ofαin S0is larger thanhof the shortest proof ofαin S1. We characterize speedability in terms of the inseparability by r.e. sets of the collection of formulae which are provable in S1but unprovable in S0from the collectionA–where again formulae and their Gödel numbers are identified. We provide precise definitions of proof length, speedability and r.e. inseparability below.We follow the terminology and notation of [Rog87] with borrowings from [Soa87]. Below,ϕis an acceptable numbering of the partial recursive functions [Rog87] andΦa complexity measure associated withϕ[Blu67], [DW83]. (shrink)

The interplay of philosophical ambitions and technical reality have given birth to rich and interesting approaches to explain the oft-claimed special character of mathematical and logical knowledge. Two projects stand out both for their audacity and their innovativeness. These are logicism and proof-theoretic semantics. This dissertation contains three chapters exploring the limits of these two projects. In both cases I find the formal results offer a mixed blessing to the philosophical projects. Chapter 1. Is a logicist bound to the (...) claim that as a matter of analytic truth there is an actual infinity of objects? If Hume’s Principle is analytic then in the standard setting the answer appears to be yes. Hodes’s work pointed to a way out by offering a modal picture in which only a potential infinity was posited. However, this project was abandoned due to apparent failures of cross-world predication. I re-explore this idea and discover that in the setting of the potential infinite one can interpret first-order Peano arithmetic, but not second-order Peano arithmetic. I conclude that in order for the logicist to weaken the metaphysically loaded claim of necessary actual infinities, they must also weaken the mathematics they recover. Chapter 2. There have been several recent results bringing into focus the super-intuitionistic nature of most notions of proof-theoretic validity. But there has been very little work evaluating the consequences of these results. In this chapter, I explore the question of whether these results undermine the claim that proof-theoretic validity shows us which inferences follow from the meaning of the connectives when defined by their introduction rules. It is argued that the super-intuitionistic inferences are valid due to the correspondence between the treatment of the atomic formulas and more complex formulas. And so the goals of proof-theoretic validity are not undermined. Chapter 3. Prawitz (1971) conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister (2019). This chapter resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The chapter further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to allow double negation elimination for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic.Abstract prepared by Will Stafford extracted partially from the dissertation. (shrink)

This book presents a detailed treatment of ordinal combinatorics of large sets tailored for independence results. It uses model theoretic and combinatorial methods to obtain results in proof theory, such as incompleteness theorems or a description of the provably total functions of a theory. In the first chapter, the authors first discusses ordinal combinatorics of finite sets in the style of Ketonen and Solovay. This provides a background for an analysis of subsystems of Peano Arithmetic as well as for (...) combinatorial independence results. Next, the volume examines a variety of proofs of Gödel's incompleteness theorems. The presented proofs differ strongly in nature. They show various aspects of incompleteness phenomena. In additon, coverage introduces some classical methods like the arithmetized completeness theorem, satisfaction predicates or partial satisfaction classes. It also applies them in many contexts. The fourth chapter defines the method of indicators for obtaining independence results. It shows what amount of transfinite induction we have in fragments of Peano arithmetic. Then, it uses combinatorics of large sets of the first chapter to show independence results. The last chapter considers nonstandard satisfaction classes. It presents some of the classical theorems related to them. In particular, it covers the results by S. Smith on definability in the language with a satisfaction class and on models without a satisfaction class. Overall, the book's content lies on the border between combinatorics, proof theory, and model theory of arithmetic. It offers readers a distinctive approach towards independence results by model-theoretic methods. (shrink)

The model-theoretic analysis of the concept of logical consequence has come under heavy criticism in the last couple of decades. The present work looks at an alternative approach to logical consequence where the notion of inference takes center stage. Formally, the model-theoretic framework is exchanged for a proof-theoretic framework. It is argued that contrary to the traditional view, proof-theoretic semantics is not revisionary, and should rather be seen as a formal semantics that can supplement model-theory. Specifically, there are (...) formal resources to provide a proof-theoretic semantics for both intuitionistic and classical logic. We develop a new perspective on proof-theoretic harmony for logical constants which incorporates elements from the substructural era of proof-theory. We show that there is a semantic lacuna in the traditional accounts of harmony. A new theory of how inference rules determine the semantic content of logical constants is developed. The theory weds proof-theoretic and model-theoretic semantics by showing how proof-theoretic rules can induce truth-conditional clauses in Boolean and many-valued settings. It is argued that such a new approach to how rules determine meaning will ultimately assist our understanding of the apriori nature of logic. (shrink)

We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to occur (...) only strictly positively. The modelling is done by constructivizing continuity notions for set operators at higher number classes and proving that strictly positive set operators are continuous in this sense. The existence of least fixed points, or more accurately, least sets closed under the operator, then easily follows. (shrink)

In Arai (An ordinal analysis of a single stable ordinal, submitted) it is shown that an ordinal \(\sup _{N is an upper bound for the proof-theoretic ordinal of a set theory \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma _{1}}V)\). In this paper we show that a second order arithmetic \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) proves the wellfoundedness up to \(\psi _{\varOmega _{1}}(\varepsilon _{\varOmega _{{\mathbb {S}}+N+1}})\) for each _N_. It is easy to interpret \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) in \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma (...) _{1}}V)\). (shrink)

A set-theoretical proof of Gowers’ Dichotomy Theorem is presented together with its application to another dichotomy concerning asymptotic l 2 basic sequences.

Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11, 12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired (...) by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature. This paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in [20]. (shrink)

We have here a systematic examination of systems of logic cast in "natural deduction" form, in the widest sense of that word. Naturally enough, the author begins with Gentzen-style systems, moves by means of the inversion principle in int-elim logics to deductions of classical and intuitionistic logic which have a canonical "normal form"; more briefly, but always with clarity, Prawitz examines natural deduction for second-order and modal logics, and also systems with even less usual forms of implication. Three appendices cover (...) the Sequenzen-kalkül of Gentzen, a system of set theory of Fitch, and some alternative formulations of natural deductions due to Jáskowski and others. There is a short bibliography. There are also some hilarious misprints, few serious.—P. J. M. (shrink)

In this paper I shall present a method for proving determinacy from large cardinals which, in many cases, seems to yield optimal results. One of the main applications extends theorems of Martin, Steel and Woodin about determinacy within the projective hierarchy. The method can also be used to give a new proof of Woodin's theorem about determinacy in L.The reason we look for optimal determinacy proofs is not only vanity. Such proofs serve to tighten the connection between large cardinals (...) and descriptive set theory, letting us bring our knowledge of one subject to bear on the other, and thus increasing our understanding of both. A classic example of this is the Harrington-Martin proof that -determinacy implies -determinacy. This is an example of a transfer theorem, which assumes a certain determinacy hypothesis and proves a stronger one. While the statement of the theorem makes no mention of large cardinals, its proof goes through 0#, first proving that-determinacy ⇒ 0# exists,and then that0# exists ⇒ -determinacyMore recent examples of the connection between large cardinals and descriptive set theory include Steel's proof thatADL ⇒ HODL ⊨ GCH,see [9], and several results of Woodin about models of AD+, a strengthening of the axiom of determinacy AD which Woodin has introduced. These proofs not only use large cardinals, but also reveal a deep, structural connection between descriptive set theoretic notions and notions related to large cardinals. (shrink)

We present an extension of constructive Zermelo{Fraenkel set theory [2]. Constructive sets are endowed with an applicative structure, which allows us to express several set theoretic constructs uniformly and explicitly. From the proof theoretic point of view, the addition is shown to be conservative. In particular, we single out a theory of constructive sets with operations which has the same strength as Peano arithmetic.

In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction (...) system of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...) class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope. (shrink)

At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...) from calculation gave rise to concerns as to whether such methods were meaningful, or appropriate to mathematics. The discovery of paradoxes stemming from overly naive use of set-theoretic language and methods led to even more pressing concerns as to whether the modern methods were even consistent. This led to heated debates in the early twentieth century and what is sometimes called the “crisis of foundations.” In lectures presented in 1922, David Hilbert launched his Beweistheorie, or Proof Theory, which aimed to justify the use of modern methods and settle the problem of foundations once and for all. This, Hilbert argued, could be achieved as follows. (shrink)

This paper shows that species are individuals with respect to evolutionary theory in the sense that the laws of the theory deal with species as irreducible wholes rather than as sets of organisms. 'Species X' is an instantiation of a primitive term of the theory. I present a sketch of a proof that it cannot be defined within the theory as a set of organisms; the proof relies not on details of my axiomatization but rather on a generally (...) accepted property of speciation; hence the same argument should work for any axiomatization which captures this generally accepted property of speciation. (shrink)

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 is the third edition of a book originally published in the 1970s; it provides a systematic and nicely organized presentation of the elegant method of using Boolean-valued models to prove independence results. Four things are new in the third edition: background material on Heyting algebras, a chapter on ‘Boolean-valued analysis’, one on using Heyting algebras to understand intuitionistic set theory, and an appendix explaining how Boolean and Heyting algebras look from the perspective of category theory. The book presents results (...) from a number of set theorists and includes an insightful and informative foreword by Dana Scott. Bell's presentation is lively and pleasant to read, and the material is given in a nicely cohesive way.One obvious reason to be interested in independence proofs is that they concern the important question, what is the set-theoretic hierarchy like? The proofs in Bell's book cover some of the most basic and fundamental independence results, such as those concerning the size of the continuum, the independence of the Axiom of Choice from ZF, cardinal collapsing, Souslin's hypothesis, and Martin's Axiom.Since Gödel's incompleteness theorem, it has been known that for any serious candidate list of set-theoretic axioms, there will be statements neither provable nor disprovable from those axioms. What is really interesting, however, and what the independence proofs discussed here show, is how many of the most natural questions about sets are not decided by the standard axioms of ZFC, and how …. (shrink)