On models of the elementary theory of (Z, +, 1)

1990 ◽  
Vol 55 (1) ◽  
pp. 1-20 ◽  
Author(s):  
Mark Nadel ◽  
Jonathan Stavi
Keyword(s):  
Stability Theory ◽  
Elementary Theory ◽  
Additive Group ◽  
Order Theory ◽  
Point Of View ◽  
Real Numbers ◽  
First Order ◽  
First Order Theory ◽  
Distinguished Element ◽  
Unbounded Subset

Let T1 be the complete first-order theory of the additive group of the integers with 1 as distinguished element (in symbols, T1 = Th(Z, +, 1)). In this paper we prove that all models of T1 are ℵ0-homogeneous (§2), classify them (and lists of elements in them) up to isomorphism or L∞κ-equivalence (§§3 and 4) and show that they may be as complex as arbitrary sets of real numbers from the point of view of admissible set theory (§5). The results of §§2 and 5 together show that while the Scott heights of all models of T1 are ≤ ω (by ℵ0-homogeneity) their HYP-heights form an unbounded subset of the cardinal .In addition to providing this unusual example of the relation between Scott heights and HYP-heights, the theory T1 has served (using the homogeneity results of §2) as an example for certain combinations of properties that people had looked for in stability theory (see end of §4). In §6 it is shown that not all models of T = Th(Z, +) are ℵ0-homogeneous, so that the availability of the constant for 1 is essential for the result of §2.The two main results of this paper (2.2 and essentially Theorem 5.3) were obtained in the summer of 1979. Later we learnt from Victor Harnik and Julia Knight that T1 is of some interest for stability theory, and were encouraged to write up our proofs.During 1982/3 we improved the proofs and added some results.

scholarly journals Quasi-decidability of a Fragment of the First-Order Theory of Real Numbers

2015 ◽  
Vol 57 (2) ◽  
pp. 157-185 ◽  
Author(s):  
Peter Franek ◽  
Stefan Ratschan ◽  
Piotr Zgliczynski
Keyword(s):  
Order Theory ◽  
Real Numbers ◽  
First Order ◽  
First Order Theory

Implementing the cylindrical algebraic decomposition within the Coq system

2007 ◽  
Vol 17 (1) ◽  
pp. 99-127 ◽  
Author(s):  
ASSIA MAHBOUBI
Keyword(s):  
Programming Language ◽  
Decision Procedure ◽  
Order Theory ◽  
Decomposition Algorithm ◽  
Proof Assistant ◽  
Real Numbers ◽  
First Order ◽  
Cylindrical Algebraic Decomposition ◽  
First Order Theory ◽  
Automation Tools

The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.

LOGICAL ASPECTS OF CAYLEY-GRAPHS: THE MONOID CASE

2006 ◽  
Vol 16 (02) ◽  
pp. 307-340 ◽  
Author(s):  
DIETRICH KUSKE ◽  
MARKUS LOHREY
Keyword(s):  
Cayley Graph ◽  
Cayley Graphs ◽  
Order Theory ◽  
Second Order ◽  
Point Of View ◽  
Direct Products ◽  
Graph Products ◽  
Arbitrary Graph ◽  
First Order ◽  
First Order Theory

Cayley-graphs of monoids are investigated under a logical point of view. It is shown that the class of monoids, for which the Cayley-graph has a decidable monadic second-order theory, is closed under free products. This result is derived from a result of Walukiewicz, stating that the decidability of monadic second-order theories is preserved under tree-like unfoldings. Concerning first-order logic, it is shown that the class of monoids, for which the Cayley-graph has a decidable first-order theory, is closed under arbitrary graph products, which generalize both, free and direct products. For the proof of this result, tree-like unfoldings are generalized to so-called factorized unfoldings. It is shown that the decidability of the first-order theory of a structure is preserved by factorized unfoldings. Several additional results concerning factorized unfoldings are shown.

A NEW FORMALIZATION OF FEFERMAN’S SYSTEM OF FUNCTIONS AND CLASSES AND ITS RELATION TO FREGE STRUCTURE

1995 ◽  
Vol 06 (03) ◽  
pp. 187-202 ◽  
Author(s):  
SUSUMU HAYASHI ◽  
SATOSHI KOBAYASHI
Keyword(s):  
Finite Number ◽  
Order Theory ◽  
Point Of View ◽  
The Other ◽  
Technical Result ◽  
Technical Point ◽  
First Order ◽  
First Order Theory

A new axiomatization of Feferman’s systems of functions and classes1,2 is given. The new axiomatization has a finite number of class constructors resembling the proposition constructors of Frege structure by Aczel.3 Aczel wrote “It appears that from the technical point of view the two approaches (Feferman’s system and Frege structure) run parallel to each other in the sense that any technical result for one approach can be reconstructed for the other”.3 By the aid of the new axiomatization, Aczel’s observation becomes so evident. It is now straightforward to give a mutual interpretation between our formulation and a first order theory of Frege structure, which improve results by Beeson in Ref. 4.

The incompleteness theorems

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Mathematical Reasoning ◽  
Order Theory ◽  
Point Of View ◽  
Incompleteness Theorem ◽  
Bertrand Russell ◽  
First Order ◽  
First Order Theory ◽  
Incompleteness Theorems ◽  
Special Case ◽  
Gödel’S Incompleteness Theorems

In this chapter we prove that the structure N = (ℕ|+, · , 1) has a first-order theory that is undecidable. This is a special case of Gödel’s First Incompleteness theorem. This theorem implies that any theory (not necessarily first-order) that describes elementary arithmetic on the natural numbers is necessarily undecidable. So there is no algorithm to determine whether or not a given sentence is true in the structure N. As we shall show, the existence of such an algorithm leads to a contradiction. Gödel’s Second Incompleteness theorem states that any decidable theory (not necessarily first-order) that can express elementary arithmetic cannot prove its own consistency. We shall make this idea precise and discuss the Second Incompleteness theorem in Section 8.5. Gödel’s First Incompleteness theorem is proved in Section 8.3. Although they are purely mathematical results, Gödel’s Incompleteness theorems have had undeniable philosophical implications. Gödel’s theorems dispelled commonly held misconceptions regarding the nature of mathematics. A century ago, some of the most prominent mathematicians and logicians viewed mathematics as a branch of logic instead of the other way around. It was thought that mathematics could be completely formalized. It was believed that mathematical reasoning could, at least in principle, be mechanized. Alfred North Whitehead and Bertrand Russell envisioned a single system that could be used to derive and enumerate all mathematical truths. In their three-volume Principia Mathematica, Russell and Whitehead rigorously define a system and use it to derive numerous known statements of mathematics. Gödel’s theorems imply that any such system is doomed to be incomplete. If the system is consistent (which cannot be proved within the system by Gödel’s Second theorem), then there necessarily exist true statements formulated within the system that the system cannot prove (by Gödel’s First theorem). This explains why the name “incompleteness” is attributed to these theorems and why the title of Gödel’s 1931 paper translates (from the original German) to “On Formally Undecidable Propositions of Principia Mathematica and Related Systems” (translated versions appear in both [13] and [14]). Depending on one’s point of view, it may or may not be surprising that there is no algorithm to determine whether or not a given sentence is true in N.

scholarly journals Note About a New Evaluation of the Direct Perturbations of the Planets on the Moon’s Motion

1981 ◽  
Vol 63 ◽  
pp. 265-266
Author(s):  
D. Standaert
Keyword(s):  
Order Theory ◽  
Second Order ◽  
Point Of View ◽  
Internal Point ◽  
First Order ◽  
Keplerian Orbits ◽  
First Order Theory ◽  
External Point ◽  
Constants Of Motion ◽  
The Mean

The aim of this paper is to present the principal features of a new evaluation of the direct perturbations of the planets on the Moon’s motion. Using the method already published in Celestial Mechanics (Standaert, 1980), we compute “a first-order theory” aiming at an accuracy of the order of the meter for all periodic terms of period less than 3 500 years.From an external point of view, we mean by that: a)keplerian orbits for the planets,b)the ELP-2000 solution of the Main Problem proposed by Mrs. Chapront (Chapront-Touzë, 1980),c)the first-order derivatives with respect to the constants of motion of the SALE theory of Henrard (Henrard, 1979).On the other hand, from an internal point of view, the computations include: d)the development in Legendre polynomials not only to the first-order in (a/a'), but also the following ones (up to the sixth-order for Venus, for example),e)the contributions of the second-order in the Lie triangle,f)second-order contributions coming from the corrections of the mean motions due to the planetary action.

Locally finite theories

1986 ◽  
Vol 51 (1) ◽  
pp. 59-62 ◽  
Author(s):  
Jan Mycielski
Keyword(s):  
Main Idea ◽  
Order Theory ◽  
Interpolation Theorem ◽  
Point Of View ◽  
Finite Model ◽  
Consistent Theory ◽  
Locally Finite ◽  
First Order ◽  
First Order Theory ◽  
Finite Theory

We say that a first order theoryTislocally finiteif every finite part ofThas a finite model. It is the purpose of this paper to construct in a uniform way for any consistent theoryTa locally finite theory FIN(T) which is syntactically (in a sense) isomorphic toT.Our construction draws upon the main idea of Paris and Harrington [6] (I have been influenced by some unpublished notes of Silver [7] on this subject) and generalizes the syntactic aspect of their result from arithmetic to arbitrary theories. (Our proof is syntactic, and it is simpler than the proofs of [5], [6] and [7]. This reminds me of the simple syntactic proofs of several variants of the Craig-Lyndon interpolation theorem, which seem more natural than the semantic proofs.)The first mathematically strong locally finite theory, called FIN, was defined in [1] (see also [2]). Now we get much stronger ones, e.g. FIN(ZF).From a physicalistic point of view the theorems of ZF and their FIN(ZF)-counterparts may have the same meaning. Therefore FIN(ZF) is a solution of Hilbert's second problem. It eliminates ideal (infinite) objects from the proofs of properties of concrete (finite) objects.In [4] we will demonstrate that one can develop a direct finitistic intuition that FIN(ZF) is locally finite. We will also prove a variant of Gödel's second incompleteness theorem for the theory FIN and for all its primitively recursively axiomatizable consistent extensions.The results of this paper were announced in [3].

Sign in / Sign up

Export Citation Format

Share Document