I formulate the Zermelo-Russell paradox for naive set theory. A sketch is given of Zermelo’s solution to the paradox: the cumulative type structure. A careful analysis of the set formation process shows a missing component in this solution: the necessity of an assumed imaginary jump out of an infinite universe. Thus a set is formed by a suitable combination of concrete and imaginary operations all of which can be made or assumed by a Turing machine. Some consequences are drawn from (...) this improved analysis of the concept of set, for the theory of sets and for the philosophy and foundations of mathematics. (shrink)

This article serves to present a large mathematical perspective and historical basis for the Axiom of Replacement as well as to affirm its importance as a central axiom of modern set theory.

A well known fact is that every Lebesgue measurable set is regular, i.e., it includes an F$_{\sigma}$ set of the same measure. We analyze this fact from a metamathematical or foundational standpoint. We study a family of Muchnik degrees corresponding to measure-theoretic regularity at all levels of the effective Borel hierarchy. We prove some new results concerning Nies's notion of LR-reducibility. We build some $\omega$-models of RCA$_0$which are relevant for the reverse mathematics of measure-theoretic regularity.

The fact that Gödel's famous incompleteness theorem and the archetype of all logical paradoxes, that of the Liar, are related closely is, of course, not only well known, but is a part of the common knowledge of the community of logicians. Indeed, almost every more or less formal treatment of the theorem makes a reference to this connection. Gödel himself remarked in the paper announcing his celebrated result :The analogy between this result and Richard's antinomy leaps to the eye;there is (...) also a close relationship with the ‘liar’ antinomy, since … we are… confronted with a proposition which asserts its own unprovability.In the light of the fact that the existence of this connection is commonplace it is all the more surprising that very little can be learnt about its exact nature except perhaps that it is some kind of similarity or analogy. There is, however, a lot more to it than that. Indeed, as we shall try to show below, the general ideas underlying the three central theorems concerning internal limitations of formal deductive systems can be taken as different ways to resolve the Liar paradox. More precisely, it will turn out that an abstract formal variant of the Liar paradox, which can almost straightforwardly inferred from its original ordinary language version, is a possible common generalization of Gödel's incompleteness theorem, the theorem of Tarski on the undefinability of truth, and that of Church concerning the undecidability of provability. (shrink)

After an introduction which demonstrates the failure of the equational analogue of Beth?s definability theorem, the first two sections of this paper are devoted to an elementary exposition of a proof that a functional constant is equationally definable in an equational theory iff every model of the set of those consequences of the theory that do not contain the functional constant is uniquely extendible to a model of the theory itself.Sections three, four and five are devoted to applications and extensions (...) of this result.Topics considered here include equational definability in first order logic, an extended notion of definability in equational logic and the synonymy of equational theories.The final two sections briefly review some of the history of equational logic. (shrink)

With quantifier elimination and restriction of language to a binary relation symbol and constant symbols it is shown that countable complete theories having three isomorphism types of countable models are "essentially" the Ehrenfeucht example [4, $\s6$ ].

We consider the informal concept of "computability" or "effective calculability" and two of the formalisms commonly used to define it, "(Turing) computability" and "(general) recursiveness". We consider their origin, exact technical definition, concepts, history, general English meanings, how they became fixed in their present roles, how they were first and are now used, their impact on nonspecialists, how their use will affect the future content of the subject of computability theory, and its connection to other related areas. After a careful (...) historical and conceptual analysis of computability and recursion we make several recommendations in section §7 about preserving the intensional differences between the concepts of "computability" and "recursion." Specifically we recommend that: the term "recursive" should no longer carry the additional meaning of "computable" or "decidable;" functions defined using Turing machines, register machines, or their variants should be called "computable" rather than "recursive;" we should distinguish the intensional difference between Church's Thesis and Turing's Thesis, and use the latter particularly in dealing with mechanistic questions; the name of the subject should be "Computability Theory" or simply Computability rather than "Recursive Function Theory.". (shrink)

The context for this paper is Feferman's theory of explicit mathematics, a formal framework serving many purposes. It is suitable for representing Bishop-style constructive mathematics as well as generalized recursion, including direct expression of structural concepts which admit self-application. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications (Feferman's notion of set) possesses a least fixed point. To be more precise, the new axiom (...) not merely postulates the existence of a least solution, but, by adjoining a new functional constant to the language, it is ensured that a fixed point is uniformly presentable as a function of the monotone operation. The upshot of the paper is that the latter extension of explicit mathematics (when based on classical logic) embodies considerable proof-theoretic strength. It is shown that it has at least the strength of the subsystem of second order arithmetic based on Π 1 2 comprehension. (shrink)

Proofs of Gödel's First Incompleteness Theorem are often accompanied by claims such as that the gödel sentence constructed in the course of the proof says of itself that it is unprovable and that it is true. The validity of such claims depends closely on how the sentence is constructed. Only by tightly constraining the means of construction can one obtain gödel sentences of which it is correct, without further ado, to say that they say of themselves that they are unprovable (...) and that they are true; otherwise a false theory can yield false gödel sentences. (shrink)

For a primitive recursive consistent and strong enough theory T we construct an independent statement which has some clear metamathematical meaning.

Set theory is an autonomous and sophisticated field of mathematics, enormously successful not only at its continuing development of its historical heritage but also at analyzing mathematical propositions cast in set-theoretic terms and gauging their consistency strength. But set theory is also distinguished by having begun intertwined with pronounced metaphysical attitudes, and these have even been regarded as crucial by some of its great developers. This has encouraged the exaggeration of crises in foundations and of metaphysical doctrines in general. However, (...) set theory has proceeded in the opposite direction, from a web of intensions to a theory of extensionpar excellence, and like other fields of mathematics its vitality and progress have depended on a steadily growing core of mathematical structures and methods, problems and results. There is also the stronger contention that from the beginning set theory actually developed through a progression ofmathematicalmoves, whatever and sometimes in spite of what has been claimed on its behalf.What follows is an account of the development of set theory from its beginnings through the creation of forcing based on these contentions, with an avowedly Whiggish emphasis on the heritage that has been retained and developed by current set theory. The whole transfinite landscape can be viewed as the result of Cantor's attempt to articulate and solve the Continuum Problem. (shrink)

This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we (...) show how to interpret the theory BTFA in Robinson's theory of arithmetic Q. This fact entails that the elementary theory of the real closed ordered fields is interpretable in Q. (shrink)

A new method of "minimal" realizability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)--functions f such that HA $\vdash \forall x\exists!yA(x, y)\Rightarrow$ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of L(HA) with only x, y free--are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the $ -recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be (...) chosen to be $ -recursive. The method is extended to intuitionistic finite-type arithmetic, HA ω 0 , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived. (shrink)

Truth predicates are widely believed to be capable of serving a certain logical or quasi-logical function. There is little consensus, however, on the exact nature of this function. We offer a series of formal results in support of the thesis that disquotational truth is a device to simulate higher-order resources in a first-order setting. More specifically, we show that any theory formulated in a higher-order language can be naturally and conservatively interpreted in a first-order theory with a disquotational truth or (...) truth-of predicate. In the first part of the paper we focus on the relation between truth and full impredicative sentential quantification. The second part is devoted to the relation between truth-of and full impredicative predicate quantification. (shrink)

This paper outlines an account of numbers based on the numerical equivalence schema, which consists of all sentences of the form ‘#x.Fx=n if and only if ∃nx Fx’, where # is the number-of operator and ∃n is defined in standard Russellian fashion. In the first part of the paper, I point out some analogies between the NES and the T-schema for truth. In light of these analogies, I formulate a minimalist account of numbers, based on the NES, which strongly parallels (...) the minimalist account of truth. One may be tempted to develop the minimalist account in a fictionalist direction, according to which arithmetic is useful but untrue, if taken at face value. In the second part, I argue that this suggestion is not as attractive as it may first appear. The NES suffers from a similar problem to the T-schema: it is deductively weak and does not enable the derivation of any non-trivial generalizations. In the third part of the paper, I explore some strategies to deal with the generalization problem, again drawing inspiration from the literature on truth. In closing this paper, I briefly compare the minimalist to some other accounts of numbers. (shrink)

According to the iterative conception of set, each set is a collection of sets formed prior to it. The notion of priority here plays an essential role in explanations of why contradiction-inducing sets, such as the Russell set, do not exist. Consequently, these explanations are successful only to the extent that a satisfactory priority relation is made out. I argue that attempts to do this have fallen short: understanding priority in a straightforwardly constructivist sense threatens the coherence of the empty (...) set and raises serious epistemological concerns; but the leading realist interpretations---ontological and modal interpretations of priority---are deeply problematic as well. I conclude that the purported explanatory virtues of the iterative conception are, at present, unfounded. (shrink)

The main objective of this PhD Thesis is to present a method of obtaining strong normalization via natural ordinal, which is applicable to natural deduction systems and typed lambda calculus. The method includes (a) the definition of a numerical assignment that associates each derivation (or lambda term) to a natural number and (b) the proof that this assignment decreases with reductions of maximal formulas (or redex). Besides, because the numerical assignment used coincide with the length of a specific sequence of (...) reduction - the worst reduction sequence - it is the lowest upper bound on the length of reduction sequences. The main commitment of the introduced method is that it is constructive and elementary, produced only through analyzing structural and combinatorial properties of derivations and lambda terms, without appeal to any sophisticated mathematical tool. Together with the exposition of the method, it is presented a comparative study of some articles in the literature that also get strong normalization by means we can identify with the natural ordinal methods. Among them we highlight Howard[1968], which performs an ordinal analysis of Godel’s Dialectica interpretation for intuitionistic first order arithmetic. We reveal a fact about this article not noted by the author himself: a syntactic proof of strong normalization theorem for the system of typified lambda calculus λ⊃ is a consequence of its results. This would be the first strong normalization proof in the literature. (written in Portuguese). (shrink)

We show how removing faith-based beliefs in current philosophies of classical and constructive mathematics admits formal, evidence-based, definitions of constructive mathematics; of a constructively well-defined logic of a formal mathematical language; and of a constructively well-defined model of such a language. -/- We argue that, from an evidence-based perspective, classical approaches which follow Hilbert's formal definitions of quantification can be labelled `theistic'; whilst constructive approaches based on Brouwer's philosophy of Intuitionism can be labelled `atheistic'. -/- We then adopt what may (...) be labelled a finitary, evidence-based, `agnostic' perspective and argue that Brouwerian atheism is merely a restricted perspective within the finitary agnostic perspective, whilst Hilbertian theism contradicts the finitary agnostic perspective. -/- We then consider the argument that Tarski's classic definitions permit an intelligence---whether human or mechanistic---to admit finitary, evidence-based, definitions of the satisfaction and truth of the atomic formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers in two, hitherto unsuspected and essentially different, ways. -/- We show that the two definitions correspond to two distinctly different---not necessarily evidence-based but complementary---assignments of satisfaction and truth to the compound formulas of PA over N. -/- We further show that the PA axioms are true over N, and that the PA rules of inference preserve truth over N, under both the complementary interpretations; and conclude some unsuspected constructive consequences of such complementarity for the foundations of mathematics, logic, philosophy, and the physical sciences. -/- . (shrink)

We consider the argument that Tarski's classic definitions permit an intelligence---whether human or mechanistic---to admit finitary evidence-based definitions of the satisfaction and truth of the atomic formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers in two, hitherto unsuspected and essentially different, ways: (1) in terms of classical algorithmic verifiabilty; and (2) in terms of finitary algorithmic computability. We then show that the two definitions correspond to two distinctly different assignments of satisfaction and truth (...) to the compound formulas of PA over N---I_PA(N; SV ) and I_PA(N; SC). We further show that the PA axioms are true over N, and that the PA rules of inference preserve truth over N, under both I_PA(N; SV ) and I_PA(N; SC). We then show: (a) that if we assume the satisfaction and truth of the compound formulas of PA are always non-finitarily decidable under I_PA(N; SV ), then this assignment corresponds to the classical non-finitary putative standard interpretation I_PA(N; S) of PA over the domain N; and (b) that the satisfaction and truth of the compound formulas of PA are always finitarily decidable under the assignment I_PA(N; SC), from which we may finitarily conclude that PA is consistent. We further conclude that the appropriate inference to be drawn from Goedel's 1931 paper on undecidable arithmetical propositions is that we can define PA formulas which---under interpretation---are algorithmically verifiable as always true over N, but not algorithmically computable as always true over N. We conclude from this that Lucas' Goedelian argument is validated if the assignment I_PA(N; SV ) can be treated as circumscribing the ambit of human reasoning about `true' arithmetical propositions, and the assignment I_PA(N; SC) as circumscribing the ambit of mechanistic reasoning about `true' arithmetical propositions. (shrink)

This monograph offers a fresh perspective on the applicability of mathematics in science. It explores what mathematics must be so that its applications to the empirical world do not constitute a mystery. In the process, readers are presented with a new version of mathematical structuralism. The author details a philosophy of mathematics in which the problem of its applicability, particularly in physics, in all its forms can be explained and justified. Chapters cover: mathematics as a formal science, mathematical ontology: what (...) does it mean to exist, mathematical structures: what are they and how do we know them, how different layers of mathematical structuring relate to each other and to perceptual structures, and how to use mathematics to find out how the world is. The book simultaneously develops along two lines, both inspired and enlightened by Edmund Husserl’s phenomenological philosophy. One line leads to the establishment of a particular version of mathematical structuralism, free of “naturalist” and empiricist bias. The other leads to a logical-epistemological explanation and justification of the applicability of mathematics carried out within a unique structuralist perspective. This second line points to the “unreasonable” effectiveness of mathematics in physics as a means of representation, a tool, and a source of not always logically justified but useful and effective heuristic strategies. (shrink)

In this paper we study several translations that map models and formulae of the language of second-order arithmetic to models and formulae of the language of truth. These translations are useful because they allow us to exploit results from the extensive literature on arithmetic to study the notion of truth. Our purpose is to present these connections in a systematic way, generalize some well-known results in this area, and to provide a number of new results. Sections 3 and 4 contain (...) some recursion- and proof-theoretic results about Kripke-style fixed-point theories of truth. Section 5 shows how to derive full second-order arithmetic from principles of truth. Section 6 investigates the proof-theoretic strength of disquotation without an arithmetical base theory. (shrink)

We use a new version of the Definability Theorem of Beth in order to unify classical theorems of Yuri Matiyasevich and Jan Denef in one structural statement. We give similar forms for other important definability results from Arithmetic and Number Theory.

I present a reconstruction of the logical system of the Tractatus, which differs from classical logic in two ways. It includes an account of Wittgenstein’s “form-series” device, which suffices to express some effectively generated countably infinite disjunctions. And its attendant notion of structure is relativized to the fixed underlying universe of what is named. -/- There follow three results. First, the class of concepts definable in the system is closed under finitary induction. Second, if the universe of objects is countably (...) infinite, then the property of being a tautology is \Pi^1_1-complete. But third, it is only granted the assumption of countability that the class of tautologies is \Sigma_1-definable in set theory. -/- Wittgenstein famously urges that logical relationships must show themselves in the structure of signs. He also urges that the size of the universe cannot be prejudged. The results of this paper indicate that there is no single way in which logical relationships could be held to make themselves manifest in signs, which does not prejudge the number of objects. (shrink)

The comprehension principle of set theory asserts that a set can be formed from the objects satisfying any given property. The principle leads to immediate contradictions if it is formalized as an axiom scheme within classical first order logic. A resolution of the set paradoxes results if the principle is formalized instead as two rules of deduction in a natural deduction presentation of logic. This presentation of the comprehension principle for sets as semantic rules, instead of as a comprehension axiom (...) scheme, can be viewed as an extension of classical logic, in contrast to the assertion of extra-logical axioms expressing truths about a pre-existing or constructed universe of sets. The paradoxes are disarmed in the extended classical semantics because truth values are only assigned to those sentences that can be grounded in atomic sentences. (shrink)

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...) unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. (shrink)

Chapin reviewed this 1972 ZEITSCHRIFT paper that proves the completeness theorem for the logic of variable-binding-term operators created by Corcoran and his student John Herring in the 1971 LOGIQUE ET ANALYSE paper in which the theorem was conjectured. This leveraging proof extends completeness of ordinary first-order logic to the extension with vbtos. Newton da Costa independently proved the same theorem about the same time using a Henkin-type proof. This 1972 paper builds on the 1971 “Notes on a Semantic Analysis of (...) Variable Binding Term Operators” (Co-author John Herring), Logique et Analyse 55, 646–57. MR0307874 (46 #6989). A variable binding term operator (vbto) is a non-logical constant, say v, which combines with a variable y and a formula F containing y free to form a term (vy:F) whose free variables are exact ly those of F, excluding y. Kalish-Montague 1964 proposed using vbtos to formalize definite descriptions “the x: x+x=2”, set abstracts {x: F}, minimization in recursive function theory “the least x: x+x>2”, etc. However, they gave no semantics for vbtos. Hatcher 1968 gave a semantics but one that has flaws described in the 1971 paper and admitted by Hatcher. In 1971 we give a correct semantic analysis of vbtos. We also give axioms for using them in deductions. And we conjecture strong completeness for the deductions with respect to the semantics. The conjecture, proved in this paper with Hatcher’s help, was proved independently about the same time by Newton da Costa. (shrink)

This paper outlines an account of numbers based on the numerical equivalence schema (NES), which consists of all sentences of the form ‘#x.Fx=n if and only if ∃nx Fx’, where # is the number-of operator and ∃n is defined in standard Russellian fashion. In the first part of the paper, I point out some analogies between the NES and the T-schema for truth. In light of these analogies, I formulate a minimalist account of numbers, based on the NES, which strongly (...) parallels the minimalist (deflationary) account of truth. One may be tempted to develop the minimalist account in a fictionalist direction, according to which arithmetic is useful but untrue, if taken at face value. In the second part, I argue that this suggestion is not as attractive as it may first appear. The NES suffers from a similar problem to the T-schema: it is deductively weak and does not enable the derivation of any non-trivial generalizations. In the third part of the paper, I explore some strategies to deal with the generalization problem, again drawing inspiration from the literature on truth. In closing this paper, I briefly compare the minimalist to some other accounts of numbers. (shrink)

We investigate incomplete symbols, i.e. definite descriptions with scope-operators. Russell famously introduced definite descriptions by contextual definitions; in this article definite descriptions are introduced by rules in a specific calculus that is very well suited for proof-theoretic investigations. That is to say, the phrase ‘incomplete symbols’ is formally interpreted as to the existence of an elimination procedure. The last section offers semantical tools for interpreting the phrase ‘no meaning in isolation’ in a formal way.

A box type is an n-type of an o-minimal structure which is uniquely determined by the projections to the coordinate axes. We characterize heirs of box types of a polynomially bounded o-minimal structure M. From this, we deduce various structure theorems for subsets of $M^k $ , definable in the expansion M of M by all convex subsets of the line. We show that M after naming constants, is model complete provided M is model complete.

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation.

We define classes Φnof formulae of first-order arithmetic with the following properties:(i) Everyφϵ Φnis classically equivalent to a Πn-formula (n≠ 1, Φ1:= Σ1).(ii)(iii)IΠnandiΦn(i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φnboth under existential and universal quantification (we call these classes Θn) the corresponding theoriesiΘnstill prove the same Π2-formulae. In a second part we consideriΔ0plus collection-principles. We (...) show that both the provably recursive functions and the provably total functions ofare polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence. (shrink)