Walter Dean

The thesis underlying this paper is that _informal rigour_ – a term famously coined by Kreisel in [ 63 ] – corresponds to a more definite method than has previously been recognized. We will illustrate this by first presenting a scheme for what we will refer to as an _informally rigorous argument_ and then showing in detail how the three central examples considered by Kreisel [ 64 ] conform to this. These respectively pertain to the analysis of first-order validity, the status Markov’s Principle in intuitionistic analysis, and the definiteness of the Continuum Hypothesis. Upon comparing these arguments systematically, we will suggest that the latter is the most tendentious in virtue of the status which Kreisel himself came to assign to the notion of second-order validity. We conclude by providing some brief observations about the scope and continued significance of Kreisel’s method.

This paper explores the relationship of artificial intelligence to resolving open questions in mathematics. We first argue that limitative results from computability and complexity theory retain their significance in illustrating that proof discovery is an inherently difficult problem. We next consider how applications of automated theorem proving, Sat-solvers, and large language models raise underexplored questions about the nature of mathematical proof — e.g., about the status of brute force and the relationship between logical and discovermental complexity. Nevertheless, we finally suggest that the results obtained thus far by automated methods do not tell against the inherent difficulty of proof discovery.

The goal of this paper is to consider the prospects for developing a consistent variant of the Theory of Constructions originally proposed by Georg Kreisel and Nicolas Goodman in light of two developments which have been traditionally associated with the theory—i.e. Kreisel’s second clause interpretation of the intuitionistic connectives, and an antinomy about constructive provability sometimes referred to as the Kreisel-Goodman paradox. After discussing the formulation of the theory itself, we then discuss how it can be used to formalize the BHK interpretation in light of concerns about the impredicativity of intuitionistic implication and Kreisel’s proposed amendments to overcome this. We next reconstruct Goodman’s presentation of a paradox pertaining to a “naive” variant of the theory and discuss the influence this had on its subsequent reception. We conclude by considering various means of responding to this result. Contrary to the received view that the second clause interpretation itself contributes to the paradox, we argue that the inconsistency arises in virtue of an interaction between reflection and internalization principles similar to those employed in Artemov’s Logic of Proofs.

This paper presents a reverse mathematical analysis of several forms of the sorites paradox. We first illustrate how traditional discrete formulations are reliant on Hölder’s representation theorem for ordered Archimedean groups. While this is provable in $\mathsf {RCA}_0$, we also consider two forms of the sorites which rest on non-constructive principles: the continuous sorites of Weber & Colyvan [35] and a variant we refer to as the covering sorites. We show in the setting of second-order arithmetic that the former depends on the existence of suprema and thus on arithmetical comprehension ( $\mathsf {ACA}_0$ ) while the latter depends on the Heine–Borel theorem and thus on Weak König’s lemma ( $\mathsf {WKL}_0$ ). We finally illustrate how recursive counterexamples to these principles provide resolutions to the corresponding paradoxes which can be contrasted with supervaluationist, epistemicist, and constructivist approaches.

This paper engages the question ‘Does the consistency of a set of axioms entail the existence of a model in which they are satisfied?’ within the frame of the Frege-Hilbert controversy. The question is related historically to the formulation, proof and reception of Gödel’s Completeness Theorem. Tools from mathematical logic are then used to argue that there are precise senses in which Frege was correct to maintain that demonstrating consistency is as difficult as it can be, but also in which Hilbert was correct to maintain that demonstrating existence given consistency is as easy as it can be.

The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis that all truths are knowable entails the implausible conclusion that all truths are known. The notoriety of this argument owes to the negative light it appears to cast on the view that there can be no verification-transcendent truths. We argue that it is overly simplistic to formalize the views of contemporary verificationists like Dummett, Prawitz or Martin-Löf using the sort of propositional modal operators which are employed in the original derivation of the Paradox. Instead we propose that the central tenet of verificationism is most accurately formulated as follows: if φ is true, then there exists a proof of φ Building on the work of Artemov (Bull Symb Log 7(1): 1-36, 2001), a system of explicit modal logic with proof quantifiers is introduced to reason about such statements. When the original reasoning of the Paradox is developed in this setting, we reach not a contradiction, but rather the conclusion that there must exist non-constructed proofs. This outcome is evaluated relative to the controversy between Dummett and Prawitz about proof existence and bivalence.

The goal of this paper is to explore the significance of Montague’s paradox—that is, any arithmetical theory $T\supseteq Q$ over a language containing a predicate $P$ satisfying $P\rightarrow \varphi $ and $T\vdash \varphi \,\therefore\,T\vdash P$ is inconsistent—as a limitative result pertaining to the notions of formal, informal, and constructive provability, in their respective historical contexts. To this end, the paradox is reconstructed in a quantified extension $\mathcal {QLP}$ of Artemov’s logic of proofs. $\mathcal {QLP}$ contains both explicit modalities $t:\varphi $ and also proof quantifiers $x:\varphi $. In this system, the basis for the rule NEC is decomposed into a number of distinct principles governing how various modes of reasoning about proofs and provability can be internalized within the system itself. A conceptually motivated resolution to the paradox is proposed in the form of an argument for rejecting the unrestricted rule NEC on the basis of its subsumption of an intuitively invalid principle pertaining to the interaction of proof quantifiers and the proof-theorem relation expressed by explicit modalities.

This article bears on four topics: observational predicates and phenomenal properties, vagueness, strict finitism as a philosophy of mathematics, and the analysis of feasible computability. It is argued that reactions to strict finitism point towards a semantics for vague predicates in the form of nonstandard models of weak arithmetical theories of the sort originally introduced to characterize the notion of feasibility as understood in computational complexity theory. The approach described eschews the use of nonclassical logic and related devices like degrees of truth or supervaluation. Like epistemic approaches to vagueness, it may thus be smoothly integrated with the use of classical model theory as widely employed in natural language semantics. But unlike epistemicism, the described approach fails to imply either the existence of sharp boundaries or the failure of tolerance for soritical predicates. Applications ofmeasurement theory(in the sense of Krantz, Luce, Suppes, & Tversky (1971)) to vagueness in the nonstandard setting are also explored.

The Paradox of the Knower was originally presented by Kaplan and Montague [26] as a puzzle about the everyday notion of knowledge in the face of self-reference. The paradox shows that any theory extending Robinson arithmetic with a predicate K satisfying the factivity axiom K → A as well as a few other epistemically plausible principles is inconsistent. After surveying the background of the paradox, we will focus on a recent debate about the role of epistemic closure principles in the Knower. We will suggest this debate sheds new light on the concept of knowledge which is at issue in the paradox – i.e. is it a “thin” notion divorced from concepts such as evidence or justification, or is it a “thick” notion more closely resembling mathematical provability? We will argue that a number of features of the paradox suggest that the latter option is more plausible. Along the way, we will provide a reconstruction of the paradox using a quantified extension of Artemovʼs [2] Logic of Proofs, as well as a series of results linking the original formulation of the paradox to reflection principles for formal arithmetic. On this basis, we will argue that while the Knower can be understood to motivate a distinction between levels of knowledge, it does not provide a rationale for recognizing a uniform hierarchy of knowledge predicates in the manner suggested by Anderson.

This paper explores the relationship borne by the traditional paradoxes of set theory and semantics to formal incompleteness phenomena. A central tool is the application of the Arithmetized Completeness Theorem to systems of second-order arithmetic and set theory in which various “paradoxical notions” for first-order languages can be formalized. I will first discuss the setting in which this result was originally presented by Hilbert & Bernays (1939) and also how it was later adapted by Kreisel (1950) and Wang (1955) in order to obtain formal undecidability results. A generalization of this method will then be presented whereby Russell’s paradox, a variant of Mirimanoff’s paradox, the Liar, and the Grelling–Nelson paradox may be uniformly transformed into incompleteness theorems. Some additional observations are then framed relating these results to the unification of the set theoretic and semantic paradoxes, the intensionality of arithmetization (in the sense of Feferman, 1960), and axiomatic theories of truth.

It is commonly held that the natural numbers sequence 0, 1, 2,... possesses a unique structure. Yet by a well known model theoretic argument, there exist non-standard models of the formal theory which is generally taken to axiomatize all of our practices and intentions pertaining to use of the term “natural number.” Despite the structural similarity of this argument to the influential set theoretic indeterminacy argument based on the downward L ̈owenheim-Skolem theorem, most theorists agree that the number theoretic version does not have skeptical consequences about the reference of “natural number” analogous to the ‘relativity’ Skolem claimed pertains to notions such as “uncountable” and “cardinal.” In this paper I argue that recent proposals by Shapiro, Lavine, McGee and Field which aim to distinguish the number and set theoretic indeterminacy arguments by locating extra-mathematical constraints on the interpretation of our number theoretic vocabulary are inadequate. I then suggest that if we consider the manner in which the natural numbers figure in our computational practices – e.g. in characterizing how we compute sums and products or determine prime factorizations – it follows that our application of computational terms such as “computable function” and “tractable computational problem” indirectly uniquely determines their structure.

Proof-theoretic reflection principles are schemas which attempt to express the soundness of arithmetical theories within their own language, e.g., ${\mathtt{{Prov}_{\mathsf {PA}} \rightarrow \varphi }}$ can be understood to assert that any statement provable in Peano arithmetic is true. It has been repeatedly suggested that justification for such principles follows directly from acceptance of an arithmetical theory $\mathsf {T}$ or indirectly in virtue of their derivability in certain truth-theoretic extensions thereof. This paper challenges this consensus by exploring relationships between reflection principles and principles of mathematical and transfinite induction as well as the status of the latter with respect to various foundational characterizations of number theory.