Online research in philosophy

Provability logic is a modal logic for studying properties of provability predicates, and Interpretability logic for studying interpretability between logical theories. Their natural models are GL-models and Veltman models, for which the accessibility relation is well-founded. That’s why the usual counterexample showing the necessity of finite image property in Hennessy-Milner theorem (see [1]) doesn’t exist for them. However, we show that the analogous condition must still hold, by constructing two GL-models with worlds in them that are modally equivalent (...) but not bisimilar, and showing how these GL-models can be converted to Veltman models with the same properties. In the process we develop some useful constructions: games on Veltman models, chains, and general method of transformation from GL-models/frames to Veltman ones. (shrink)

There are many classical connections between the proof-theoretic strength of systems of arithmetic and the provable totality of recursive functions. In this paper we study the provability strength of the totality of recursive functions by investigating the degree structure induced by the relative provability order of recursive algorithms. We prove several results about this proof-theoretic degree structure using recursion-theoretic techniques such as diagonalization and the Recursion Theorem.

The provability logic of a theory $T$ is the set of modal formulas, which under any arithmetical realization are provable in $T$. We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$. We make an analogous modification for interpretability logics. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, the result is the logic of linear frames. However, for the (...) theory Primitive Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic by capitalizing on the well-studied relationship between PRA and I$\Sigma_1$. We then study interpretability logics, obtaining upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely related to linear frames. The technique is also applied to yield the nontrivial result that IL(PRA) $\subset$ ILM. (shrink)

This book, written by one of the most distinguished of contemporary philosophers of mathematics, is a fully rewritten and updated successor to the author's earlier The Unprovability of Consistency (CUP, 1979). Modal logic is concerned with the notions of necessity and possibility. What George Boolos does is to show how the concepts, techniques and methods of modal logic shed brilliant light on the most important logical discovery of the twentieth century: the incompleteness theorems of Kurt Godel and the 'self referential' (...) sentences constructed in their proof. The book explores the effects of reinterpreting the notions of necessity and possibility to near probability and consistency. It contains the first application of quantified modal logic to formal probability, and shows the results of applying modal logic to formal provability. (shrink)

Michael Redhead's recent argument aiming to show that humanly certifiable truth outruns provability is critically evaluated. It is argued that the argument is at odds with logical facts and fails.

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics (...) for Int which resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

This paper propounds a systematic examination of the link between the Knower Paradox and provability interpretations of modal logic. The aim of the paper is threefold: to give a streamlined presentation of the Knower Paradox and related results; to clarify the notion of a syntactical treatment of modalities; finally, to discuss the kind of solution that modal provability logic provides to the Paradox. I discuss the respective strength of different versions of the Knower Paradox, both in the framework (...) of first-order arithmetic and in that of modal logic with fixed point operators. It is shown that the notion of a syntactical treatment of modalities is ambiguous between a self-referential treatment and a metalinguistic treatment of modalities, and that these two notions are independent. I survey and compare the provability interpretations of modality respectively given by Skyrms, B. (1978, The Journal of Philosophy 75: 368–387) Anderson, C.A. (1983, The Journal of Philosophy 80: 338–355) and Solovay, R. (1976, Israel Journal of Mathematics 25: 287–304). I examine how these interpretations enable us to bypass the limitations imposed by the Knower Paradox while preserving the laws of classical logic, each time by appeal to a distinct form of hierarchy. (shrink)

PA is Peano Arithmetic. Pr(x) is the usual Σ1-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬ Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness. In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point (...) property and the Craig interpolation lemma. We also consider other examples of the strong provability predicates and their applications. (shrink)

(2) Vol., Classification of Propositional Provability Logics LD Beklemishev Introduction Overview. The idea of an axiomatic approach to the study of ...

In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. There (...) is often an underly ing assumption that the move to a proof of cut elimination for sequents built from multisets is easy. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of GLSV 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 formal setting is particularly important for sequents built from multisets, in order 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 diffi cult to verify the correctness of his induction argument based on “width”. In our formulation however, verification of the induction argument is straight forward. Finally, the multiset setting also introduces a new complication in the 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 show that the algorithm purporting to show the non termi nation of Valentini’s arguments is not a faithful representation of the original arguments, but is instead a transformation already known to be insufficient. (shrink)

This paper offers a justification of the ‘Hilbert-Bernays Derivability Conditions’ by considering what is required of a theory which gives an account of provability in itself.

In this paper the system IL for relative interpretability described in Visser (1988) is studied.1 In IL formulae A|> B (read: A interprets B) are added to the provability logic L. The intended interpretation of a formula A|.

In this paper the system IL for relative interpretability described in Visser (1988) is studied.1 In IL formulae A|> B (read: A interprets B) are added to the provability logic L. The intended interpretation of a formula A|> B in an (arithmetical) theory T is: T + B is relatively interpretable in T + A. The system has been shown to be sound with respect to such arithmetical interpretations (˘Svejdar 1983, Montagna 1984, Visser 1986, 1988P). As axioms for (...) IL we take the usual axioms A→ A and ( A→A)→ A (Löb's Axiom) for the provability logic L and its rules, modus ponens and necessitation, plus the axioms: (1) (A→B)→(A|>B ) (2) (A|> B) ∧ (B|> C) → (A|> C) (3) (A|> C) ∧ (B|> C)→(A∨B|> C) (4) (A|> B)→( A→ B) (5) A|>A With respect to priority of parentheses |> is treated as →. (shrink)

I present a new interpretation of Wittgenstein's later philosophy of logic and mathematics. This interpretation, like others, emphasizes Wittgenstein's attempt to reconcile platonistic and constructivistic approaches. But, unlike other interpretations, mine explains that attempt in terms of Wittgenstein's position about the relations between our concepts of necessity and provability. If what I say here is correct, then we can rescue Wittgenstein from the charge of naive relativism. For his relativism extends only to provability, and not to necessity.

The core ideas of the dialogicalapproach to modal propositional logic are explainedby means of an elementary example. Subsequently,ways of extending this approach to the system G ofso-called provability logic are checked, therebyraising the question whether the dialogician is inneed of shaping his Nichtverzögerungsregel(non-delay-rule), in order to get it sufficiently precise,in different ways for different modal systems.

In this paper the modal operator "x is provable in Peano Arithmetic" is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

Predicate modal formulas with non-modalized quantifiers (call them Q-formulas) are considered as schemata of arithmetical formulas, where is interpreted as the provability predicate of some fixed correct extension T of arithmetic. A method of constructing 1) non-provable in T and 2) false arithmetical examples for Q-formulas by Kripke-like countermodels of certain type is given. Assuming the means of T to be strong enough to solve the (undecidable) problem of derivability in QGL, the Q-fragment of the predicate version of the (...) logic GL, we prove the recursive enumerability of the sets of Q-formulas all arithmetical examples of which are: 1) T-provable, 2) true. In. particular, the first one is shown to be exactly QGL and the second one to be exactly the Q-fragment of the predicate version of Solovay's logic S. (shrink)

This article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF, cf. [14, 15]. The particular tautologies we study, the τ-formulas, are obtained from any ᵊ/poly map g; they express that a string is outside of the range of g. Maps g considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the τ-formulas for at least EF from some general, plausible computational hardness hypothesis. In (...) this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of [15]). These two properties imply the hardness of the τ-formulas from the function but unlike the hardness they are preserved under composition and iteration. We link the existence of maps with these two properties to the provability of circuit lower bounds, and we characterize maps g yielding hard τ-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing EF admits a pseudo-surjective function unless it simulates a proof system WF introduced by Jerabek [11]. an extension of EF. We propose a concrete map g as a candidate function possibly pseudo-surjective or free for strong proof systems. The map is defined as a Nisan-Wigderson generator based on a random function and on a random sparse matrix. We prove that it is iterable in a particular way in resolution, yielding the output/input ratio $n^{3-\varepsilon}$ (that improves upon a direct construction of Alekhnovich et al. [2]). (shrink)

The paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic: If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that $PA \nvdash fR$ . This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding "the predicate part" as a (...) specific addition to the standard Solovay construction. (shrink)

Provability logics with many modal operators for progressions of theories obtained by iterating their consistency statements are introduced. The corresponding arithmetical completeness theorem is proved.

Predicate modal formulas are considered as schemata of arithmetical formulas, where is interpreted as the standard formula of provability in a fixed sufficiently rich theory T in the language of arithmetic. QL T(T) and QL T are the sets of schemata of T-provable and true formulas, correspondingly. Solovay's well-known result — construction an arithmetical counterinterpretation by Kripke countermodel — is generalized on the predicate modal language; axiomatizations of the restrictions of QL T(T) and QL T by formulas, which contain (...) no variables different from x, are given by means of decidable prepositional bimodal systems; under the assumption that T is 1-complete, there is established the enumerability of the restrictions of QL T(T) and QL T by: 1) formulas in which the domains of different occurrences of don't intersect and 2) formulas of the form n A. (shrink)

This paper concerns modal logics of provability — Gödel-Löb systemGL and Solovay logicS — the smallest and the greatest representation of arithmetical theories in propositional logic respectively. We prove that the decision problem for admissibility of rules (with or without parameters) inGL andS is decidable. Then we get a positive solution to Friedman''s problem forGL andS. We also show that A. V. Kuznetsov''s problem of the existence of finite basis for admissible rules forGL andS has a negative solution. Afterwards (...) we give an algorithm deciding the solvability of logical equations inGL andS and constructing some solutions. (shrink)

Lucas and Redhead ([2007]) announce that they will defend the views of Redhead ([2004]) against the argument by Panu Raatikainen ([2005]). They certainly re-state the main claims of Redhead ([2004]), but they do not give any real arguments in their favour, and do not provide anything that would save Redhead’s argument from the serious problems pointed out in (Raatikainen [2005]). Instead, Lucas and Redhead make a number of seemingly irrelevant points, perhaps indicating a failure to understand the logico-mathematical points at (...) issue. (shrink)

The views of Redhead ([2004]) are defended against the argument by Panu Raatikainen ([2005]). The importance of informal rigour is canvassed, and the argument for the a priori nature of induction is explained. The significance of Gödel's theorem is again rehearsed.

Conservativeness has been proposed as an important requirement for deflationary truth theories. This in turn gave rise to the so-called ‘conservativeness argument’ against deflationism: a theory of truth which is conservative over its base theory S cannot be adequate, because it cannot prove that all theorems of S are true. In this paper we show that the problems confronting the deflationist are in fact more basic: even the observation that logic is true is beyond his reach. This seems to conflict (...) with the deflationary characterization of the role of the truth predicate in proving generalizations. However, in the final section we propose a way out for the deflationist — a solution that permits him to accept a strong theory, having important truth-theoretical generalizations as its theorems. (shrink)

We investigate what happens when ‘truth’ is replaced with ‘provability’ in Yablo’s paradox. By diagonalization, appropriate sequences of sentences can be constructed. Such sequences contain no sentence decided by the background consistent and sufficiently strong arithmetical theory. If the provability predicate satisfies the derivability conditions, each such sentence is provably equivalent to the consistency statement and to the Gödel sentence. Thus each two such sentences are provably equivalent to each other. The same holds for the arithmetization of the (...) existential Yablo paradox. We also look at a formulation which employs Rosser’s provability predicate. (shrink)

According to the received view, formalism – interpreted as the thesis that mathematical truth does not outrun the consequences of our maximal mathematical theory – has been refuted by Goedel's theorem. In support of this claim, proponents of the received view usually invoke an informal argument for the truth of the Goedel sentence, an argument which is supposed to reconstruct our reasoning in seeing its truth. Against this, Field has argued in a series of papers that the principles involved in (...) this argument – when applied to our maximal mathematical theory – are unsound. This paper defends the received view by showing that there is a way of seeing the truth of the Goedel sentence which is immune to Field's strategy. (shrink)

We present a quite simple proof of the fixed point theorem for GL. We also use this proof to show that Sambin's algorithm yields a fixed point.

Given an argumentation network we associate with it a modal formula representing the ‘logical content’ of the network. We show a one-to-one correspondence between all possible complete Caminada labellings of the network and all possible models of the formula.

Cieslinski has given an interesting response to Shapiro 1998 and Ketland 1999, which argued that deflationary truth theories are inadequate, since they lack the property of ‘reflective adequacy’. Cieslinski’s response, following Tennant (2002, 2005), aims to explain, without a detour using truth axioms, why someone who accepts the axioms of a theory should also accept its reflection principles. The argument is formulated very clearly (in fact, to justify a different reflection principle), and involves a couple of important assumptions, the crucial (...) one being that the reflection scheme for a theory ‘expresses’ the acceptance of its theorems. I argue that this assumption is incorrect. For if the reflection principle for a theory expresses the claim that one is ready to accept its theorems, this latter claim should imply the reflection principle. But it does not. So, I conclude, the response fails to yield the required ‘truth-free’ method for proving or justifying reflection principles. (shrink)

Lucas and Redhead ([2007]) announce that they will defend the views of Redhead ([2004]) against the argument by Panu Raatikainen ([2005]). They certainly re-state the main claims of Redhead ([2004]), but they do not give any real arguments in their favour, and do not provide anything that would save Redhead’s argument from the serious problems pointed out in (Raatikainen [2005]). Instead, Lucas and Redhead make a number of seemingly irrelevant points, perhaps indicating a failure to understand the logico-mathematical points at (...) issue. (shrink)

New epistemic principles are formulated in the language of Shapiros system of Epistemic Arithmetic. It is argued that some plausibility can be attributed to these principles. The relations between these principles and variants of controversial constructivistic principles are investigated. Special attention is given to variants of the intuitionistic version of Churchs thesis and to variants of Markovs principle.

For every finite n ≥ 4 there is a logically valid sentence φ n with the following properties: φ n contains only 3 variables (each of which occurs many times); φ n contains exactly one nonlogical binary relation symbol (no function symbols, no constants, and no equality symbol): φ n has a proof in first-order logic with equality that contains exactly n variables, but no proof containing only n - 1 variables. This result was first proved using the machinery of (...) algebraic logic developed in several research monographs and papers. Here we replicate the result and its proof entirely within the realm of (elementary) first-order binary predicate logic with equality. We need the usual syntax, axioms, and rules of inference to show that φ n has a proof with only n variables. To show that φ n has no proof with only n - 1 variables we use alternative semantics in place of the usual, standard, set-theoretical semantics of first-order logic. (shrink)

We give a self-contained and streamlined version of the classification of the provably computable functions of PA. The emphasis is put on illuminating as well as seems possible the intrinsic computational character of the standard cut elimination process. The article is intended to be suitable for teaching purposes and just requires basic familiarity with PA and the ordinals below ε0. (Familiarity with a cut elimination theorem for a Gentzen or Tait calculus is helpful but not presupposed).

In this article we show how to extract with the use of the Buchholz-Cichon-Weiermann approach to subrecursive hierarchies from Rathjen's 1991 ordinal analysis of KPM a characterization of the provably total number-theoretic functions of KPM and some of its (most prominent) subsystems in a uniform and direct way.

Inspired by Pohlers' proof-theoretic analysis of KPω we give a straightforward non-metamathematical proof of the (well-known) classification of the provably total functions of $PA, PA + TI(\prec\lceil)$ (where it is assumed that the well-ordering $\prec$ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.

In this paper we continue, from [2], the development of provably recursive analysis, that is, the study of real numbers defined by programs which can be proven to be correct in some fixed axiom system S. In particular we develop the provable analogue of an effective operator on the set C of recursive real numbers, namely, a provably correct operator on the set P of provably recursive real numbers. In Theorems 1 and 2 we exhibit a provably correct operator on (...) P which is discontinuous at 0; we thus disprove the analogue of the Ceitin-Moschovakis theorem of recursive analysis, which states that every effective operator on C is (effectively) continuous. Our final theorems show, however, that no provably correct operator on P can be proven (in S) to be discontinuous. (shrink)

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

Preface 1 The First Theorem revisited 1.1 Notational preliminaries 1.2 Definitional preliminaries 1.3 A general version of G¨ odel’s First Theorem 1.4 Giving the First Theorem bite 1.5 Generic G¨ odel sentences and arithmetic truth 1.6 Canonical and standard G¨ odel sentences 2 The Second Theorem revisited 2.1 Definitional preliminaries 2.2 Towards G¨ odel’s Second Theorem 2.3 A general version of G¨ odel’s Second Theorem 2.4 Giving the Second Theorem bite 2.5 Comparisons 2.6 Further results about provability predicates 2.7 (...) Back to the First Theorem 2.8 Introducing Rosserized provability predicates.. (shrink)

The aim of this paper is to provide epistemic reasons for investigating the notions of informal rigour and informal provability. I argue that the standard view of mathematical proof and rigour yields an implausible account of mathematical knowledge, and falls short of explaining the success of mathematical practice. I conclude that careful consideration of mathematical practice urges us to pursue a theory of informal provability.

According to Edmund Husserl in the Prolegomena to Pure Logic, which constitutes the preliminary rational foundation for – and also the entire first volume of – his Logical Investigations, pure logic is the a priori theoretical, nomological science of „demonstration“ (LI 1, 57; Hua XVIII, 23).1 For him, demonstration includes both consequence and provability. Consequence is the defining property of all and only formally valid arguments, (...) i. e., arguments that cannot lead from true premises to false conclusions. And provability (a. k. a. „completeness“) is the property of a logical system such that, for every truth of logic in that system, there is, at least in principle, a rigorous step-by-step logically valid procedure demonstrating its validity according to strictly universal, ideal, and necessary logical laws. In this way, the laws of pure logic completely determine its internal structure. Moreover, these laws and these proofs are all knowable a priori, with selfevident insight (LI 1, 196; Hua XVIII, 185–195). So not only is pure logic independent of any other theoretical science, in that it requires no other science in order to ground its core notion of demonstration, it also provides both epistemic and semantic foundations for every other theoretical science, as well as every practical discipline or „technology.“ To the extent that pure logic is the foundation of every other.. (shrink)

Three clusters of philosophically significant issues arise from Frege's discussions of definitions. First, Frege criticizes the definitions of mathematicians of his day, especially those of Weierstrass and Hilbert. Second, central to Frege's philosophical discussion and technical execution of logicism is the so-called Hume's Principle, considered in The Foundations of Arithmetic . Some varieties of neo-Fregean logicism are based on taking this principle as a contextual definition of the operator 'the number of …', and criticisms of such neo-Fregean programs sometimes appeal (...) to Frege's objections to contextual definitions in later writings. Finally, a critical question about the definitions on which Frege's proofs of the laws of arithmetic depend is whether the logical structures of the definientia reflect our pre-Fregean understanding of arithmetical terms. It seems that unless they do, it is unclear how Frege's proofs demonstrate the analyticity of the arithmetic in use before logicism. Yet, especially in late writings, Frege characterizes the definitions as arbitrary stipulations of the senses or references of expressions unrelated to pre-definitional understanding. One or more of these topics may be studied in a survey course in the philosophy of mathematics or a course on Frege's philosophy. The latter two topics are obviously central in a seminar in the philosophy of mathematics in general or more specialized seminars on logicism, or on mathematical definitions and concept formation. Author Recommends: 1. Kant, Immanuel. Critique of Pure Reason . Trans. P. Guyer and A. Wood. Cambridge: Cambridge University Press, 1999 [1781, 1787], A7-10/B11-14, A151/B190. In the first Critique , Kant appears to give four distinct accounts of analytic judgments. The initial famous account explains analyticity in terms of the predicate-concept belonging to the subject-concept (A6–7/B11). In this passage, we also find an account of establishing analytic judgments on the basis of conceptual containments and the principle of non-contradiction. (The other accounts are in terms of 'identity' (A7/B1l), in terms of the explicative–ampliative contrast (A7/B11), and by reference to the notion of 'cognizability in accordance with the principle of contradiction' (A151/B190).) 2. Frege, Gottlob. The Foundations of Arithmetic . Trans. J. L. Austin. 2nd ed. Evanston, IL: Northwestern University Press, 1980 [1884], especially sections 1–4, 87–91. Frege here criticizes and reformulates Kant's account of analyticity. Central to Frege's account is the provability of an analytic statement on the basis of (Frege's) logic and definitions that express analyses of (mathematical, especially arithmetical) concepts. 3. Frege, Gottlob. Review of E. G. Husserl. 'Philosophie der Arithmetik I [1894],' in Frege, Collected Papers . Ed. B. McGuinness. Trans. M. Black et al. Oxford: Blackwell, 1984. 195–209. In this review, Frege responds to Husserl's charge that Frege's definitions fail to capture our intuitive pre-analytic arithmetical concepts by claiming that the adequacy of mathematical definitions is measured, not by their expressing the same senses, but merely by their having the same references, as pre-definitional vocabulary. It follows not only that Husserl's criticism is unfounded, but also that there can be alternative, equally legitimate, definitions of mathematical terms. 4. Frege, 'Logic in Mathematics,' in Frege, Posthumous Writings . Trans. P. Long and R. White. Oxford: Blackwell, 1979 [1914]. 203–50. These are a set of lecture notes including, among other things, an account of proper definitions as mere abbreviation of complex signs by simple ones, in contrast to definitions which purport to express the analyses of existing concepts. Frege here claims that if there is any doubt whether a definition purporting to express an analysis succeeds in capturing the senses of the pre-definitional expressions, then the definition fails as an analysis, and should be regarded as the introduction of an entirely new expression abbreviating the definiens . 5. Picardi, Eva. 'Frege on Definition and Logical Proof,' Temi e Prospettive della Logica e della Filosofia della Scienza Contemporanee . i vol. Eds. C. Cellucci and G. Sambin. Bologna: Cooperativa Libraria Universitaria Editrice Bologna, 1988. 227–30. Picardi sets out forcefully the view that unless Frege's definitions capture the meanings of existing arithmetical terms, his logicism cannot have the epistemological significance he takes it to have. 6. Dummett, Michael. 'Frege and the Paradox of Analysis,' in Dummett, Frege and other Philosophers . Oxford: Oxford University Press, 1991. 17–52. Dummett agrees with Picardi's view and analyzes the philosophical pressures that led Frege to the account of definition in 'Logic in Mathematics.' Especially significant is Dummett's claim of the centrality of the transparency of sense – that if one grasps the senses of any two expressions, one must know whether they have the same sense – in Frege's account. 7. Benacerraf, Paul. 'Frege: The Last Logicist,' Midwest Studies in Philosophy . vol. 6. Eds. P. French, T. Uehling, and H. Wettstein. Minneapolis: University of Minnesota Press, 1981. 17–35. Frege's aims, on Benacerraf's reading, are primarily mathematical. Frege was interested in traditional philosophical issues such as the analyticity of arithmetic only to the extent that they can be exploited for the mathematical goal of proving previously unproven arithmetical statements. Hence, Frege never had any serious interest in or need for showing that his definitions of arithmetical terms reflect existing arithmetical conceptions. 8. Weiner, Joan. 'The Philosopher Behind the Last Logicist,' in Frege: Tradition and Influence . Ed. C. Wright. Oxford: Blackwell, 1984. 57–79. Weiner argues that on Frege's view, prior to his definitions of arithmetical terms the references of such expressions are in fact not known by those who use arithmetical vocabulary. Thus, in Foundations , Frege operated with a 'hidden agenda' (263) namely, replacing existing arithmetic with a new science based on stipulative definitions that assign new senses to key arithmetical terms. 9. Tappenden, Jamie. 'Extending Knowledge and 'Fruitful Concepts': Fregean Themes in the Foundations of Mathematics.' Noûs 29 (1995): 427–67. Tappenden argues that Frege takes his crucial innovation over previous practices and accounts of mathematical concept formation to be the role of quantificational structure made possible by his logical discoveries. 10. Horty, John. Frege on Definitions: A Case Study of Semantic Content . Oxford: Oxford University Press, 2007. A useful interpretation of Frege's views of definition, together with suggestive extensions for resolving the issues framing Frege's views. 11. Shieh, Sanford. 'Frege on Definitions,' Philosophy Compass 3/5 (2008): 992–1012. A more detailed account of Frege's views on definition and the philosophical issues they raise, surveying and discussing critically the main substantive and interpretive issues. Online Materials On Frege http://plato.stanford.edu/entries/frege/ On the Paradox of Analysis http://plato.stanford.edu/entries/analysis/ Sample Syllabus The following is a 3-week module that can be incorporated into fairly focused historically oriented graduate-level seminars on logicism or on the paradox of analysis. It is also possible to compress the material into 2 weeks in an undergraduate or graduate class Frege's thought in general. Week I: Background, Kant on Analyticity; Definition in Foundations , Review of Husserl, and 'Logic in Mathematics' Readings Kant, Immanuel. Critique of Pure Reason , A7–10/B11–14. Frege, Gottlob. The Foundations of Arithmetic , sections 1–4, 87–91. Frege, Gottlob. Review of E. G. Husserl, Philosophie der Arithmetik I. Frege, Gottlob. 'Logic in Mathematics.' Optional Proops, Ian. 'Kant's Conception of Analytic Judgment,' Philosophy and Phenomenological Research LXX, 3 (2005): 588–612. Week II: The Supposed Paradox of Analysis, Picardi and Dummett; Bypassing Traditional Epistemological Issues About Mathematics, Benacerraf Readings Picardi, Eva. 'Frege on Definition and Logical Proof.' Dummett, Michael. 'Frege and the Paradox of Analysis.' Benacerraf, Paul. 'Frege: The Last Logicist.' Optional Tappenden, Jamie. 'Extending Knowledge and 'Fruitful Concepts': Fregean Themes in the Foundations of Mathematics.' Week III: Weiner's Hidden Agenda Interpretation Readings Weiner, Joan. 'The Philosopher Behind the Last Logicist.' Optional Weiner, Joan. Frege in Perspective . Ithaca, NY: Cornell University Press, 1990. Focus Questions 1. To what extent is Frege's account of analyticity in Foundations a rejection, and to what extent an updating, of Kant's view of analyticity? 2. According to Picardi it 'would be incomprehensible' how Frege's proofs tells us anything about the arithmetic we already have unless his 'definitions [are] somehow responsible to the meaning of [arithmetical] sentences as these are understood' (228). Why does she hold this? Why does Dummett agree with her? Do you think Frege's logicism needs to address this worry? 3. What are the major differences and continuities in Frege's discussions of definition in mathematics in Foundations , the review of Husserl and 'Logic in Mathematics'? 4. Frege writes that definitions must prove their worth by being fruitful. He also says that nothing can be proven using a proper definition that cannot be proven without it. Are these claims consistent? Why or why not? 5. Weiner held that in Foundations Frege had 'hidden agenda.' What, according to her, is this agenda? How does this fit with Frege's later views of definition? 6. What are Frege's main complaints about Weierstrass's definitions in 'Logic in Mathematics'? Are these criticisms consistent with Frege's account of 'definition proper' in the same text? Seminar/Project Ideas What, if anything, is the relation between Frege's critique of Hilbert's use of definitions and Frege's later views of definitions? (shrink)

The modal logic of Gödel sentences, termed as GS , is introduced to analyze the logical properties of ‘true but unprovable’ sentences in formal arithmetic. The logic GS is, in a sense, dual to Grzegorczyk’s Logic, where modality can be interpreted as ‘true and provable’. As we show, GS and Grzegorczyk’s Logic are, in fact, mutually embeddable. We prove Kripke completeness and arithmetical completeness for GS . GS is also an extended system of the logic of ‘Essence and Accident’ proposed (...) by Marcos (Bull Sect Log 34(1):43–56, 2005 ). We also clarify the relationships between GS and the provability logic GL and between GS and Intuitionistic Propositional Logic. (shrink)

It might seem that three of Godel’s results - the Completeness and the First and Second Incompleteness Theorems - assume so little that they are reasonably indisputable. A version of the Completeness Theorem, for instance, can be proven in RCA0, which is the weakest system studied extensively in Simpson’s encyclopaedic Subsystems of Second Order Arithmetic. And it often seems that the minimum requirements for a system just to express the Incompleteness Theorems are sufficient to prove them. However, it will be (...) shown that a particular sub-system of Peano Arithmetic is powerful enough to express assertions about syntax, provability, consistency, and models, while being too weak to allow the standard proofs of the theorems to go through. An alternative proof is available for the First Incompleteness Theorem, but is of such a different nature that the import of the theorem changes. And there are no alternative proofs for (certainly) the Completeness and (apparently) the Second Incompleteness Theorems. It is therefore perfectly rational for someone to be skeptical about Godel’s results. (shrink)

This paper replies to Nanay’s response to my recent paper. My suggestions are the following. First, “should” or “ought” does not need to be deontic. Second, etiological theories of function, like provability logic, do not need to attribute modal force to their explanans. Third, the explanans of the homological account of trait type individuation does not appeal to a trait’s etiological function, that is, what a trait should or ought to do. Finally, my reference to Cummins’s notion of function (...) was intended to note that the homological account is permitted to use this non-etiological notion of function. (shrink)

Truth’s universal knowability entails its discovery. This threatens antirealism, which is thought to require it. Fortunately, antirealism is not committed to it. Avoiding it requires adoption (and extension) of Dag Prawitz’s position in his long-term disagreement with Michael Dummett on the notion of provability involved in intuitionism’s identification of it with truth. Antirealism (intuitionism generalized) must accommodate a notion of lost-opportunity truth (a kind of recognition-transcendent truth), and even truth consisting in the presence of unperformable verifications. Dummett’s position cannot (...) abide this, while Prawitz’s can. Antirealism’s epistemic notion of truth derives from general features of its meaning theory, not from a universal knowability principle. (shrink)

Some systems of modal logic, such as S5, which are often used as epistemic logics with the ‘necessity’ operator read as ‘the agent knows that’, are problematic as general epistemic logics for agents whose computational capacity does not exceed that of a Turing machine because they impose unwarranted constraints on the agent’s theory of non-epistemic aspects of the world, for example by requiring the theory to be decidable rather than merely recursively axiomatizable. To generalize this idea, two constraints on an (...) epistemic logic are formulated: r.e. conservativeness, that any recursively enumerable theory R in the sublanguage without the epistemic operator is conservatively extended by some recursively enumerable theory in the language with the epistemic operator which is permitted by the logic to be the agent’s overall theory; the weaker requirement of r.e. quasi-conservativeness is similar except for applying only when R is consistent. The logic S5 is not even r.e. quasiconservative; this result is generalized to many other modal logics. However, it is also proved that the modal logics S4, Grz and KDE are r.e. quasi-conservative and that K4, KE and the provability logic GLS are r.e. conservative. Finally, r.e. conservativeness and r.e. quasiconservativeness are compared with related non-computational constraints. (shrink)

The uniform reflection principle for the theory of uniform T-sentences is added to PA. The resulting system is justified on the basis of a disquotationalist theory of truth where the provability predicate is conceived as a special kind of analyticity. The system is equivalent to the system ACA of arithmetical comprehension. If the truth predicate is also allowed to occur in the sentences that are inserted in the T-sentences, yet not in the scope of negation, the system with the (...) reflection schema for these T-sentences assumes the strength of the Kripke-Feferman theory KF, and thus of ramified analysis up to go. (shrink)

Full proofs of the Gödel incompleteness theorems are highly intricate affairs. Much of the intricacy lies in the details of setting up and checking the properties of a coding system representing the syntax of an object language (typically, that of arithmetic) within that same language. These details are seldom illuminating and tend to obscure the core of the argument. For this reason a number of efforts have been made to present the essentials of the proofs of Gödel’s theorems without getting (...) mired in syntactic or computational details. One of the most important of these efforts was made by Löb [8] in connection with his analysis of sentences asserting their own provability. Löb formulated three conditions (now known as the Hilbert-Bernays-Löb derivability conditions), on the provability predicate in a formal system which are jointly sufficient to yield the Gödel’s second incompleteness theorem for it. A key role in Löb’s analysis is played by (a special case of) what later became known as the diagonalization or fixed point property of formal systems, a property which had already, in essence, been exploited by Gödel in his original proofs of the incompleteness theorems. The fixed point property plays a central role in Lawvere’s [7] category-theoretic account of incompleteness phenomena (see also [10]). Incompleteness theorems have also been subjected to intensive investigation within the framework of modal logic (see, e.g.[4], [5]). In this formulation the modal operator takes up the role previously played by the provability predicate, and the derivability conditions on the latter are translated into algebraic conditions (the so-called GL, i.e., Gödel–Löb, conditions) on the former. My purpose here is to present a framework for incompleteness phenomena, fully compatible with intuitionistic or constructive principles, in which the idea of a coding system is retained, only in a 2 simple, but very general form, a form wholly free of syntactical notions. As codes we shall take the elements of an arbitrary given nonempty set, possibly, but not necessarily, the set of natural numbers.. (shrink)

This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

Anti-realistic conceptions of truth and falsity are usually epistemic or inferentialist. Truth is regarded as knowability, or provability, or warranted assertability, and the falsity of a statement or formula is identified with the truth of its negation. In this paper, a non-inferentialist but nevertheless anti-realistic conception of logical truth and falsity is developed. According to this conception, a formula (or a declarative sentence) A is logically true if and only if no matter what is told about what is told (...) about the truth or falsity of atomic sentences, A always receives the top-element of a certain partial order on non-ontic semantic values as its value. The ordering in question is a told-true order. Analogously, a formula A is logically false just in case no matter what is told about what is told about the truth or falsity of atomic sentences, A always receives the top-element of a certain told-false order as its value. Here, truth and falsity are pari passu , and it is the treatment of truth and falsity as independent of each other that leads to an informational interpretation of these notions in terms of a certain kind of higher-level information. (shrink)

In his paper "Finitism" (1981), W.W. Tait maintains that the chief difficulty for everyone who wishes to understand Hilbert's conception of finitist mathematics is this: to specify the sense of the provability of general statements about the natural numbers without presupposing infinite totalities. Tait further argues that all finitist reasoning is essentially primitive recursive. In this paper, we attempt to show that his thesis "The finitist functions are precisely the primitive recursive functions" is disputable and that another, likewise defended (...) by him, is untenable. The second thesis is that the finitist theorems are precisely the universal closures of the equations that can be proved in PRA. /// En su articulo "Finitism" (1981), W.W. Tait sostiene que la dificultad principal para quien quiere comprender la concepción hilbertiana de la matemática finitista es ésta: especificar el sentido de la demostrabilidad de enunciados generales sobre los números naturales sin presuponer totalidades infinitas. Además, Tait argumenta que todo razonamiento finitista es esencialmente primitivo recursivo. En este artículo tratamos de mostrar que su tesis "Las funciones finitistas son precisamente las funciones primitivas recursivas" es discutible y que otra, también defendida por él, resulta insostenible. La segunda tesis es que los teoremas finitistas son precisamente las clausuras universales de las ecuaciones que pueden demostrarse en PRA. (shrink)

A well-known problem with Hintikka-style logics of knowledge is that of logical omniscience. One knows too much. This breaks down into two subproblems: one knows all tautologies, and one’s knowledge is closed under consequence. A way of addressing the second of these is to move from knowledge simpliciter, to knowledge for a reason. Then, as consequences become ‘further away’ from one’s basic knowledge, reasons for them become more complex, thus providing a kind of resource measurement. One kind of reason is (...) a formal proof. Sergei Artemov has introduced a logic of explicit proofs, LP. I present a semantics for this, based on the idea that it is a logic of knowledge with explicit reasons. A number of fundamental facts about LP can be established using this semantics. But it is equally important to realize that it provides a natural logic of more general applicability than its original provenance, arithmetic provability. (shrink)