Weiermann [18] introduces a new method to generate fast growing functions in order to get an elegant and perspicuous proof of a bounding theorem for provably total recursive functions in a formal theory, e.g., in PA. His fast growing function θαη is described as follows. For each ordinal a and natural number n let denote a finitely branching, primitive recursive tree of ordinals, i.e., an ordinal as a label is attached to each node in the tree so that the labelling is compatible with the tree ordering. Then the tree is well founded and hence finite by König's lemma. Define θαηn =the depth of the tree =the length of the longest branch in .

We introduce new fast and slow growing functions in this mode of definitions and show that each of these majorizes provably total recursive functions in PA.

We prove that the standard cut is definable in each existentially closed model of IΔ0 + exp by a (parameter free) П1–formula. This definition is optimal with respect to quantifier complexity and allows us to improve some previously known results on existentially closed models of fragments of arithmetic.

Using coding devices based on a theorem due to Zsigmondy, Birkhoff and Vandiver, we first define in terms of successor S and coprimeness predicate ⊥ a full arithmetic over the set of powers of some fixed prime, then we define in the same terms a restriction of the exponentiation. Hence we prove the main result insuring that all arithmetical relations and functions over prime powers and their opposite are {S, ⊥}-definable over Z. Applications to definability over Z and N are stated as corollaries of the main theorem.

Though many working mathematicians embrace a rough and ready form of Platonism, that venerable position has suffered a checkered philosophical career. Indeed the three schools of thought with which most of us began our official philosophizing about mathematics—Intuitionism, Formalism, and Logicism—all stand in fundamental disagreement with Platonism. Nevertheless, various versions of Platonistic thinking survive in contemporary philosophical circles. The aim of this paper is to describe these views, and, as my title suggests, to trace their roots.

I'll begin with some preliminary remarks about the big three schools. This seems a reasonable approach to the issues both because most observers are familiar, at least in a general way, with the tenets of Intuitionism, Formalism, and Logicism, and because it is in reaction to these that contemporary Platonism has taken shape.

Pure Type Systems. PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic.

First we consider a simplification of the start and weakening rules of PTSs. which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems.

A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications.

We prove, relative to suitable hypotheses, that it is consistent for there to be unboundedly many measurable cardinals each of which possesses a large degree of strong compactness, and that it is consistent to assume that the least measurable is partially strongly compact and that the second measurable is strongly compact. These results partially answer questions of Magidor on the relationship of strong compactness to measurability.

Kirby and Paris have exhibited combinatorial algorithms whose computations always terminate, but for which termination is not provable in elementary arithmetic. However, termination of these computations can be proved by adding an axiom first introduced by Goodstein in 1944. Our purpose is to investigate this axiom of Goodstein, and some of its variants, and to show that these are potentially adequate to prove termination of computations of a wide class of algorithms. We prove that many variations of Goodstein's axiom are equivalent, over elementary arithmetic, and contrast these results with those recently obtained for Kruskal's theorem.

Recursion categories have been proposed by Di Paola and Heller in [DPH] as the basis for a category-theoretic approach to recursion theory, in the context of a more general and ambitious project of a purely algebraic treatment of incompleteness phenomena. The way in which the classical notion of creative set is rendered in this new category-theoretic framework plays, therefore, a central role. This is done in [DPH] (Definition 8.1) by defining the notion of creative domains or, rather, domains which are creative relative to some criterion: thus, in a recursion category, every criterion provides a notion of creativeness.

A basic result on creative domains (cf. [DPH, Theorem 8.13]) is that, under certain assumptions, a version of the classical result, due to Myhill [MYH], stating that every creative set is complete, holds: in a recursion category with equality (i.e. exists for every object X) and having enough atoms, every domain which is creative with respect to atoms is also complete.

A first order representation (f.o.r.) in topology is an assignment of finitary relational structures of the same type to topological spaces in such a way that homeomorphic spaces get sent to isomorphic structures. We first define the notions “one f.o.r. is at least as expressive as another relative to a class of spaces” and “one class of spaces is definable in another relative to an f.o.r.”, and prove some general statements. Following this we compare some well-known classes of spaces and first order representations. A principal result is that if X and Y are two Tichonov spaces whose posets of zero-sets are elementarily equivalent then their respective rings of bounded continuous real-valued functions satisfy the same positive-universal sentences. The proof of this uses the technique of constructing ultraproducts as direct limits of products in a category theoretic setting.

Every recursively enumerable extension of arithmetic which obeys the disjunction property obeys the numerical existence property [Fr, 1]. The requirement of recursive enumerability is essential. For extensions of intuitionistic second order arithmetic by means of sentences (in its language) with no existential set quantifiers, the numerical existence property implies the set existence property. The restriction on existential set quantifiers is essential. The numerical existence property cannot be eliminated, but in the case of finite extensions of HAS, can be replaced by a weaker form of it. As a consequence, the set existence property for intuitionistic second order arithmetic can be proved within itself.

We work in set-theory without choice ZF . A set is countable if it is finite or equipotent with ℕ. Given a closed subset F of [0, 1]I which is a bounded subset of ℓ 1(I) (resp. such that F ⊆ c 0(I)), we show that the countable axiom of choice for finite sets, (resp. the countable axiom of choice AC ℕ) implies that F is compact. This enhances previous results where AC ℕ (resp. the axiom of Dependent Choices) was required. If I is linearly orderable (for example I = ℝ), then, in ZF , the closed unit ball of the Hilbert space ℓ 2 (I) is (Loeb-)compact in the weak topology. However, the weak compactness of the closed unit ball of is not provable in ZF .

Consider the statement:

(1) What I am saying cannot be proved.

Let us suppose that this statement can be proved. Then it must be true, i.e., in its own words, it cannot be proved, which contradicts our supposition.

Therefore the statement cannot be proved, since our supposition has led to a contradiction. In other words, the statement is true. In this way we have proved the statement.

Therefore the statement both can and cannot be proved.

In the second part of the argument, if we speak of proving (1) in a given formal system S, then we cannot draw the conclusion that we have proved the statement in S. For it is possible that the argument cannot be formalized in S. Indeed, as we know, Gödel shows in his famous article of 1931 that for suitable systems S, it is possible to construct in S a statement saying in effect that the statement itself is not provable in S. The conclusion Gödel draws, we may recall, is that the statement thus constructed is true but not provable in S. Thus no contradictions arise in this way if we are confined to provability in a given system.

A dual of (1) is the following:

(2) What I am saying can be refuted.

Let us suppose that this statement is true, or, in its own words, that it can be refuted. Then it must be false, which contradicts our supposition.

Therefore the statement is false, since our supposition has led to a contradiction. In this way, we have refuted the statement. We see that the statement can be refuted; in other words, it is true.

Kristiansen and Murwanashyaka recently proved that Robinson arithmetic, Q, is interpretable in an elementary theory of full binary trees, T. We prove that, conversely, T is interpretable in Q by producing a formal interpretation of T in an elementary concatenation theory QT+, thereby also establishing mutual interpretability of T with several well-known weak essentially undecidable theories of numbers, strings, and sets. We also introduce a “hybrid” elementary theory of strings and trees, WQT*, and establish its mutual interpretability with Robinson’s weak arithmetic R, the weak theory of trees WT of Kristiansen and Murwanashyaka, and the weak concatenation theory WTCε of Higuchi and Horihata.

That elementary number theory is consistent and can be given a metamathematical consistency proof has been well known since Gentzen's 1936 paper, and a number of different proofs of this result have since been offered. What is presented here is essentially a simplified and generalized version of the proof given by Ackermann in 1940 [1]; but the proof given here applies to systems formalized in standard quantification theory rather than in Hilbert's ε-calculus, and is based upon the analysis of quantificational reasoning given by Herbrand's Fundamental Theorem. Dreben and Denton sketch such a proof in [2], but at a crucial point they follow Ackermann in tying the strategy of their proof too closely to the standard model. This makes the proof more complex than it need be and restricts its application to systems with induction on the standard well-ordering. The present proof is both simpler and more general in that it applies to systems ZR of number theory with induction on arbitrary recursive well-orderings R. This generalization was first obtained by Tait in [11] using functionals of lowest type. Some technical devices employed below are similar to ones used by Tait, but while the proof-theoretic methods employed here are naturally characterizable in terms of functionals of lowest type the present proof avoids the introduction of such functionals into the languages studied.

We show that the elimination rule for the multiplicative (or intensional) conjunction Λ is admissible in many important multiplicative substructural logics. These include LLm (the multiplicative fragment of Linear Logic) and RMIm (the system obtained from LLm by adding the contraction axiom and its converse, the mingle axiom.) An exception is Rm (the intensional fragment of the relevance logic R, which is LLm together with the contraction axiom). Let SLLm and SRm be, respectively, the systems which are obtained from LLm and Rm by adding this rule as a new rule of inference. The set of theorems of SRm is a proper extension of that of Rm, but a proper subset of the set of theorems of RMIm. Hence it still has the variable-sharing property. SRm has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLLm relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLLm corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element (in the first case we get the system BCKm, in the second - the system SRm). Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.

1. The notion of derivability. Italic capitals, with or without subscripts, will be used as variables. They are to take as values some manner of elements which may for the present be left undetermined. Now let us consider abstractly the notion of the derivability of an element X from one or more specified elements by a series of steps of a specified kind. This involves reference to two conditions upon elements. One of these conditions, expressible by some statement form containing a single free variable, determines the elements from which X is said to be derivable. The other condition, expressed say by a statement form containing k + 1 free variables, determines the kind of steps by which the derivation is to proceed; it is the condition which any elements Z1, … Zk, Y must fulfill if progress from Zi, …, Zk to Y is to constitute a step of derivation in the intended sense. Supposing “f(Y)” supplanted by the first of these statement forms, whatever it may be, and “g(Z1, …, Zk, Y)” supplanted by the other, let us adopt the form of notation

to express derivability of X in the suggested sense. The meaning of (1) can be formulated more accurately as follows:

(i) There are elements Y1 to Ym (for some m) such that Ym = X and, for each i≦m, either f(Yi) or else there are numbers j1 to Ym, each less than i, for which g(Yj1, …, Yjk, Yi).

(Variable subscripts are to be understood, here and throughout the paper, as referring only to positive integers.)

The notion (1) is illustrated in the ancestral R* of a relation R;1 for,

Another illustration is afforded by metamathematics. Suppose our elements are the expressions used in some formal system; suppose we have defined “Post(Y)”, meaning that Y is a postulate of that system; and suppose we have defined “Inf(ZI, …, Zk, Y)” (for some fixed k large enough for all purposes of the system in question), meaning that Y proceeds from Z1, …, Zk by one application of one or another of the rules of inference of the system. Then

would mean that X is a theorem of the system.