We emphasize the role of the choice of vocabulary in formalization of a mathematical area and remark that this is a particular preoccupation of logicians. We use this framework to discuss Kennedy’s notion of ‘formalism freeness’ in the context of various schools in model theory. Then we clarify some of the mathematical issues in recent discussions of purity in the proof of the Desargues proposition. We note that the conclusion of ‘spatial content’ from the Desargues proposition involves arguments which are algebraic and even metamathematical. Hilbert showed that the Desargues proposition implies the coordinatizing ring is associative, which in turn implies the existence of a three-dimensional geometry in which the given plane can be embedded. With W. Howard we give a new proof, removing Hilbert’s ‘detour’ through algebra, of the ‘geometric’ embedding theorem.

Finally, our investigation of purity leads to the conclusion that even the introduction of explicit definitions in a proof can violate purity. We argue that although both involve explicit definition, our proof of the embedding theorem is pure while Hilbert’s is not. Thus the determination of whether an argument is pure turns on the content of the particular proof. Moreover, formalizing the situation does not provide a tool for characterizing purity.

This paper shows that any propositional logic that extends a basic substructural logic BSL (a weak, nondistributive, nonassociative, and noncommutative version of Full Lambek logic with a paraconsistent negation) can be enriched with questions in the style of inquisitive semantics and logic. We introduce a relational semantic framework for substructural logics that enables us to define the notion of an inquisitive extension of λ, denoted as ${\lambda ^?}$, for any logic λ that is at least as strong as BSL. A general theory of these “inquisitive extensions” is worked out. In particular, it is shown how to axiomatize ${\lambda ^?}$, given the axiomatization of λ. Furthermore, the general theory is applied to some prominent logical systems in the class: classical logic Cl, intuitionistic logic Int, and t-norm based fuzzy logics, including for example Łukasiewicz fuzzy logic Ł. For the inquisitive extensions of these logics, axiomatization is provided and a suitable semantics found.

We investigate the general properties of general Bayesian learning, where “general Bayesian learning” means inferring a state from another that is regarded as evidence, and where the inference is conditionalizing the evidence using the conditional expectation determined by a reference probability measure representing the background subjective degrees of belief of a Bayesian Agent performing the inference. States are linear functionals that encode probability measures by assigning expectation values to random variables via integrating them with respect to the probability measure. If a state can be learned from another this way, then it is said to be Bayes accessible from the evidence. It is shown that the Bayes accessibility relation is reflexive, antisymmetric, and nontransitive. If every state is Bayes accessible from some other defined on the same set of random variables, then the set of states is called weakly Bayes connected. It is shown that the set of states is not weakly Bayes connected if the probability space is standard. The set of states is called weakly Bayes connectable if, given any state, the probability space can be extended in such a way that the given state becomes Bayes accessible from some other state in the extended space. It is shown that probability spaces are weakly Bayes connectable. Since conditioning using the theory of conditional expectations includes both Bayes’ rule and Jeffrey conditionalization as special cases, the results presented generalize substantially some results obtained earlier for Jeffrey conditionalization.

We prove that the theory of the extensional compositional truth predicate for the language of arithmetic with Δ0-induction scheme for the truth predicate and the full arithmetical induction scheme is not conservative over Peano Arithmetic. In addition, we show that a slightly modified theory of truth actually proves the global reflection principle over the base theory.

We examine the closure conditions of the probabilistic consequence relation of Hawthorne and Makinson, specifically the outstanding question of completeness in terms of Horn rules, of their proposed (finite) set of rules O. We show that on the contrary no such finite set of Horn rules exists, though we are able to specify an infinite set which is complete.

A formalization of Gödel’s incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows Świerczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of this theory is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalization itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.

Following recent developments in the literature on axiomatic theories of truth, we investigate an alternative to the widespread habit of formalizing the syntax of the object-language into the object-language itself. We first argue for the proposed revision, elaborating philosophical evidences in favor of it. Secondly, we present a general framework for axiomatic theories of truth with ‘disentangled’ theories of syntax. Different choices of the object theory O will be considered. Moreover, some strengthenings of these theories will be introduced: we will consider extending the theories by the addition of coding axioms or by extending the schemas of O, if present, to the entire vocabulary of our theory of truth. Finally, we touch on the philosophical consequences that the theories described can have on the debate about the metaphysical status of the truth predicate and on the formalization of our informal metatheoretic reasoning.

This paper investigates the question of characterizing first-order LFIs (logics of formal inconsistency) by means of two-valued semantics. LFIs are powerful paraconsistent logics that encode classical logic and permit a finer distinction between contradictions and inconsistencies, with a deep involvement in philosophical and foundational questions. Although focused on just one particular case, namely, the quantified logic QmbC, the method proposed here is completely general for this kind of logics, and can be easily extended to a large family of quantified paraconsistent logics, supplying a sound and complete semantical interpretation for such logics. However, certain subtleties involving term substitution and replacement, that are hidden in classical structures, have to be taken into account when one ventures into the realm of nonclassical reasoning. This paper shows how such difficulties can be overcome, and offers detailed proofs showing that a smooth treatment of semantical characterization can be given to all such logics. Although the paper is well-endowed in technical details and results, it has a significant philosophical aside: it shows how slight extensions of classical methods can be used to construct the basic model theory of logics that are weaker than traditional logic due to the absence of certain rules present in classical logic. Several such logics, however, as in the case of the LFIs treated here, are notorious for their wealth of models precisely because they do not make indiscriminate use of certain rules; these models thus require new methods. In the case of this paper, by just appealing to a refined version of the Principle of Explosion, or Pseudo-Scotus, some new constructions and crafty solutions to certain nonobvious subtleties are proposed. The result is that a richer extension of model theory can be inaugurated, with interest not only for paraconsistency, but hopefully to other enlargements of traditional logic.

The two expressions ‘The cumulative hierarchy’ and ‘The iterative conception of sets’ are usually taken to be synonymous. However, the second is more general than the first, in that there are recursive procedures that generate some ill-founded sets in addition to well-founded sets. The interesting question is whether or not the arguments in favour of the more restrictive version – the cumulative hierarchy – were all along arguments for the more general version.

We analyze the precise modal commitments of several natural varieties of set-theoretic potentialism, using tools we develop for a general model-theoretic account of potentialism, building on those of Hamkins, Leibman and Löwe [14], including the use of buttons, switches, dials and ratchets. Among the potentialist conceptions we consider are: rank potentialism (true in all larger $V_\beta $ ), Grothendieck–Zermelo potentialism (true in all larger $V_\kappa $ for inaccessible cardinals $\kappa $ ), transitive-set potentialism (true in all larger transitive sets), forcing potentialism (true in all forcing extensions), countable-transitive-model potentialism (true in all larger countable transitive models of ZFC), countable-model potentialism (true in all larger countable models of ZFC), and others. In each case, we identify lower bounds for the modal validities, which are generally either S4.2 or S4.3, and an upper bound of S5, proving in each case that these bounds are optimal. The validity of S5 in a world is a potentialist maximality principle, an interesting set-theoretic principle of its own. The results can be viewed as providing an analysis of the modal commitments of the various set-theoretic multiverse conceptions corresponding to each potentialist account.

Valentini (1983) has presented a proof of cut-elimination for provability logic GL for a sequent calculus using sequents built from sets as opposed to multisets, thus avoiding an explicit contraction rule. From a formal point of view, it is more syntactic and satisfying to explicitly identify the applications of the contraction rule that are ‘hidden’ in proofs of cut-elimination for such sequent calculi. There is often an underlying assumption that the move to a proof of cut-elimination for sequents built from multisets is straightforward. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of the calculus with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut-elimination for GL in a multiset setting.

Here we refute this claim by placing Valentini’s arguments in a formal setting and proving cut-elimination for sequents built from multisets. The use of sequents built from multisets enables us to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini’s original proof relies on a novel induction parameter called “width” which is computed ‘globally’. It is difficult to verify the correctness of his induction argument based on “width.” In our formulation however, verification of the induction argument is straightforward. Finally, the multiset setting also introduces a new complication in the case of contractions above cut when the cut-formula is boxed. We deal with this using a new transformation based on Valentini’s original arguments.

Finally, we discuss the possibility of adapting this cut-elimination procedure to other logics axiomatizable by formulae of a syntactically similar form to the GL axiom.

We develop a point-free construction of the classical one-dimensional continuum, with an interval structure based on mereology and either a weak set theory or a logic of plural quantification. In some respects, this realizes ideas going back to Aristotle, although, unlike Aristotle, we make free use of contemporary “actual infinity”. Also, in contrast to intuitionistic analysis, smooth infinitesimal analysis, and Eret Bishop’s (1967) constructivism, we follow classical analysis in allowing partitioning of our “gunky line” into mutually exclusive and exhaustive disjoint parts, thereby demonstrating the independence of “indecomposability” from a nonpunctiform conception. It is surprising that such simple axioms as ours already imply the Archimedean property and the interval analogue of Dedekind completeness (least-upper-bound principle), and that they determine an isomorphism with the Dedekind–Cantor structure of ℝ as a complete, separable, ordered field. We also present some simple topological models of our system, establishing consistency relative to classical analysis. Finally, after describing how to nominalize our theory, we close with comparisons with earlier efforts related to our own.

This paper extends Kripke’s theory of truth to a language with a variably strict conditional operator, of the kind that Stalnaker and others have used to represent ordinary indicative conditionals of English. It then shows how to combine this with a different and independently motivated conditional operator, to get a substantial logic of restricted quantification within naive truth theory.

According to propositional contingentism, it is contingent what propositions there are. This paper presents two ways of modeling contingency in what propositions there are using two classes of possible worlds models. The two classes of models are shown to be equivalent as models of contingency in what propositions there are, although they differ as to which other aspects of reality they represent. These constructions are based on recent work by Robert Stalnaker; the aim of this paper is to explain, expand, and, in one aspect, correct Stalnaker’s discussion.

Increases in the use of automated theorem-provers have renewed focus on the relationship between the informal proofs normally found in mathematical research and fully formalised derivations. Whereas some claim that any correct proof will be underwritten by a fully formal proof, sceptics demur. In this paper I look at the relevance of these issues for formalism, construed as an anti-platonistic metaphysical doctrine. I argue that there are strong reasons to doubt that all proofs are fully formalisable, if formal proofs are required to be finitary, but that, on a proper view of the way in which formal proofs idealise actual practice, this restriction is unjustified and formalism is not threatened.

In practice, mathematical proofs are most often the result of careful planning by the agents who produced them. As a consequence, each mathematical proof inherits a plan in virtue of the way it is produced, a plan which underlies its “architecture” or “unity.” This paper provides an account of plans and planning in the context of mathematical proofs. The approach adopted here consists in looking for these notions not in mathematical proofs themselves, but in the agents who produced them. The starting point is to recognize that to each mathematical proof corresponds a proof activity which consists of a sequence of deductive inferences—i.e., a sequence of epistemic actions—and that any written mathematical proof is only a report of its corresponding proof activity. The main idea to be developed is that the plan of a mathematical proof is to be conceived and analyzed as the plan of the agent(s) who carried out the corresponding proof activity. The core of the paper is thus devoted to the development of an account of plans and planning in the context of proof activities. The account is based on the theory of planning agency developed by Michael Bratman in the philosophy of action. It is fleshed out by providing an analysis of the notions of intention—the elementary components of plans—and practical reasoning—the process by which plans are constructed—in the context of proof activities. These two notions are then used to offer a precise characterization of the desired notion of plan for proof activities. A fruitful connection can then be established between the resulting framework and the recent theme of modularity in mathematics introduced by Jeremy Avigad. This connection is exploited to yield the concept of modular presentations of mathematical proofs which has direct implications for how to write and present mathematical proofs so as to deliver various epistemic benefits. The account is finally compared to the technique of proof planning developed by Alan Bundy and colleagues in the field of automated theorem proving. The paper concludes with some remarks on how the framework can be used to provide an analysis of understanding and explanation in the context of mathematical proofs.

In this sequel to Self-reference in arithmetic I we continue our discussion of the question: What does it mean for a sentence of arithmetic to ascribe to itself a property? We investigate how the properties of the supposedly self-referential sentences depend on the chosen coding, the formulae expressing the properties and the way a fixed point for the expressing formulae are obtained. In this second part we look at some further examples. In particular, we study sentences apparently expressing their Rosser-provability, their own ${\rm{\Sigma }}_n^0$-truth or their own ${\rm{\Pi }}_n^0$-truth. Finally we offer an assessment of the results of both papers.

We propose a model for belief which is free of presuppositions. Current models for belief suffer from two difficulties. One is the well known problem of logical omniscience which tends to follow from most models. But a more important one is the fact that most models do not even attempt to answer the question what it means for someone to believe something, and just what it is that is believed. We provide a flexible model which allows us to give meaning to beliefs in general contexts, including the context of animal belief (where action is usually our only clue to a belief), and of human belief which is expressed in language.

The notion of strict identity is sometimes given an explicit second-order definition: objects with all the same properties are identical. Here, a somewhat different problem is raised: Under what conditions is the identity relation on the domain of a structure first-order definable? A structure may have objects that are distinct, but indiscernible by the strongest means of discerning them given the language (the indiscernibility formula). Here a number of results concerning the indiscernibility formula, and the definability of identity, are collected and a number of applications discussed.

In this paper we will investigate different axiomatic theories of truth that are minimal in some sense. One criterion for minimality will be conservativity over Peano Arithmetic. We will then give a more fine-grained characterization by investigating some interpretability relations. We will show that disquotational theories of truth, as well as compositional theories of truth with restricted induction are relatively interpretable in Peano Arithmetic. Furthermore, we will give an example of a theory of truth that is a conservative extension of Peano Arithmetic but not interpretable in it. We will then use stricter versions of interpretations to compare weak theories of truth to subsystems of second-order arithmetic.