Timeline for What are examples of (collections of) papers which "close" a field?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 6, 2021 at 13:40 | comment | added | Adam P. Goucher | You can convert homogeneous rational equations in side lengths (such as $a^2 + b^2 = c^2$) into equivalent Tarski-geometric statements. In particular, convert it to a rational equation of degree 1 (e.g. $a^2/c + b^2/c = c$), construct each of the monomial terms using repeated application of the Intersecting Chords Theorem, and sum the terms on each side of the equation by concatenating lengths. | |
| Jul 6, 2021 at 7:37 | comment | added | user44143 | Tarski's result says nothing about area, so it omits a large part of the ancient field of Euclidean geometry -- even Euclid's statement of the Pythagorean theorem! mathcs.clarku.edu/~djoyce/java/elements/bookI/propI47.html: "In right-angled triangles the square on the side opposite the right angle equals the sum of the squares on the sides containing the right angle." | |
| Jan 19, 2020 at 2:51 | comment | added | user21820 | I don't know what exactly is the state-of-art now, but just a few years back I remember putting some elegant non-contrived geometry problem into some prover and it produced a corresponding polynomial with degree something like $48$, and did not finish proving the theorem (I don't recall what the problem was or how long I ran the prover for). And anyway, I can easily state some ancient geometry problems that you can't express in Tarski's axiomatization, such as Steiner's porism and Poncelot's porism. | |
| Jan 17, 2020 at 18:21 | comment | added | Adam P. Goucher | Doubly-exponential in the number of times you alternate between universal and existential quantifiers. Are there any non-contrived geometry problems which alternate many times between universal and existential quantifiers? | |
| Dec 6, 2019 at 3:30 | comment | added | user21820 | I don't agree with this answer at all. The theory of real-closed fields that underlies Tarski's theory of Euclidean geometry requires doubly-exponential time to decide, so numerous geometry problems remain unreachable by the decision procedure within human time scales. Furthermore, Tarski's axiomatization is not the only one; it is weaker than Hilbert's axiomatization, and the latter is in fact essentially incomplete. | |
| S Dec 4, 2019 at 19:28 | history | answered | Adam P. Goucher | CC BY-SA 4.0 | |
| S Dec 4, 2019 at 19:28 | history | made wiki | Post Made Community Wiki by Adam P. Goucher |