We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular (...) logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result. (shrink)

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom andqa (...) new extension atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system. (shrink)

We extend results of Bonet, Buss and Pitassi on Bondy’s Theorem and of Nozaki, Arai and Arai on Bollobás’ Theorem by proving that Frankl’s Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parametert, we prove that Frankl’s Theorem has polynomial size AC0-Frege proofs from instances of the pigeonhole principle.

Sam Buss produced the first polynomial size Frege proof of thepigeonhole principle. We introduce a variation of that problem and producea simpler proof based on parity. The proof appearing here has an upperbound that is quadratic in the size of the input formula.

The first complete English translation of a groundbreaking work. An ambitious account of the relation of mathematics to logic. Includes a foreword by Crispin Wright, translators' Introduction, and an appendix on Frege's logic by Roy T. Cook. The German philosopher and mathematician Gottlob Frege (1848-1925) was the father of analytic philosophy and to all intents and purposes the inventor of modern logic. Basic Laws of Arithmetic, originally published in German in two volumes (1893, 1903), is Freges magnum opus. (...) It was to be the pinnacle of Freges lifes work. It represents the final stage of his logicist project the idea that arithmetic and analysis are reducible to logic and contains his mature philosophy of mathematics and logic. The aim of Basic Laws of Arithmetic is to demonstrate the logical nature of mathematical theorems by providing gapless proofs in Frege's formal system using only basic laws of logic, logical inference, and explicit definitions. The work contains a philosophical foreword, an introduction to Frege's logic, a derivation of arithmetic from this logic, a critique of contemporary approaches to the real numbers, and the beginnings of a logicist treatment of real analysis. As is well-known, a letter received from Bertrand Russell shortly before the publication of the second volume made Frege realise that his basic law V, governing the identity of value-ranges, leads into inconsistency. Frege discusses a revision to basic law V written in response to Russells letter in an afterword to volume II. The continuing importance of Basic Laws of Arithmetic lies not only in its bearing on issues in the foundations of mathematics and logic but in its model of philosophical inquiry. Frege's ability to locate the essential questions, his integration of logical and philosophical analysis, and his rigorous approach to criticism and argument in general are vividly in evidence in this, his most ambitious work. Philip Ebert and Marcus Rossberg present the first full English translation of both volumes of Freges major work preserving the original formalism and pagination. The edition contains a foreword by Crispin Wright and an extensive appendix providing an introduction to Frege's formal system by Roy T. Cook. Readership: Scholars and advanced students in philosophy of logic, philosophy of mathematics, and early analytic philosophy. (shrink)

The paper considers a commonly used axiomatization of the classical propositional logic and studies how different axiom schemata in this system contribute to proof complexity of the logic. The existence of a polynomial bound on proof complexity of every statement provable in this logic is a well-known open question.The axiomatization consists of three schemata. We show that any statement provable using unrestricted number of axioms from the first of the three schemata and polynomially-bounded in size set of axioms from the (...) other schemata, has a polynomially-bounded proof complexity. In addition, it is also established, that any statement, provable using unrestricted number of axioms from the remaining two schemata and polynomially-bounded in size set of axioms from the first scheme, also has a polynomially-bounded proof complexity. (shrink)

We prove that for sufficiently large \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $n$\end{document}, there are tautologies of size \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $O(n)$\end{document} that require proofs containing \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\Omega( n / \log n )$\end{document} lines in axiomatic systems of propositional logic based on the rules of substitution and detachment.

Frege's account of indirect proof has been thought to be problematic. This thought seems to rest on the supposition that some notion of logical consequence ? which Frege did not have ? is indispensable for a satisfactory account of indirect proof. It is not so. Frege's account is no less workable than the account predominant today. Indeed, Frege's account may be best understood as a restatement of the latter, although from a higher order point of view. (...) I argue that this ascent is motivated by Frege's conception of logic. (shrink)

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.

I present a novel interpretation of Frege’s attempt at Grundgesetze I §§29-31 to prove that every expression of his language has a unique reference. I argue that Frege’s proof is based on a contextual account of reference, similar to but more sophisticated than that enshrined in his famous Context Principle. Although Frege’s proof is incorrect, I argue that the account of reference on which it is based is of potential philosophical value, and I analyze the class of (...) cases to which it may successfully be applied. (shrink)

It is widely believed that some puzzling and provocative remarks that Frege makes in his late writings indicate he rejected independence arguments in geometry, particularly arguments for the independence of the parallels axiom. I show that this is mistaken: Frege distinguished two approaches to independence arguments and his puzzling remarks apply only to one of them. Not only did Frege not reject independence arguments across the board, but also he had an interesting positive proposal about the logical (...) structure of correct independence arguments, deriving from the geometrical principle of duality and the associated idea of substitution invariance. The discussion also serves as a useful focal point for independently interesting details of Frege's mathematical environment. This feeds into a currently active scholarly debate because Frege's supposed attitude to independence arguments has been taken to support a widely accepted thesis (proposed by Ricketts among others) concerning Frege's attitude toward metatheory in general. I show that this thesis gains no support from Frege's puzzling remarks about independence arguments. (shrink)

ABSTRACTIn this paper, we present a generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems and which augment Avron's Frege system HŁuk with nested and general versions of the disjunction elimination rule, respectively. For these systems, we provide upper bounds on speed-ups w.r.t. both the number of steps (...) in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus GŁuk for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. (shrink)

In this article, I try to shed some new light onGrundgesetze§10, §29–§31 with special emphasis on Frege’s criteria and proof of referentiality and his treatment of the semantics of canonical value-range names. I begin by arguing against the claim, recently defended by several Frege scholars, that the first-order domain inGrundgesetzeis restricted to value-ranges, but conclude that there is an irresolvable tension in Frege’s view. The tension has a direct impact on the semantics of the concept-script, not least (...) on the semantics of value-range names. I further argue that despite first appearances truth-value names play a distinguished role as semantic “target names” for “test names” in the criteria of referentiality and do not figure themselves as “test names” regarding referentiality. Accordingly, I show in detail that Frege’s attempt to demonstrate that by virtue of his stipulations “regular” value-range names have indeed been endowed with a unique reference, can plausibly be regarded as a direct application of the context principle. In a subsequent section, I turn to some special issues involved in §10. §10 is closely intertwined with §31 and in my and Richard Heck’s view would have been better positioned between §30 and §31. In a first step, I discuss the piecemeal strategy which Frege applies when he attempts to bestow a unique reference on value-range names in §3, §10–§12. In a second step, I critically analyze his tentative, but predictably unsuccessful proposal to identify all objects whatsoever, including those already clad in the garb of value-ranges, with their unit classes. In conclusion, I present two arguments for my claim that Frege’s identification of the True and the False with their unit classes in §10 is illicit even if both the permutation argument and the identifiability thesis that he states in §10 are regarded as formally sound. The first argument is set out from the point of view of the syntax of his formal language. It suggests though that a reorganization of the exposition of the concept-script would have solved at least one of the problems to which the twin stipulations in §10 give rise. The second argument rests on semantic considerations. If it is sound, it may call into question, if not undermine the legitimacy of the twin stipulations. (shrink)

In this paper, we explore Fregean metatheory, what Frege called the New Science. The New Science arises in the context of Frege’s debate with Hilbert over independence proofs in geometry and we begin by considering their dispute. We propose that Frege’s critique rests on his view that language is a set of propositions, each immutably equipped with a truth value (as determined by the thought it expresses), so to Frege it was inconceivable that axioms could (...) even be considered to be other than true. Because of his adherence to this view, Frege was precluded from the sort of metatheoretical considerations that were available to Hilbert; but from this, we shall argue, it does not follow that Frege was blocked from metatheory in toto. Indeed, Frege suggests in Die Grundlagen der Geometrie a metatheoretical method for establishing independence proofs in the context of the New Science. Frege had reservations about the method, however, primarily because of the apparent need to stipulate the logical terms, those terms that must be held invariant to obtain such proofs. We argue that Frege’s skepticism on this score is not warranted, by showing that within the New Science a characterization of logical truth and logical constant can be obtained by a suitable adaptation of the permutation argument Frege employs in indicating how to prove independence. This establishes a foundation for Frege’s metatheoretical method of which he himself was unsure, and allows us to obtain a clearer understanding of Frege’s conception of logic, especially in relation to contemporary conceptions. (shrink)

Gottlob Frege's Grundgesetze der Arithmetik, or Basic Laws of Arithmetic, was intended to be his magnum opus, the book in which he would finally establish his logicist philosophy of arithmetic. But because of the disaster of Russell's Paradox, which undermined Frege's proofs, the more mathematical parts of the book have rarely been read. Richard G.

Sections “Introduction: Hume’s Principle, Basic Law V and Cardinal Arithmetic” and “The Julius Caesar Problem in Grundlagen—A Brief Characterization” are peparatory. In Section “Analyticity”, I consider the options that Frege might have had to establish the analyticity of Hume’s Principle, bearing in mind that with its analytic or non-analytic status the intended logical foundation of cardinal arithmetic stands or falls. Section “Thought Identity and Hume’s Principle” is concerned with the two criteria of thought identity that Frege states in (...) 1906 and their application to Hume’s Principle. In Section “The Nature ofion: A Critical Assessment of Grundlagen, §64”, I scrutinize Frege’s characterization of abstraction in Grundlagen, §64 and criticize in this context the currently widespread use of the terms “recarving” and “reconceptualization”. Section “Frege’s Proof of Hume’s Principle” is devoted to the formal details of Frege’s proof of Hume’s Principle. I begin by considering his proof sketch in Grundlagen and subsequently reconstruct in modern notation essential parts of the formal proof in Grundgesetze. In Section “Equinumerosity and Coextensiveness: Hume’s Principle and Basic Law V Again”, I discuss the criteria of identity embodied in Hume’s Principle and in Basic Law V, equinumerosity and coextensiveness. In Section “Julius Caesar and Cardinal Numbers—A Brief Comparison Between Grundlagen and Grundgesetze ”, I comment on the Julius Caesar problem arising from Hume’s Principle in Grundlagen and analyze the reasons for its absence in this form in Grundgesetze. I conclude with reflections on the introduction of the cardinals and the reals by abstraction in the context of Frege’s logicism. (shrink)

Gottlob Frege famously rejects the methodology for consistency and independence proofs offered by David Hilbert in the latter's Foundations of Geometry. The present essay defends against recent criticism the view that this rejection turns on Frege's understanding of logical entailment, on which the entailment relation is sensitive to the contents of non-logical terminology. The goals are (a) to clarify further Frege's understanding of logic and of the role of conceptual analysis in logical investigation, and (b) to (...) point out the extent to which his understanding of logic differs importantly from that of the model-theoretic tradition that grows out of Hilbert's work. (shrink)

This analysis of Frege's views on language and metaphysics in On Sense and Reference, arguably one of the most important philosophical essays of the past hundred years, provides a thorough introduction to the function/argument analysis and applies Frege's technique to the central notions of predication, identity, existence and truth. Of particular interest is the analysis of the Paradox of Identity and a discussion of three solutions: the little-known Begriffsschrift solution, the sense/reference solution, and Russell's 'On Denoting' solution. Russell's (...) views wend their way through the work, serving as a foil to Frege. Appendices give the proofs of the first 68 propositions of Begriffsschrift in modern notation. This book will be of interest to students and professionals in philosophy and linguistics. (shrink)

We study the complexity of proving the Pigeon Hole Principle in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We prove a size-depth trade-off upper bound for monotone proofs of the standard encoding of the PHP as a monotone sequent. At one extreme of the trade-off we get quasipolynomia -size monotone proofs, and at the other extreme we get subexponential-size bounded-depth monotone proofs. This result is a consequence of deriving the basic properties of (...) certain monotone formulas computing the Boolean threshold functions. We also consider the monotone sequent expressing the Clique-Coclique Principle defined by Bonet, Pitassi and Raz [9]. We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one-to-one and onto PHP, and so CLIQUE also has quasipolynomia -size monotone proofs. As a consequence of our results, Resolution, Cutting Planes with polynomially bounded coefficients, and Bounded-Depth Frege are exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudlák. (shrink)

Frege says, at the end of a discussion of formalism in the Foundations of Arithmetic, that his own foundational program “could be called formal” but is “completely different” from the view he has just criticized. This essay examines Frege’s relationship to Hermann Hankel, his main formalist interlocutor in the Foundations, in order to make sense of these claims. The investigation reveals a surprising result: Frege’s foundational program actually has quite a lot in common with Hankel’s. This undercuts (...) Frege’s claim that his own view is completely different from Hankel’s formalism, and motivates a closer examination of where the differences lie. On the interpretation offered here, Frege shares important parts of the formalist perspective, but differs in recognizing a kind of content for arithmetical terms which can only be made available via proof from prior postulates. (shrink)

In Part III of his 1879 logic Frege proves a theorem in the theory of sequences on the basis of four definitions. He claims in Grundlagen that this proof, despite being strictly deductive, constitutes a real extension of our knowledge, that it is ampliative rather than merely explicative. Frege furthermore connects this idea of ampliative deductive proof to what he thinks of as a fruitful definition, one that draws new lines. My aim is to show that we can (...) make good sense of these claims if we read Frege’s notation diagrammatically, in particular, if we take that notation to have been designed to enable one to exhibit the (inferentially articulated) contents of concepts in a way that allows one to reason deductively on the basis of those contents. (shrink)

By a well-known result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 36–50; R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976], all Frege systems for the classical propositional calculus are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 129–146] have recently (...) shown p-equivalence of Frege systems for the intuitionistic propositional calculus in the standard language, building on a description of admissible rules of IPC by Iemhoff [R. Iemhoff, On the admissible rules of intuitionistic propositional logic, Journal of Symbolic Logic 66 281–294]. We prove a similar result for an infinite family of normal modal logics, including K4, GL, S4, and. (shrink)

Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

Frege's docent's dissertation Rechnungsmethoden, die sich auf eine Erweiterung des Grössenbegriffes gründen(1874) contains indications of a bold attempt to extend arithmetic. According to it, arithmetic means the science of magnitude, and magnitude must be understood structurally without intuitive support. The main thing is insight into the formal structure of the operation of ?addition?. It turns out that a general ?magnitude domain? coincides with a (commutative) group. This is an interesting connection with simultaneous developments in abstract algebra. As his main (...) application, Frege studies iterations of functions. He does not yet pose the question of existence proofs. Measurement of magnitudes is also connected to numbers, but the discussion is here ambiguous in a way which calls for the systematic account of numbers in Grundgesetze. (shrink)

Frege's Grundgesetze was one of the 19th century forerunners to contemporary set theory which was plagued by the Russell paradox. In recent years, it has been shown that subsystems of the Grundgesetze formed by restricting the comprehension schema are consistent. One aim of this paper is to ascertain how much set theory can be developed within these consistent fragments of the Grundgesetze, and our main theorem shows that there is a model of a fragment of the Grundgesetze which defines (...) a model of all the axioms of Zermelo-Fraenkel set theory with the exception of the power set axiom. The proof of this result appeals to G\"odel's constructible universe of sets, which G\"odel famously used to show the relative consistency of the continuum hypothesis. More specifically, our proofs appeal to Kripke and Platek's idea of the projectum within the constructible universe as well as to a weak version of uniformization (which does not involve knowledge of Jensen's fine structure theory). The axioms of the Grundgesetze are examples of abstraction principles, and the other primary aim of this paper is to articulate a sufficient condition for the consistency of abstraction principles with limited amounts of comprehension. As an application, we resolve an analogue of the joint consistency problem in the predicative setting. (shrink)

The analysis of identity as coreference is strongly associated with Frege ; it is the view in Begriffsschrift, and, some have argued, henceforth throughout his work. This thesis is incorrect: Frege never held that identity is coreference. The case is made not by interpretation of “proof-quotes”, but rather by exploring how Frege actually deploys the concept. Two cases are considered. The first, from Grundgesetze, are the definitions of the core concepts, zero and truth; the second, from Begriffsschrift, (...) is the validity of Leibniz's Law. In both cases, if identity is coreference, results ensue that would be unacceptable to Frege. (shrink)

This paper defends the view that Frege’s reduction of arithmetic to logic would, if successful, have shown that arithmetical knowledge is analytic in essentially Kant’s sense. It is argued, as against Paul Benacerraf, that Frege’s apparent acceptance of multiple reductions is compatible with this epistemological thesis. The importance of this defense is that (a) it clarifies the role of proof, definition, and analysis in Frege’s logicist works; and (b) it demonstrates that the Fregean style of reduction is (...) a valuable tool for those who would investigate the nature of arithmetical knowledge. (shrink)

A Ramsey statement denoted \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${n \longrightarrow (k)^2_2}$$\end{document} says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into a valid DNF formula RAM(n, k) of size O(nk) and with terms of size \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\left(\begin{smallmatrix}k\\2\end{smallmatrix}\right)}$$\end{document}. Let rk be the minimal n for which the statement holds. We prove that (...) RAM(rk, k) requires exponential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll [15]. As a consequence of Pudlák’s work in bounded arithmetic [19] it is known that there are quasi-polynomial size constant depth Frege proofs of RAM(4k, k), but the proof complexity of these formulas in resolution R or in its extension R(log) is unknown. We define two relativizations of the Ramsey statement that still have quasi-polynomial size constant depth Frege proofs but for which we establish exponential lower bound for R. (shrink)

Gregory Landini offers a detailed historical account of Frege's notations and the philosophical views that led Frege from Begriffssscrhrift to his mature work Grundgesetze, addressing controversial issues that surround the notations.

Controversy remains over exactly why Frege aimed to estabish logicism. In this essay, I argue that the most influential interpretations of Frege's motivations fall short because they misunderstand or neglect Frege's claims that axioms must be self-evident. I offer an interpretation of his appeals to self-evidence and attempt to show that they reveal a previously overlooked motivation for establishing logicism, one which has roots in the Euclidean rationalist tradition. More specifically, my view is that Frege had (...) two notions of self-evidence. One notion is that of a truth being foundationally secure, yet not grounded on any other truth. The second notion is that of a truth that requires only clearly grasping its content for rational, a priori justified recognition of its truth. The overarching thesis I develop is that Frege required that axioms be self-evident in both senses, and he relied on judging propositions to be self-evident as part of his fallibilist method for identifying a foundation of arithmetic. Consequently, we must recognize both notions in order to understand how Frege construes ultimate foundational proofs, his methodology for discovering and identifying such proofs, and why he thought the propositions of arithmetic required proof. (shrink)

Abstract Though it has been claimed that Frege's commitment to expressions in indirect contexts not having their customary senses commits him to an infinite number of semantic primitives, Terrence Parsons has argued that Frege's explicit commitments are compatible with a two-level theory of senses. In this paper, we argue Frege is committed to some principles Parsons has overlooked, and, from these and other principles to which Frege is committed, give a proof that he is indeed committed (...) to an infinite number of semantic primitives?an intolerable result. (shrink)

I examine Frege’s explanation of how Hilbert ought to have presented his proofs of the independence of the axioms of geometry: in terms of mappings between (what we would call) fully interpreted statements. This helps make sense of Frege’s objections to the notion of different interpretations, which many have found puzzling. (The paper is the text of a talk presented in October 1994.).

Kant discovered a philosophical problem with mathematical proof. Despite being a priori , its methodology involves more than analytic truth. But what else is involved? This problem is widely taken to have been solved by Frege’s extension of logic beyond its restricted (and largely Aristotelian) form. Nevertheless, a successor problem remains: both traditional and contemporary (classical) mathematical proofs, although conforming to the norms of contemporary (classical) logic, never were, and still aren’t, executed by mathematicians in a way that (...) transparently reveals why these proofs—written in the vernacular to this very day—succeed in conforming to those norms. (shrink)

In contemporary historical studies, Peano is usually included in the logical tradition pioneered by Frege. In this paper, I shall first demonstrate that Frege and Peano independently developed a similar way of using logic for the rigorous expression and proof of mathematical laws. However, I shall then suggest that Peano also used his mathematical logic in such a way that anticipated a formalisation of mathematical theories which was incompatible with Frege’s conception of logic.

In this paper, we characterize the strength of the predicative Frege hierarchy, , introduced by John Burgess in his book [J. Burgess, Fixing frege, in: Princeton Monographs in Philosophy, Princeton University Press, Princeton, 2005]. We show that and are mutually interpretable. It follows that is mutually interpretable with Q. This fact was proved earlier by Mihai Ganea in [M. Ganea, Burgess’ PV is Robinson’s Q, The Journal of Symbolic Logic 72 619–624] using a different proof. Another consequence of (...) the our main result is that is mutually interpretable with Kalmar Arithmetic . The fact that interprets EA was proved earlier by Burgess. We provide a different proof. Each of the theories is finitely axiomatizable. Our main result implies that the whole hierarchy taken together, , is not finitely axiomatizable. What is more: no theory that is mutually locally interpretable with is finitely axiomatizable. (shrink)

1. There is only one rule of inference, modus ponens. This is true both in the presentations of Begriffsschrift and Grundgesetze. There are other ways of making transitions between propositions in proofs, but these are never labeled by Frege “rules of inference.” These pertain to scope of quantification, parsing of formulas, introduction of definitions, conventions for the use and replacement of the various letters, and certain structural reorganizations, ; cf. the list in Gg §48.

Concerns a problem posed, but not solved, by Frege in part III of his Grundgesetze. As a preliminary to defining ‘real number’, Frege attempts to analyse the notion of a quantitative domain. He was unaware of the previous attempt of Otto Holder to do this; it is remarked how much weaker Frege's assumptions were in deriving theorems than Holder's. Frege deals with groups on which there is a right‐invariant semilinear ordering, although he does not use this (...) terminology. He is uncertain whether it can be deduced that the ordering is also left‐invariant, and proves as much as possible without invoking the assumption that it is. The independence proof, due to Dr Peter Neumann, establishes that it could not be deduced. (shrink)

We consider small-weight Cutting Planes (CP * ) proofs; that is, Cutting Planes (CP) proofs with coefficients up to $\operatorname{Poly}(n)$ . We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP * proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution. We also (...) prove the following two theorems: (1) Tree-like CP * proofs cannot polynomially simulate non-tree-like CP * proofs. (2) Tree-like (CP * proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other. Our proofs also work for some generalizations of the CP * proof system. In particular, they work for CP * with a deduction rule, and also for any proof system that allows any formula with small communication complexity, and any set of sound rules of inference. (shrink)

What makes certain definitions fruitful? And how can definitions play an explanatory role? The purpose of this paper is to examine these questions via an investigation of Frege’s treatment of definitions. Specifically, I pursue this issue via an examination of Frege’s views about the scientific unification of logic and arithmetic. In my view, what interpreters have failed to appreciate is that logicism is a project of unification, not reduction. For Frege, unification involves two separate steps: (1) an (...) account of the content expressed by arithmetical claims and (2) the justification of that content. The distinction between these steps allows us to see that there are two notions of definition at play in Frege’s logicist work, viz., one concerned with conceptual analysis, the other concerned with the construction of gap-free proof. I then use this discussion to explain how Frege employs his definitions to defend an epistemological thesis about arithmetic, and to clarify Grundlagen’s fruitfulness condition of definitions, and thereby address two interpretive puzzles from the recent literature. (shrink)

In this paper, we discuss the prevailing view amongst philosophers and many mathematicians concerning mathematical proof. Following Cellucci, we call the prevailing view the “axiomatic conception” of proof. The conception includes the ideas that: a proof is finite, it proceeds from axioms and it is the final word on the matter of the conclusion. This received view can be traced back to Frege, Hilbert and Gentzen, amongst others, and is prevalent in both mathematical text books and logic text books.

Given the harmony principle for logical operators, compositionality ought to ensure that harmony should obtain at the level of whole contents. That is, the role of a content qua premise ought to be balanced exactly by its role as a conclusion. Frege's contextual definition of propositional content happens to exploit this balance, and one appeals to the Cut rule to show that the definition is adequate. We show here that Frege's definition remains adequate even when one relevantizes logic (...) by abandoning an unrestricted Cut rule. The proof exploits the fact that in the relevantized logic, which abandons the unrestricted rule of Cut, any failure of the transitivity of deduction is offset by the epistemic gain involved in learning that a stronger-than-expected result holds. (shrink)

In a series of articles dating from 1903 to 1906, Frege criticizes Hilbert’s methodology of proving the independence and consistency of various fragments of Euclidean geometry in his Foundations of Geometry. In the final part of the last article, Frege makes his own proposal as to how the independence of genuine axioms should be proved. Frege contends that independence proofs require the development of a ‘new science’ with its own basic truths. This paper aims to provide (...) a reconstruction of this New Science that meets modern standards and to examine possible problems surrounding Frege’s original proposal. The paper is organized as follows: the first two sections summarize the main points of the Frege–Hilbert controversy and discuss some issues surrounding the problem of independence proofs. Section 3 contains an informal presentation of Frege’s proposal. In section 4 a more detailed reconstruction of Frege’s New Science is set out while section 5 examines what is left out. The concluding section is devoted to a discussion of Frege’s strategy and its significance from a broader perspective. (shrink)

In the first chapter, we discuss Dummett’s idea that the notion of truth arises from the one of the correctness of an assertion. We argue that, in a first-order language, the need of defining truth in terms of the notion of satisfaction, which is yielded by the presence of quantifiers, is structurally analogous to the need of a notion of truth as distinct from the one of correctness of an assertion. In the light of the analogy between predicates in (...) class='Hi'>Frege and open formulas in Tarksi, we concentrate on the semantic status of predicates. We register a dual attitude of Dummett towards Frege’s ascription of reference to predicates. On the one it is needed to endow quantifiers with their appropriate meaning. On the other hand, the introduction of concepts, as semantic correlate of predicates, smuggles a realist flavor in the overall semantic picture. In concluding the excursus (and with it the chapter), we stress Dummett’s will of developing a semantic picture free from this realist trait. In the second chapter, we present the idea of a proof-theoretic semantics. As for Frege true sentences denotes the truth-value True, so here closed' (i.e. categorical) valid argumentations denotes proofs. If a language contains implication-like operators, in order to characterize the condition of validity of a closed argumentation one has to introduce a notion of validity applying to ‘open’ (i.e. hypothetical) argumentations. We argue that this problem is analogous to the one posed by quantifiers in Frege-Tarksi’s style semantics. That is, implication forces one to introduce notion of validity for argumentations, which is more substantial than the correctness of the assertion of their conclusions. As we saw, the corresponding claim in the truth-based approach—that quantifiers require one to introduce a notion of truth, which is more substantial than the one of an assertion being correct—was the source of realism. Hence, Dummett proposes to reduce the semantic contribution of open argumentations to the one of their ‘closed instances’. In the truth-based perspective, this would correspond to the denial of the need of introducing concepts as the semantic correlates of predicates. We argue that Dummett’s fear, that an irreducible notion of function (represented by the need of ascribing validity to open argumentations) would lead to realism, turns out to be ill-founded. In the third chapter, we discuss the role played by the notion of truth in the anti-realist account. The notion of truth is what the anti-realist needs to cope with the so-called paradox of deduction. The analysis of the paradox yields to distinguishing between the truth of a sentence and the truth of a sentence being recognized. In terms of these conceptual couple, we reconsider the relationship between truth and assertion in an anti-realist perspective. Grounds are provided for a thesis (which was already advanced in chapter two), according to which the notion of the assertion of a sentence being correct is primarily connected only with the canonical means of establishing a sentence. The possibility of establishing a sentence by indirect means is conceptually dependent on the practice of establishing logical relationship of dependence among sentences. That is, the notion of a closed valid non-canonical argumentation is of any theoretical relevance only in presence of a notion of validity applying to open argumentations. In the fourth chapter, we discuss the possibility of characterizing in the proof-theoretic-semantics a notion of refutation. We develop an original characterization of refutations starting from an informal inductive specification of the condition of refutations of logically complex sentences. A sub-structural logic, called dual-intuitionistic logic, stands to this notion in the same relationship in which intuitionistic logic stands to the notion of proof so far consdered. All notions developed in chapter 2 have their corresponding (dual) ones in the framework developed. In particular, the distinctions canonical/non-canonical and closed/open argumentations. In the refutation based perspective, elimination rules have priority over introductions and the (only) assumption over the (many) conclusions. In the conclusions, we indicate the ingredients that an anti-realist approach to meaning should incorporate, in order to avoid the difficulties we registered. The core of an alternative view is a different conception of the relationship between categorical and hypothetical notions, in which the validity of open argumentations is not reduced to that of their instances, but rather it is directly defined. As a limit case, one would get a notion of validity applying to closed argumentations. (shrink)

BY THE middle of the nineteenth century, serious difficulties in carrying out the Cartesian project of explaining through attention to our ideas how we may know things as they really are had become evident. A satisfactory account of the connection between occurrences of ideas in us and the properties of things apart from our ideas of them, an account promised by Descartes in the Meditations, had not been forthcoming. Descartes' claim that God's omnipotence guarantees that the members of some recognizable (...) class of our ideas, the class of clear and distinct perceptions, represent things as they really are became clearly unsatisfactory as part of a realist theory of knowledge as soon as Hume and Kant had shown the unsoundness of Descartes' proofs of the existence of God. Whether or not God's omnipotence guarantees that we can know things as they are, it had become evident that we lack adequate grounds for claiming to know that this is the case. Consequently, there developed by the middle of the nineteenth century a consensus that we lacked a satisfactory account of how our ideas enable us to know things. (shrink)