Elementary Theory of Real Numbers

Erwin Engeler
Additional contact information
Erwin Engeler: ETH-Zentrum, Mathematikdepartment

Chapter § 3 in Foundations of Mathematics, 1993, pp 14-28 from Springer

Abstract: Abstract The axiomatization presented in the previous section is an attempt to axiomatize the set of theorems true in the intended structure. How well does it do this? The best for which one can hope in an axiomatization is that it can serve as the basis for an effective decision procedure, i.e. a procedure which, given any sentence S of the language, decides in finitely many steps whether or not S is true in the intended structure. The most informative decision procedures are those which proceed by quantifier elimination. This method is also the oldest. It was applied in the twenties by Langford to the theory of dense orderings, by Presburger to the (additive) theory of the integers, and finally by Tarski to the theory that we are considering. The paper by Yu. Ershov, mentioned in the references, surveys numerous subsequent applications of the method.

Keywords: Decision Procedure; Induction Assumption; Atomic Formula; Elementary Theory; Existential Quantifier (search for similar items in EconPapers)
Date: 1993
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-3-642-78052-3_3

Ordering information: This item can be ordered from
http://www.springer.com/9783642780523

DOI: 10.1007/978-3-642-78052-3_3

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().