Being relevant to some topic can be informally understood as making a difference or having something to contribute. Given a sequent Delta:Gamma, we can say, somewhat schematically, that a component of the sequent is relevant to the sequent when it contributes to the validity of the sequent. Different ways of making precise the idea of contributing to the validity and different understandings of the components of a sequent lead to a hierarchy of explications of relevance. I identify four key explications, called gaunt validity, perfect validity, relevant validity, and perfectibility. Each is shown to enjoy an interesting variable sharing property. Furthermore, if we begin with a standard sequent calculus for classical logic and introduce some simple constraints on the rules, the result is a fragment of classical logic that proves exactly the gauntly valid sequents.
Abstract treating negation as a defined connective, and a key lemma fails when $$\lnot $$ ¬ is included as a primitive connective. I provide a new proof of this result that applies when negation is a primitive connective and which also shows that $$\wedge ,\vee ,\rightarrow ,\lnot $$ ∧ , ∨ , → , ¬ are not interdefinable.
Set-theoretic potentialism is the view that the universe of sets is potentially infinite: it can always, necessarily, be expanded to a more inclusive universe of sets. One version of this view is that the set-theoretic universe can always be expanded to a forcing extension in particular. This view has primarily been studied from a technical point of view, however; in this chapter I explore what philosophical conceptions of set theory might motivate forcing potentialism. I begin by raising an explanatory challenge for any form of width potentialism based on the iterative conception of set and then sharpen this challenge to argue that any broadly iterative conception of set is inconsistent with the claim that the possible width extension of a universe are exactly its forcing extensions. Finally, I suggest one possible way meeting the explanatory challenge by disentangling the iterative conception of set formation from the combinatorial conception of sethood. This makes room for what I call the iterative logical conception of set. I sketch a toy model of a potentialist system which is both height- and width potentialist and where the width extension include all (but not only) the forcing extensions.
Free choice sequences play a key role in the Brouwerian continuum. Using recent modal analysis of potential infinity, we can make sense of free choice sequences as potentially infinite sequences of natural numbers without adopting Brouwer’s distinctive idealistic metaphysics. This provides classicists with a means to make sense of intuitionistic ideas from their own classical perspective. I develop a modal-potentialist theory of real numbers that suffices to capture the most distinctive features of intuitionistic analysis, such as Brouwer’s continuity theorem, the existence of a sequence that is monotone, bounded, and non-convergent, and the inability to decompose the continuum non-trivially.
Abstract This paper explores how, given a proof, we can systematically transform it into a proof that contains no irrelevancies and which is as strong as possible. I define a weaker and stronger notion of what counts as a proof with no irrelevancies, calling them perfect proofs and gaunt proofs, respectively. Using classical core logic to study classical validities and core logic to study intuitionistic validities, I show that every core proof or classical core proof can be transformed into a perfect proof. In a sequel paper, I show how proofs in core logic can also be transformed into gaunt proofs and I observe that this property fails for classical core logic.
This paper is the second part of a series exploring how, given a proof, we can inductively transform it into a proof that contains no irrelevancies and is as strong as possible. In the prequel paper, I defined a weaker and a stronger notion of what counts as a proof with no irrelevancies, calling them perfect proofs and gaunt proofs, respectively. There, I showed how proofs in core logic and classical core logic can be transformed into perfect proofs. In this paper I study gaunt proofs. I show how proofs in core logic can be inductively transformed into gaunt core proofs, but that this property fails for the natural deduction system of classical core logic.