Computing with Reals and Decidability of Elementary Geometry, ETH 2004
Prof. J.A. Makowsky
e-mail address for comments and questions:
janos@cs.technion.ac.il
makowsky@math.ethz.ch
Office ETH: HG-J16.4, Tel: (01-63) 23358
Previously updated: April 21, 2004
Last updated:
May 11, 2004
Special announcements:
No lecture on Wednesday, June 16, 2004
This page contains material for the course
Computing with Reals and Decidability of Elementary Geometry
given at the D-MATH of ETHZ in the summer semester 2004.
It is partially based on my courses
Computing over the Reals
and
Automated Theorem Proving
given irregularly at the Computer Science Department of
the Technion - Israel Institute of Technology.
Abstracts of ETH-lectures
- 31.3.2004
Introduction.
What is geometry?
Tarski's Theorem:
The deciability of elementary geometry (outline only).
What are the complexity classes P and NP
over arithmetic structures (outline only).
First order logic over arithmetic structures.
Terms and their meaning.
- 07.4.2004
First order logic over arithmetic structures.
Formulas and their meaning.
Exact statement of Tarski's Theorem:
Th(R) is computable.
But Th(N), Th(Z), Th(Q) are not.
- 14.4.2004
The First order theory of infinite sets
is computable.
An example of computing the truth value of a formula
with equality only.
The method of quantifier elimination.
A complete axiomatization of Th(Infinite sets).
Proof of completeness using:
- Isomorphic structures cannot be distinguished
with First order logic statements.
- Goedel's completeness theorem for First order Logic.
- The Loewenheim-Skolem-Tarski-Mal'cev Theorem.
It is about the possible infinite cardinalities of models
of a countable theory
(namely: all infinite cardinalities
are possible).
- 21.4.2004
Quantifier elimination for the theory of infinite sets.
Conjunctive and disjunctive normal forms (CNF and DNF)
for quantifierfree formulas.
Prenex normal forms for quantified formulas.
General strategy of quantifier elimination:
-
Put formula into prenex normal form
-
Eliminate innermost quantifier (w.l.o.g it can be assumed to be existential)
by using DNF of quantifierfree part.
-
Separate variables.
- If bound variable to be eliminated occurs in an equality
use substitutions.
-
Otherwise use the fact that the universe is infinite.
- 28.4.2004
The theory of dense linear orders.
Quantifier elimination using complete configurations.
Quantifier elimination using the Fourier-Motzkin method.
- 5.5.2004
The theory of the reals
as ordered abelian groups has quantifier elimination.
Counterexamples to Q.E.
-
Th([Z,<]) does not have quantifier elimination.
The proof we gave was based on the fact that
q.f. formulas are preserved under substructures.
The substructure we used was <2Z,<> with
Th([Z,<])= Th([2Z,<]).
We conclude that over
Th([Z,<]) the formula \exists x (y < x & x < z )
is not equivalent to a q.f. formula.
-
Th([R,+,-, \times, 0,1]) does not have quantifier elimination.
We tried the same trick using [Q,+,-, \times, 0,1].
But this does only show that over the axioms of
fields the formula \exists y (yy=x) is not equivalent
to a q.f. formula.
NOTE:
We would like to show that over
Th([Q,+,-, \times, 0,1]) the same holds.
Can you complete the proof?
We introduced Skolem functions and gave an
more efficient Q.E. for
Th([R,+,-, <, 0,1]).
THis proof is due to Ferrante and Rackoff (1974).
- 12.5.2004
Completion of counterexamples of previous lecture.
Robinson's abstract quantifier elimination theorem.
The theory of the complex numbers as fields ACF_0
has Q.E. (via Steinitz' structure theorem
for algebraically closed fields)
- 19.5.2004
Planned:
The theory of the reals
and as ordered fields.
Sturm sequences and Tarski's theorem.
- 26.5.2004
Planned:
Computability over the reals