Abstract This paper proves normalisation theorems for intuitionist and classical positive free logic, without and with the ι $\iota $ iota operator for definite descriptions ‘the F ’. Positive free logic also opens a number of options for rules for ι $\iota $ iota . In total, six different formalisations of theories of definite descriptions will be discussed, three proposed by Lambert, and three alternatives. The latter are motivated by considerations relating to proof-theoretic harmony between introduction and elimination rules. The philosophical importance of the various systems and results is indicated. The paper builds on [20], but is largely self-contained. The proofs for the present systems are easier than those for negative free logic.
Abstract In the opening sections of Das Kontinuum , Hermann Weyl describes the formation of the mathematical universe as shaped by two generative procedures: the logical process and the mathematical process. These procedures can be iterated, providing a conceptual motivation for the ramified hierarchy. In this paper, we offer a detailed analysis of Weyl’s ideas and present a formalization of the theory resulting from the iteration of the logical–mathematical process. We explore not only the variant based on classical logic, explicitly considered in Das Kontinuum , but also a constructive counterpart. Furthermore, we show that a restricted version of Weyl’s procedure gives rise to a theory that is conservative over the system ACA 0 $\mathbf {ACA}_0$ bold upper A upper C upper A 0 , while the unrestricted version can be interpreted within a certain fragment of Homotopy Type Theory. This provides a precise analysis of the iteration of the mathematical process and establishes a robust link with modern formal systems. Philosophically, our work clarifies the notion of predicativity as conceived by Weyl in this context and highlights its relationship with the logic underlying the process. To this end, we study a version of the Axiom of Reducibility recently introduced by Palmgren.
In this article, I investigate the modal logic of exact equivalence (i.e., sameness of exact verifiers). In particular, by building on Kim's exact truthmaker semantics for modal logic, I provide an answer to the following question: which sentences of the language of propositional modal logic are exactly equivalent by virtue of their logical form?
An apparent issue for the Revision Theory of definitions has long been that its most plausible versions engender $\omega $ -inconsistencies. In this paper I develop a new $\omega $ -consistent revision theory and use it to argue that revision theorists can and should embrace $\omega $ -consistency. I show how my theory, called $\mathbf {S}<^>{\#N}$ , withstands the theoretical pressures towards $\omega $ -inconsistency and moreover compares favorably to the best $\omega $ -inconsistent theories vis-& agrave;-vis several important desiderata. I tentatively conclude that $\mathbf {S}<^>{\#N}$ is the best known revision theory.
Potentialism holds that certain objects are successively generated in an incompletable process. While it is natural to analyze this view modally, there are theorems that connect the resulting modal analysis of potentialism with the non-modal languages of ordinary mathematics. By extending this approach to plural languages, this article proves a far stronger result about definitional equivalence. This opens the door to a new and entirely non-modal explication of potentialism, using a restricted plural logic. Some advantages of this "demodalized" explication are discussed. It is certainly simpler and more user-friendly than the extant modal analysis, as illustrated by an application to potentialist set theory. More ambitiously, I suggest that the explication might also enable potentialists to sidestep the tricky question of which mathematical objects are actual.
Abstract Developments of proof-theoretic semantics that locate meaning uniformly either with introduction rules or with elimination rules give rise to higher-order inference rules. These higher-order rules typically resist straightforward formulation in natural deduction and appear to license a more general class of valid inference patterns than the corresponding rules in Gentzen’s original calculus. Examples from Koslow’s and Schroeder-Heister’s approaches to proof-theoretic semantics illustrate the pattern. We show that this apparent generality is an illusion. In every case in which they arise, the higher-order rule is seen to be a twofold universalization of Gentzen’s lower-level rule and is proven to be interderivable with it. The result highlights the primacy of the universal construction—rather than the details of any particular presentation—as determining meaning. An application to identity shows that higher-order rules can even make explicit universal constructions that remain hidden at the level of familiar inferential patterns.
This paper studies the definability of natural language generalized quantifiers. The semantics of generalized quantifiers are provided by a collection of subsets of the underlying domain. However, the generalized quantifiers appearing in natural language are definable either by first-order quantification or by cardinality notions. This paper provides an explanation for this observed phenomenon. The explanation is that the famous constraints of domain independence and conservativity, when extended to Henkin models, suffice to ensure low-level definability, namely Δ^1_1-definability or at least Σ^1_1-definability; and in most cases this definability can be made to be bounded. This is basically a consequence of Feferman's Preservation Theorem, which Marker has provided a short model-theoretic proof of. Further, we verify that the paradigmatic cardinality quantifiers are indeed Δ^1_1-definable for a reasonable choice of background theory. Finally, in many other cases, we show that this definability can be lowered to first-order definability.
This paper analyses some connectives introduced by Stephen Read, known as 'Bullet connectives'. From the proof-theoretic semantics perspective, these connectives satisfy the requirement of harmony; however, they allow for the looping derivation of a contradiction. Namely, when the operation of detour reduction is applied to such a derivation, it leads to a non-terminating phenomenon. By appealing to Prawtiz's notion of validity, we argue that such connectives cannot be considered as logical ones. Still, it is possible to assign a computational meaning to such connectives, as several useful computation properties are induced by their harmonious behaviour. In particular, we show that a fixed point operator can be defined by using the rules of a generalised version of the Bullet connectives. Such a generalisation is an instance of (non-terminating) recursive types. Finally, we show that type-free (i.e., untyped) lambda-calculus is interpretable in simply typed lambda-calculus extended with yet another variant of the Bullet connectives, and that the introduction rules of the Bullet connectives are interpretable by Nakano's modality in typed lambda-calculus. We conclude that such a computational interpretation of the Bullet connectives is possible only if we separate the notion of types from that of propositions, which are meaningful and assertible linguistic entities (in fact, it is larger). Therefore, the computational interpretation we propose cannot be considered an instance of the Curry-Howard correspondence between propositions and types, and between proofs and programs.
We define a notion of conditional inaccessibility of a decision between two actions represented by two utility functions defined in a finite probability space, where the decision is based on the order of the expected values of the two utility functions: a decision making Agent preferring the action with the higher expected utility. The conditional inaccessibility expresses that the decision cannot be obtained if the expectation values of the utility functions are calculated using the Jeffrey conditional probability defined by a prior and by partial evidence about the probability that determines the decision. Examples of conditionally inaccessible decisions are given, and it is shown that if a conditionally inaccessible decision exists in a probability space, then there exists a continuum number of conditionally inaccessible decisions in that probability space. Open questions and conjectures about the conditional inaccessibility of decisions are formulated. The results are interpreted as showing the crucial role of priors in Bayesian taming of epistemic uncertainties about probabilities that determine decisions based on utility maximizing.
This paper investigates the negation-free fragment of the bi-connexive logic 2C, called 2C $_-$ , from the perspective of bilateralist proof-theoretic semantics (PTS). It is argued that eliminating primitive negation has two important conceptual consequences. First, it requires a reconceptualization of contradictory logics: in a bilateralist framework, contradiction need not be understood in terms of negation inconsistency, but rather as the coexistence of proofs and refutations for certain formulas within a non-trivial system. Second, it challenges the standard definition of connexive logics, which typically rely on negation-based schemata. Instead, a rule-based conception of connexivity, grounded in bilateralist PTS, is proposed. This reconception avoids dependence on the validation of specific formula schemata and thereby also dependence on negation. The paper also addresses the issue of proof-refutation duality in the absence of strong negation, which can be formalized and recovered at a meta-level by extending the system with a two-sorted typed $\lambda $ -calculus.
Central to certain versions of logical atomism are claims to the effect that every proposition is a truth-functional combination of elementary propositions. Assuming that propositions form a Boolean algebra, we consider a number of natural formal regimentations of informal claims in this vicinity, and show that they are equivalent. For a number of reasons, such as the need to accommodate quantifiers, logical atomists might consider only complete Boolean algebras, and take into account infinite truth-functional combinations. We show that in such a variant setting, some of the regimentations come apart, and explore how they relate to each other. We also discuss how they relate to the claim that propositions form a double powerset algebra, which has been proposed by a number of authors as a way of capturing the central logical atomist idea.
This paper explores the mathematical connections between the algebraic and relational semantics of Lewis's logics for counterfactual conditionals. Specifically, we introduce topological variants of Lewis's well-known possible-worlds semantics-based on spheres, selection functions, and orders-and establish duality results with respect to varieties of Boolean algebras equipped with a counterfactual operator, which serve as the equivalent algebraic semantics of Lewis's main systems. These results aim to provide a solid mathematical foundation for the study of Lewis's logics, and offer a new perspective on the most well-known possible worlds-based models. In particular, we write explicit proofs for several results that are often assumed without proof in the literature. Leveraging these duality results, we also derive alternative proofs of strong completeness for Lewis's variably strict conditional logics with respect to their intended models, and clarify the role of the limit assumption in sphere semantics.
The present paper first distinguishes three different ways in which the logic of parthood and composition on the one hand, and the logic of location on the other might interact. It then goes on to explore several relations between location and composition. In doing so it (i) sheds new light on recent results and (ii) proves new substantive ones along the way.
The Lindenbaum lemma saying that completely meet-irreducible closed sets form a basis of any finitary closure system is an easy-to-prove yet crucial result transcending algebraic logic. While the finitarity restriction is crucial for its usual proof, it is not necessary: there are indeed works proving it (or its variant for a larger class of finitely meet-irreducible closed sets) for non-finitary closure systems arising from particular infinitary logics (i.e., substitution-invariant consequence relations). There is also a general result proving it for a wide class of logics with strong p-disjunction and a countable Hilbert-style axiomatization. Identifying the essential properties of strong p-disjunctions we prove a variant of the Lindenbaum lemma for closure systems which are 1) defined over countable sets, 2) countably axiomatized, and 3) frames (in the order-theoretic sense) but not necessarily substitution-invariant.
Dynamic Epistemic Logic extends classical epistemic logic by modeling not only static knowledge but also its evolution through information updates. Among its various systems, Public Announcement Logic (PAL) provides one of the simplest and most studied frameworks for representing epistemic change. While the semantics of PAL is well understood as transformation of Kripke models, the proof theory so far developed fails to represent this dynamism in purely syntactical terms. The aim of this paper is to repair this lack. In particular, building on a hypersequent calculus for S5, we extend it with a mechanism that models the transition between epistemic models induced by public announcements. We call these structures dynamic hypersequents. Using dynamic hypersequents, we construct a calculus for PAL and we show that it enjoys several desirable properties: admissibility of all structural rules (including contraction), invertibility of logical rules, as well as syntactic cut-elimination.
In this note, we investigate iterations of consistency, local and uniform reflection over Heyting arithmetic. For consistency and local reflection, we recover the same results known to hold for Peano arithmetic. In the case of uniform reflection, we present a new, self-contained proof of Dragalin's extension of Feferman's completeness theorem, drawing on ideas from Rathjen's novel proof of Feferman's classical result (cf. [12]).
This paper presents a unified algebraic study of a family of logics related to Abelian logic (Ab), the logic of Abelian lattice-ordered groups. We treat Ab as the base system and refer to its expansions as superabelian logics. The paper focuses on two main families of expansions. First, we investigate the rich landscape of infinitary extensions of Ab, providing an axiomatization for the infinitary logic of real numbers and showing that there exist $2<^>{2<^>\omega }$ distinct logics in this family. Second, we introduce pointed Abelian logic ( ${ ext {pAb}}$ ), the logic of pointed Abelian lattice-ordered groups, by adding a new constant to the language. This framework includes & Lstrok;ukasiewicz unbound logic. We provide axiomatizations for its finitary and infinitary versions as extensions of ${ ext {pAb}}$ and establish their precise relationship with standard & Lstrok;ukasiewicz logic via a formal translation. Finally, the methods developed for this analysis are generalized to axiomatize the logics of other prominent pointed groups.
In Outline of a Theory of Truth, Kripke introduces many of the central concepts of the logical study of truth and paradox. He informally defines some of these-such as groundedness and paradoxicality-using modal locutions. We introduce a modal language for regimenting these informal definitions. Though groundedness and paradoxicality are expressible in the modal language, we prove that intrinsicality-which Kripke emphasizes but does not define modally-is not. This follows from a characterization of the modally definable sets and relations and an attendant axiomatization of the modal semantics.
We prove that the satisfaction relation $\mathcal {N}\models \varphi [\vec a]$ of first-order logic is not absolute between models of set theory having the structure $\mathcal {N}$ and the formulas $\varphi $ all in common. Two models of set theory can have the same natural numbers, for example, and the same standard model of arithmetic $\left \langle {\mathbb N},{+},{\cdot },0,1, <\right \rangle $ , yet disagree on their theories of arithmetic truth; two models of set theory can have the same natural numbers and the same arithmetic truths, yet disagree on their truths-about-truth, at any desired level of the iterated truth-predicate hierarchy; two models of set theory can have the same natural numbers and the same reals, yet disagree on projective truth; two models of set theory can have the same $\left \langle {H}_{\omega _2},{\in }\right \rangle $ or the same rank-initial segment $\left \langle {V}_\delta ,{\in }\right \rangle $ , yet disagree on which assertions are true in these structures. On the basis of these mathematical results, we argue that a philosophical commitment to the determinateness of the theory of truth for a structure cannot be seen as a consequence solely of the determinateness of the structure in which that truth resides. The determinate nature of arithmetic truth, for example, is not a consequence of the determinate nature of the arithmetic structure ${\mathbb N}=\{\,{0,1,2,\ldots }\,\}$ itself, but rather, we argue, is an additional higher-order commitment requiring its own analysis and justification.
This paper develops a logic of essence (HLE) in the framework of higher-order logic. The theory aims to provide a general framework for theorizing about the essences of objects, properties, propositions, and logical operations like conjunction, negation, quantification, etc. The first part of the paper presents the formal language and axiom system of HLE. After that, some theorems of the system are proved and it is shown how the logic of metaphysical necessity can be developed within the framework of HLE. The second part of the paper develops a possible worlds semantics for HLE, gives a proof of soundness, and provides examples of models that demonstrate the consistency of some simple essentialist theories.
