First-Order Reasoning and Primitive Recursive Natural Number Notations

AbstractFor α less than ε0 let Nα be the number of occurrences of ω in the Cantor normal form of α. Further let ∣n∣ denote the binary length of a natural number n, let ∣n∣h denote the h-times iterated binary length of n and let inv(n) be the least h such that ∣n∣h ≤ 2. We show that for any natural number h first order Peano arithmetic, PA, does not prove the following sentence: For all K there exists an M which bounds the lengths n of all strictly descending sequences 〈α0, …, αn〉 of ordinals less than ε0 which satisfy the condition that the Norm Nαi of the i-th term αi is bounded by K + ∣i∣ · ∣i∣i.As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence 〈α0, …, αn〉 of ordinals less than ε0 which satisfies the condition that the Norm Nαi of the i-th term αi is bounded by K + ∣i∣ · inv(i). The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations.Using results from Otter and from Matoušek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856.…

Download Full-text

More on definable sets of p-adic numbers

Journal of Symbolic Logic ◽

10.2307/2274581 ◽

1988 ◽

Vol 53 (3) ◽

pp. 912-920 ◽

Cited By ~ 2

Author(s):

Philip Scowcroft

Keyword(s):

Cross Section ◽

Quantifier Elimination ◽

Order Theory ◽

Model Completeness ◽

First Order ◽

First Order Theory ◽

Ordered Fields ◽

Definable Sets ◽

The Cross ◽

Primitive Recursive

To eliminate quantifiers in the first-order theory of the p-adic field Qp, Ax and Kochen use a language containing a symbol for a cross-section map n → pn from the value group Z into Qp [1, pp. 48–49]. The primitive-recursive quantifier eliminations given by Cohen [2] and Weispfenning [10] also apply to a language mentioning the cross-section, but none of these authors seems entirely happy with his results. As Cohen says, “all the operations… introduced for our simple functions seem natural, with the possible exception of the map n → pn” [2, p. 146]. So all three authors show that various consequences of quantifier elimination—completeness, decidability, model-completeness—also hold for a theory of Qp not employing the cross-section [1, p. 453; 2, p. 146; 10, §4]. Macintyre directs a more specific complaint against the cross-section [5, p. 605]. Elementary formulae which use it can define infinite discrete subsets of Qp; yet infinite discrete subsets of R are not definable in the language of ordered fields, and so certain analogies between Qp and R suggested by previous model-theoretic work seem to break down.To avoid this problem, Macintyre gives up the cross-section and eliminates quantifiers in a theory of Qp written just in the usual language of fields supplemented by a predicate V for Qp's valuation ring and by predicates Pn for the sets of nth powers in Qp (for all n ≥ 2).

Download Full-text

Theories with finitely many models

Journal of Symbolic Logic ◽

10.1017/s0022481200031236 ◽

1986 ◽

Vol 51 (2) ◽

pp. 374-376 ◽

Cited By ~ 1

Author(s):

Simon Thomas

Keyword(s):

Natural Number ◽

Complete Theory ◽

Elementary Equivalence ◽

First Order ◽

Finite Models ◽

Simple Observation ◽

Finite Structure ◽

Order Language ◽

Complete Theories

If L is a first order language and n is a natural number, then Ln is the set of formulas which only make use of the variables x1,…,xn. While every finite structure is determined up to isomorphism by its theory in L, the same is no longer true in Ln. This simple observation is the source of a number of intriguing questions. For example, Poizat [2] has asked whether a complete theory in Ln which has at least two nonisomorphic finite models must necessarily also have an infinite one. The purpose of this paper is to present some counterexamples to this conjecture.Theorem. For each n ≤ 3 there are complete theories in L2n−2andL2n−1having exactly n + 1 models.In our notation and definitions, we follow Poizat [2]. To test structures for elementary equivalence in Ln, we shall use the modified Ehrenfeucht-Fraïssé games of Immerman [1]. For convenience, we repeat his definition here.Suppose that L is a purely relational language, each of the relations having arity at most n. Let and ℬ be two structures for L. Define the Ln game on and ℬ as follows. There are two players, I and II, and there are n pairs of counters a1, b1, …, an, bn. On each move, player I picks up any of the counters and places it on an element of the appropriate structure.

Download Full-text

A finite arithmetic

Journal of Symbolic Logic ◽

10.2307/2272060 ◽

1973 ◽

Vol 38 (2) ◽

pp. 232-248 ◽

Cited By ~ 1

Author(s):

Philip T. Shepard

Keyword(s):

Number Theory ◽

Natural Number ◽

Singular Term ◽

New Method ◽

Axiomatic System ◽

Natural Numbers ◽

Substantial Loss ◽

First Order ◽

Finite Arithmetic

In this paper I shall argue that the presumption of infinitude may be excised from the area of mathematics known as natural number theory with no substantial loss. Except for a few concluding remarks, I shall restrict my concern in here arguing the thesis to the business of constructing and developing a first-order axiomatic system for arithmetic (called ‘FA’ for finite arithmetic) that contains no theorem to the effect that there are infinitely many numbers.The paper will consist of five parts. Part I characterizes the underlying logic of FA. In part II ordering of natural numbers is developed from a restricted set of axioms, induction schemata are proved and a way of expressing finitude presented. A full set of axioms are used in part III to prove working theorems on comparison of size. In part IV an ordinal expression is defined and characteristic theorems proved. Theorems for addition and multiplication are derived in part V from definitions in terms of the ordinal expression of part IV. The crucial final constructions of part V present a new method of replacing recursive characterizations by strict definitions.In view of our resolution not to assume that there are infinitely many numbers, we shall have to deal with the situation where singular arithmetic terms of FA may fail to refer. For I know of no acceptable and systematic way of avoiding such situations. As a further result, singular-term instances of universal generalizations of FA are not to be inferred directly from the generalizations themselves. Nevertheless, (i) (x)(y)(x + y = y + x), for example, and all its instances are provable in FA.

Download Full-text

A formalization of the theory of ordinal numbers

Journal of Symbolic Logic ◽

10.2307/2269620 ◽

1965 ◽

Vol 30 (3) ◽

pp. 295-317 ◽

Cited By ~ 8

Author(s):

Gaisi Takeuti

Keyword(s):

Set Theory ◽

Natural Extension ◽

Mathematical Induction ◽

Predicate Calculus ◽

Transfinite Induction ◽

First Order ◽

Recursive Functions ◽

Ordinal Numbers ◽

Primitive Recursive ◽

Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

Download Full-text

Automated complexity analysis of Nuprl extracted programs

Journal of Functional Programming ◽

10.1017/s0956796800003865 ◽

2001 ◽

Vol 11 (1) ◽

pp. 3-31 ◽

Cited By ~ 12

Author(s):

RALPH BENZINGER

Keyword(s):

Abstract Interpretation ◽

Complexity Analysis ◽

Cost Model ◽

Functional Program ◽

First Order ◽

Value Evaluation ◽

Recursive Programs ◽

Symbolic Evaluation ◽

Primitive Recursive ◽

Higher Order Functions

This paper describes the Automated Complexity Analysis Prototype (ACAp) system for automated complexity analysis of functional programs synthesized with the Nuprl proof development system. We define a simple abstract cost model for NUPRL's term language based on the current call-by-name evaluator. The framework uses abstract functions and abstract lists to facilitate reasoning about primitive recursive programs with first-order functions, lazy lists and a subclass of higher-order functions. The ACAp system automatically derives upper bounds on the time complexity of NUPRL extracts relative to a given profiling semantics. Analysis proceeds by abstract interpretation of the extract, where symbolic evaluation rules extend standard evaluation to terms with free variables. Symbolic evaluation of recursive programs generates systems of multi-variable difference equations, which are solved using the MATHEMATICA computer algebra system. The use of the system is exemplified by analyzing a proof extract that computes the maximum segment sum of a list and a functional program that determines the minimum of a list via sorting. For both results, we compare call-by-name to call-by-value evaluation.

Download Full-text

Cardinality logics. Part II: Definability in languages based on ‘exactly’

Journal of Symbolic Logic ◽

10.2307/2274570 ◽

1988 ◽

Vol 53 (3) ◽

pp. 765-784 ◽

Cited By ~ 1

Author(s):

Harold Hodes

Keyword(s):

Natural Number ◽

Higher Order ◽

Semantic Role ◽

Singular Terms ◽

First Order ◽

The Third ◽

Ordinary Usage ◽

Quantifier Phrases

This paper continues the project initiated in [5]: a model-theoretic study of the concept of cardinality within certain higher-order logics. As recommended by an editor of this Journal, I will digress to say something about the project's motivation. Then I will review some of the basic definitions from [5]; for unexplained notation the reader should consult [5].The syntax of ordinary usage (with respect to the construction of arguments as well as the construction of individual sentences) makes it natural to classify numerals and expressions of the form ‘the number of F's’ as singular terms, expressions like ‘is prime’ or ‘is divisible by’ as predicates of what Frege called “level one”, and expressions like ‘for some natural number’ as first-order quantifier-phrases. From this syntatic classification, it is a short step—so short as to be frequently unnoticed—to a semantic thesis: that such expressions play the same sort of semantic role as is played by the paradigmatic (and nonmathematical) members of these lexical classes. Thus expressions of the first sort are supposed to designate objects (in post-Fregean terms, entities of type 0), those of the second sort to be true or false of tuples of objects, and those of the third sort to quantify over objects. All this may be summed up in Frege's dictum: “Numbers are objects.”

Download Full-text

HALF-MONOPOLE AND MULTIMONOPOLE

International Journal of Modern Physics A ◽

10.1142/s0217751x05020811 ◽

2005 ◽

Vol 20 (10) ◽

pp. 2195-2204 ◽

Cited By ~ 6

Author(s):

ROSY TEH ◽

K. M. WONG

Keyword(s):

Natural Number ◽

Topological Charge ◽

Magnetic Charge ◽

Axially Symmetric ◽

Yang Mills ◽

First Order ◽

Half Integer

We would like to present some exact SU(2) Yang–Mills–Higgs monopole solutions of half-integer topological charge. These solutions can be just an isolated half-monopole or a multimonopole with topological magnetic charge ½m where m is a natural number. These static monopole solutions satisfy the first order Bogomol'nyi equations. The axially symmetric one-half monopole gauge potentials possess a Dirac-like string singularity along the negative z-axis. The multimonopole gauge potentials are also singular along the z-axis and possess only mirror symmetries.

Download Full-text

FIELDS WITH SEVERAL COMMUTING DERIVATIONS

Journal of Symbolic Logic ◽

10.1017/jsl.2013.19 ◽

2014 ◽

Vol 79 (01) ◽

pp. 1-19 ◽

Cited By ~ 11

Author(s):

DAVID PIERCE

Keyword(s):

Natural Number ◽

Geometric Characterization ◽

Model Companion ◽

First Order ◽

Existentially Closed ◽

Differential Fields ◽

Theory Of Fields ◽

Differential Varieties

AbstractFor every natural numberm, the existentially closed models of the theory of fields withmcommuting derivations can be given a first-order geometric characterization in several ways. In particular, the theory of these differential fields has a model-companion. The axioms are that certain differential varieties determined by certain ordinary varieties are nonempty. There is no restriction on the characteristic of the underlying field.

Download Full-text

A converse of the Barwise completeness theorem

Journal of Symbolic Logic ◽

10.2307/2271985 ◽

1973 ◽

Vol 38 (4) ◽

pp. 594-612

Author(s):

Jonathan Stavi

Keyword(s):

Completeness Theorem ◽

The Body ◽

Cut Elimination ◽

Closed Set ◽

First Order ◽

Admissible Sets ◽

Inductive Definitions ◽

Closure Conditions ◽

Primitive Recursive ◽

The Universe

In this paper a converse of Barwise's completeness theorem is proved by cut-elimination considerations applied to inductive definitions. We show that among the transitive sets T satisfying some weak closure conditions (closure under primitive-recursive set-functions is more than enough), only the unions of admissible sets satisfy Barwise's completeness theorem in the form stating that if φ ∊ T is a sentence which has a derivation (in the universe) then φ has a derivation in T. See §1 for the origin of the problem in Barwise's paper [Ba].Stated quite briefly the proof is as follows (a step-by-step account including relevant definitions is given in the body of the paper):Let T be a transitive prim.-rec. closed set, and let is nonempty, transitive and closed under pairs}. For each let κ(A) be the supremum of closure ordinals of first-order positive operators on subsets of A (first-order with respect to By Theorem 1 of [BGM], it is enough to prove that rank(T) in order to obtain that T is a union of admissible sets. (The rank of a set is defined by rank(x) = supy ∊ x (rank(y) + 1); since T is prim.-rec. closed, rank(T) = smallest ordinal not in T.)Let We show how to find in T (in fact, in Lω(A)) a derivable sentence τ that has no derivation D such that rank(D) ≤ α. Thus, if τ is to have a derivation in T, rank(T) > α. α is arbitrary (< κ(A)), so rank(T) ≥ κ(A). Q.E.D.

Download Full-text