Talk:Tarski's axioms

I'm the anonymous user who wrote this article, sorry. I do actually have an account. Gene Ward Smith 8 July 2005 18:50 (UTC)

Are you sorry for not using your account or for writing the article? :)

Thanks for your work! Oleg Alexandrov 9 July 2005 02:29 (UTC)

---

I think there are a few typos in the Axiom schema of completeness. I am confused which variables occur in which formula and what you mean by the dots.

216.250.179.7 07:21, 3 January 2006 (UTC) Yeah, the completeness axiom is definitely typo-riddled. I would've tried to fix it myself, but I didn't want to expend the mental energy.

My extensive revisions

I am the anonymous polisher of this article, mainly because of my admiration for Alfred Tarski, and because I was fascinated to discover in middle age that Euclidian geometry, as it was (is?) taught in high school texts is logically flawed. I have hard copy of Szczerba (1986) on my desk, and urge any of you deeply interested in this entry to read him carefully. I take his statement of Tarski's axioms as the definitive one in the English language. Evidence, by the way, of Tarski's deep commitment to elementary geometry is the 40pp letter he wrote in 1978 to Schwabhäuser. That letter has been published in revised form as Tarski and Givant (1999).

I have:

• Cleaned up the axiom schema of Completeness and renamed it Continuity;
• Modified Pasch as per Schwabhäuser et al (1983), Tarski's swan song, so that Transitivity and Connectivity of betweenness are now theorems;
• Altered the notation as follows. To say that ab is congruent with cd, I follow Tarski and write Cabcd but ab ≡ cd rather than Cabcd. To say that b is between a and c, I drop the predicate letter B and simply write abc. Here I deviate from Tarski;
• Revised the verbal summaries of the axioms, and added a few of my own (I'll write description of what Five Segments does, manana);
• I have eliminated the tedious dance of subscripts in Five Segments in favor of Tarski's prime notation;
• Expanded 2-3 sentences in the entry to a section titled "Discussion." I invite those competent in metamathematics to revise and expand this section;
• Added some references.

The true power of Tarski's axioms emerges when it is seen that straightforward (but tedious to express) generalizations of Upper and Lower Dimension suffice to axiomatize Euclidian geometry for any finite number of dimensions. In Hilbert's axioms, the shift from plane to solid geometry requires adding planes to the domain, and 6 new axioms.202.36.179.65 09:30, 18 March 2006 (UTC)

Attention Mathematicians

In order of increasing difficulty, perhaps...

• How does one define betweenness from congruence? Szczerba (1986) asserts this is possible when the dimensionality > 1, but gives no details.

Given a pair of distinct points p and q, the set of all points x such that px=qx is a n-1 dimensional hyperplane. Three pairwise points are colinear points provided that any hyperplane which contains two of the points also contains the third. So we can talk about lines.

Given a points p and q, you can talk about the n-1 dimensional hypersphere centered at p and passing thru q as the set of all x such that px=pq. (The degenerate case p=q gives a point.)

The midpoint of the line segment from p to q (p, q distinct) is the unique m such that pm=qm and all three of p,q,m are colinear. (If p=q, we define m=p.)

x is between p and q provided that any line which passes thru the point x intersects the hypersphere centered at the midpoint m (of the line segment from p to q) and passing thru p and q.

--Ramsey2006 00:05, 20 October 2006 (UTC)

• Can Five Segment be replaced by something with fewer atomic sentences? As things stand, Five Segment accounts for 9 of the 44 atomic sentences in this axiom set.
• Can axioms in this spirit be found for affine, projective, and Riemannian geometries? The matter of how Euclidian is a special case of Riemannian should then be revisited.
• Reflexivity of Congruence and Pasch have not been proved independent of the other axioms. The Holy Grail here is a fully independent axiom set.

202.36.179.65 19:00, 21 March 2006 (UTC)

My understanding is that affine or projective geometries can be easily described by eliminating the axioms having betweenness or congruence, respectively. I'll try to verify this. Adam 02:45, 28 April 2006 (UTC)

Diagrams of the axioms would be nice...

The axioms are not illustrated because I do not know how to upload images (scanned from Tarski and Givant 1999) to Wikipedia.202.36.179.65 19:49, 26 March 2006 (UTC)

Note about first order and finitly axiomatizable

I deleted a remark saying that hilbert aximatic is not first order because of quantification over lines. I think it is false because lines are nto defined as a set of points in hilbert, lines could be anything. I also deleted a comment saying that euclidean geometry is not finitly axiomatizable beacause the result of Tarski says that epsilon2 is not equivalent to a finite axiomatic system expressed *in the language of epsilon2*. The question of the language is important because othewise it can be finitly axiomtized. So i think the comment is misleading. —The preceding unsigned comment was added by Jnarboux (talk • contribs) 15:06, 23 May 2006 (UTC)

I've reinstated both. Hilbert's axioms are heavily non-first-order for reasons much more important than quantification over lines. Finite non-axiomatizability of Euclidean geometry is an important property and should be mentioned, though you are right that care with the language is in order. Nevertheless, I'd love to see a complete finite FO axiomatization of geometry in any nontrivial language. -- EJ 23:51, 7 August 2006 (UTC)

Axioms

The schema of continuity given in the article is nonsense, it is logically equivalent to the single formula

$\forall a\,(axy)\to \exists b\,(xby)$,

which moreover follows from the dimension axioms. I'll try to lookup the correct statement. -- EJ 00:16, 8 August 2006 (UTC)

Done. I also made the axioms more in line with Tarski's formulation, undoing the omission of B and prenexation of the formulas, which only served to make it unreadable. -- EJ 01:42, 8 August 2006 (UTC)

Definition of partial order relation <=

What does "ywuv" mean in xy≤zu↔∀v(zv≡uv→∃w(xw≡yw∧ywuv)) ? Is this definition a wff? Otto 17:51, 27 August 2006 (UTC)

Congruence is not an equivalence relation

Now it says that "congruence is an equivalence relation", but that cannot be the case, because congruence is a quaternery relation and an equivalence relation is binary. I do not see how you can construct an equivalence relation out of congruence. It should be possible if you can construct an ordered pair of points and so define a binary relation of congruence between two ordered pairs of points. I do not see how to get there. Otto 20:49, 27 August 2006 (UTC)

And where exactly do you want to get? Congruence is formally a quaternary relation on points, but it can be considered a binary relation on pairs of points (or on line segments, if you wish). Indeed, the notation $xy\equiv zw$ strongly suggests such interpretation, and it is the only way to make any intuitive sense of the predicate. Now, as a relation on pairs, congruence is reflexive, transitive, and symmetric, hence an equivalence relation. In fact, congruence is a prototypic equivalence: it was the first equivalence relation recorded in history, and its name was thus adopted for other equivalence relations in modular arithmetic, universal algebra, etc., see congruence relation. What more do you expect? -- EJ 19:02, 29 August 2006 (UTC)

EJ, what you ask me is a rhetoric question. It is easy to talk here about "pairs of points", but that doesn't solve the problem. I asked for a definition of that concept within the language of Tarksi's axioms. Or alternatively, a definition from congruence as a binary relation. The text as it was before I changed it, was confusing, because it didn't comply with the ordinary meaning of an equivalence relation, which is binary. Otto 20:17, 29 August 2006 (UTC)

But there is no problem to solve, that's the point. Equivalence is a reflexive, symmetric, and transitive relation, period, there is no requirement in the definition that its domain contains only points, not pairs. I don't understand what you mean by "within the language of Tarski's axioms". Sure, pairs of points are not a primitive notion in Tarski's language, but we can talk about pairs in the theory because concepts involving pairs are trivially definable in the language. We have an infinite supply of variables for points, so we just use two of them when we need to speak about a pair. That's the usual modus operandi in axiomatic theories: we keep the basic language minimal, and we introduce other concepts by definitions. For example, read the descriptions of the axioms as given in the article: it mentions "distance", "line segment", "triangle", "intersect", "collinear", "midpoint", "angle", "circle", none of which are primitive concepts, but are easily definable.

So back to the "problem". The original formulation could do with specification of the domain of the equivalence (the original author presumably omitted it because it is obvious), but blurring it by insertion of words like "suggest" and "similar" only makes it more confusing. -- EJ 21:06, 29 August 2006 (UTC)

Elementary?

What does the term "elementary geometry" mean here, as opposed to "full geometry"? —Jorend 23:15, 17 November 2006 (UTC)

In this context, "elementary" is a synonym for first-order. -- EJ 13:50, 20 November 2006 (UTC)

Thanks, EJ. —Jorend 19:22, 20 November 2006 (UTC)

Axiom schema of Continuity Question

Something seems wrong. Let $a=(0,0$) in $R^{2}$ let $X=\{x|\phi (x)\}=\{({\frac {1}{2}},0),({\frac {3}{4}},0),({\frac {7}{8}},0),({\frac {15}{16}},0),\ldots \}$ and $Y=\{y|\psi (y)\}=\{(1,0)\}$. I can't think of a $b$ that satisfies that axiom for ALL $x$. Should it be:

$\exists a\,\forall x\,\forall y\,[(\phi (x)\land \psi (y))\rightarrow Baxy]\rightarrow \forall x\,\forall y\,[(\phi (x)\land \psi (y))\rightarrow \exists b\,Bxby]?$

--71.3.208.120 (talk) 18:27, 7 September 2008 (UTC) Wait, no that doesn't do what you are looking for does it? You're looking for a nice definition of Dedekind cuts, right? The normal way of saying this is that every set with an upper bound has a _least_ upper bound.

So is $Bxyy$ always true for all $x$ and $y$? If that's the case then for the example, set $b=(1,0)$, and you are done.

My problem was an assumption that betweenness concotated _strict_ betweenness, which isn't true. --Hal Canary (talk) 20:54, 7 September 2008 (UTC)

Axiom of Euclid

The B-version of the Axiom of Euclid states in English that "Given any triangle, there exists a circle that includes all of its vertices." I don't see why this excludes spherical geometry, it seems to me that this is true also on a sphere (also in the formal form).

In hyperbolic geometry this axiom seems not true. This can be seen from the Poincare disk projection of the hyperbolic plane, in that projection circles stay circles (iirc) and selecting three points close to the edge would require a circle that crosses the boundary of the disk.

Further down the article says "Negating the Axiom of Euclid yields hyperbolic geometry" without a mention of spherical geometry. Perhaps it is the case that one of the other axioms already excludes spherical geometry? If that is the case, than the wording in the "Axiom of Euclid" section should note that (at least) the B variant is only equivalent with Euclids parallel postulate when combined with that other axiom.

The same seems to be the case with the C variant of the axiom. It can easily be shown to be not true in hyperbolic geometry (take v far enough away so that when a and b are pushed to there affine limit, ab will not include v) but I can't find any example where this is false in spherical geometry. Although I haven't tried very hard.

Can someone enlighten me on this? —Preceding unsigned comment added by BlackShift (talk • contribs) 15:50, 4 November 2008 (UTC)

Obviously, the three version of Euclid's axiom are only supposed to be equivalent over all the other axioms of the theory. It does not make much sense to ask them to be equivalent on their own. — Emil J. 16:09, 4 November 2008 (UTC)

The text is somewhat confusing then, because it states that all three versions are equivalent to Euclids parallel postulate which is not even part of the theory. Negating/removing that postulate gives the possibility of a spherical geometry as well as a hyperbolic one. So I inferred that the same would hold for these three axioms since they are said to be equivalent to it, however this is apparently not true (only hyperbolic). Therefore, the axioms are not (all three) equivalent to the parallel postulate.

The axiom that excludes a spherical geometry is the "Identity of Betweenness". In a spherical geometry, Bxyx does not infer y=x, in fact I suppose in spherical geometry any y is Bxyx. I think this is only relevant to variant B and C of the axiom.BlackShift (talk) 17:38, 4 November 2008 (UTC)

From the other axioms one can deduce the existence of parallel lines, so the other axioms exclude spherical geometry (JulienNarboux). — Preceding unsigned comment added by 2A01:E35:2E78:9EA0:AC05:E2AC:88FA:A9E0 (talk) 08:46, 13 May 2015 (UTC)

References

According to MathSciNet, the bibliographic data for Tarski's 1959 paper is:

\bib{MR0106185}{article}{
   author={Tarski, Alfred},
   title={What is elementary geometry?},
   conference={
      title={The axiomatic method. With special reference to geometry and
      physics. Proceedings of an International Symposium held at the Univ.
      of Calif., Berkeley, Dec. 26, 1957-Jan. 4, 1958 (edited by L. Henkin,
      P. Suppes and A. Tarski)},
   },
   book={
      series={Studies in Logic and the Foundations of Mathematics},
      publisher={North-Holland Publishing Co.},
      place={Amsterdam},
   },
   date={1959},
   pages={16--29},
   review={\MR{0106185 (21 \#4919)}},
}

I am going to fix the reference to reflect this. — Carl (CBM · talk) 18:24, 30 June 2010 (UTC)

As long as I'm looking at this article, I'm going to restore the original parenthetical referencing style, as in this revision, with inline references rather than footnotes. I do not object to the linking templates, but I will need to format the Franzen reference using a template so that I get the anchor to link to. I may change all the other refs to use the citation template as well, unless someone objects. That would permit linking all the inline references. — Carl (CBM · talk) 19:14, 30 June 2010 (UTC)

Carl:The Tarski talk was presented at the conference in 1957, as pointed out in the preface to the source I cited, which is an exact reprint of the North Holland version.. However, the source I cited is available in toto on line at the provided url, a great convenience to anyone interested in reading it, the earlier one is not. The publication date for the source cited is stated and it is 2007.

I fixed the citation so (Tarski, 1957) would show up as the harvard link. I provided the actual publication date of the cited source and provided the date of the talk in the citation data. Where, exactly , is the problem here? Brews ohare (talk) 23:10, 30 June 2010 (UTC)

Btw, none of the name-date references you included in-line are proper harvard links except for the first one that I set up. They do not link to the sources in the reference list. Brews ohare (talk) 23:17, 30 June 2010 (UTC)

The only ones that should link at the moment are Franzén 2005 and Tarski 1959. I just checked them, and they do. The others are just inline references at the moment, but not linked. I have no objection to the linking, but it's not a requirement for author-date referencing and I usually don't bother with it because of fragility problems that might be historical now.

As for the year, the publication date of the paper is 1959, which is what I wanted to double-check. The publication date, by convention, is the date cited in mathematics; it would not matter if the paper was presented orally in 1957, 1952, or 1935. We should cite the original publication, not the reprint. I have no objection to adding a courtesy link to the reprint, of course. — Carl (CBM · talk) 00:13, 1 July 2010 (UTC)

The in-line indicator in the article is (Tarski, 1959) and its purpose is to locate a particular citation in the reference list. It could just as well be (Tarski, #1) or (Tarski, a1) or simply (Ref #1). It really is only an arbitrary choice to make the identifier in-line the date of first publication, just as it is arbitrary to make it the date of presentation of the paper.

On the other hand, the citation itself should provide real information useful in finding the source, and so should refer to the actual date of publication. As things stand at the moment, the citation provides info on the old North Holland original proceedings publication, while the url link is to the new 2007 reprint of that volume which is not identified. However, the isbn is for the Reprint. That strikes me as an odd hodgepodge arrangement. Of course the useful info to the reader locates the 2007 Reprint, not the antiquarian original North Holland version. There is no purpose served in emphasizing the North Holland citation: it is largely replaced by the new Reprint, and the Reprint is cheaper and easier to find, and provides on-line access to the full text of this paper. Brews ohare (talk) 03:10, 1 July 2010 (UTC)

Sorry; I copied the ISBN from the old citation. I will see if I can reformat the courtesy link in a way I think you will prefer.

The "useful" info to the reader is the original publication, because that is what establishes the context of where and when the paper was published. That is one of the benefits of author-date referencing: the reader can see the year when each source was published, and use that to inform her opinion of the source. Citing the reprint instead of the original publication would be deceptive. Tarski could not possibly have published a paper in 2007, because he died in 1983. So is somewhat discomforting to read a citation such as "(Tasrski 2007)". Similarly, the citation "(Aristotle 1992)" would make very little sense. — Carl (CBM · talk) 11:04, 1 July 2010 (UTC)

The issue you raise that citing a reprint is "deceptive" is odd. The citation says explicitly that it refers to a reprint, and provides the actual date, location and name of the symposium where the talk was presented. The "discomforting" citation (Tarski, 2007) was fixed up to read (Tarski, 1957) so that was not and need not be an issue. The clear explanation of your activities here is some aesthetic of your own that serves no purpose, and in fact makes finding and reading the source harder for the reader. Brews ohare (talk) 11:28, 1 July 2010 (UTC)

However, after all this unnecessary activity, the present cumbersome citation does again include the Reprint, thank you. I hope a reader will be able to understand that the link to "Reprint" actually is the full text of the article in question. That is by no means obvious. Brews ohare (talk) 11:33, 1 July 2010 (UTC)

Citing a 1957 paper would be utterly unacceptable because there is no 1957 paper. There is a 1959 paper that was reprinted. The purpose of the reference is not particularly to help the reader locate a reprint. In a printed paper, there would be no reason to cite the reprint at all; it's a luxury that we have here. Moreover, according to worldcat.org, the original is available in over 300 libraries. So it isn't exactly hard to find.

But that misses the point: we should cite the original publication even if it isn't particularly easy to find. As WP:SCG says, "Where possible, Wikipedia should strive to provide the original reference for any discovery, breakthrough, or novel theoretical development, both for attribution and historical completeness: ...". One role of a reference work such as an encyclopedia is to present the historical record of a field. It is not actually budensome for a reader to go to the library or request a book or paper through their document delivery service. — Carl (CBM · talk) 11:44, 1 July 2010 (UTC)

Carl: You are inventing and critiquing a nonexistent situation: the reference is to a talk and if the time and location of the presentation is clearly stated there is absolutely no distortion or curtailment of historical fact, nor difficulty in finding the text of the talk when the Reprint is clearly identified and the full text linked and available for on-line viewing. You haven't got a leg to stand on. And if you think traveling 500 miles from Reno to a library in Las Vegas isn't burdensome compared to clicking a link on my PC, that's indicative of a strange mind set. Brews ohare (talk) 14:58, 1 July 2010 (UTC)

The reference is not to a talk; the talk itself is unpublished as far as I know. The reference is to the paper published in the proceedings of the conference. The convenience of clicking a link is not at all a factor that would lead us to cite a reprint instead of the original, although a courtesy link to an online reprint (or preprint) is always welcome in addition. — Carl (CBM · talk) 15:04, 1 July 2010 (UTC)

Indeed. The idea of referencing a talk directly is quite odd, and I'm pretty sure it would violate our WP:RS guidelines, as only people present in the audience at the conference can possibly know what Tarski said in his talk, it does not admit subsequent verification. The source actually used in this article is not the talk itself, but Tarski's paper in the conference proceedings, and that was published in 1959. As Carl formatted it, this is a perfectly standard way to cite a paper in proceedings.—Emil J. 10:24, 2 July 2010 (UTC)

Possibilities

It might be good to show how an interesting result such as the Pythagorean theorem could be expressed (never mind proved) in Tarski's system. It seems as though we could do something like the following:

• Define scalar addition: $ab+cd\equiv ef:=\exists xyz(Bxyz\land ab\equiv xy\land cd\equiv yz\land ef\equiv xz)$
• Define congruence of triangles: $\triangle abc\equiv \triangle def:=ab\equiv de\land bc\equiv ef\land ca\equiv fd$
• Define "strict" in-betweenness: $Sabc:=Babc\land a\neq b\land b\neq c$
• Define congruence of angles: $\angle abc\equiv \angle def:=\exists wxyz(Sawb\land Sbxc\land Sdye\land Sezf\land \triangle wbx\equiv \triangle yez)$
• Then define a right angle: $Rabc:=\exists wxyz(Swxy\land \angle abc\equiv wxz\land \angle abc\equiv zxy)$
• Define similar triangles: $\triangle abc\sim \triangle def:=\angle abc\equiv \angle def\land \angle bca\equiv \angle efd$
• We can now define scalar multiplication, via the proportionality property of similar triangles: $ab.cd\equiv ef.gh:=\exists uvwxyz(\triangle uvw\sim \triangle xyz\land ab\equiv uv\land ef\equiv xy\land cd\equiv yz\land gh\equiv vw)$
• Then Pythagoras can be expressed as: $Rabc\rightarrow \forall ij(i\neq j\rightarrow \exists uvwxyz(ab.ab\equiv uv.ij\land bc.bc\equiv wx.ij\land ac.ac\equiv yz.ij\land uv+wx\equiv yz))$ (here $ij$ is being used as the "unit").

Anyway, this is just me speculating. It would be great to have input from someone who actually knows authoritative answers to these questions :) Then maybe we could add relevant sections to the article. Cheers. Grover cleveland (talk) 19:50, 10 December 2011 (UTC)

I think most of those definitions (or ones along those lines) are in the Schwabhäuser and Szmielew book which we cite. I haven't read that work, however, but have spent much time with one which claims to be based on it: Julien Narboux (2007), "Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156. This material is also worked out at [1] and following pages on wikiproofs.org. As for how much of it to include in the wikipedia article, I don't know. As your example shows, even stating a familiar result without proof takes a fair number of definitions, some of which are not really obvious (for example, your definition of congruent triangles allows for degenerate triangles, in which the points are collinear or in which two or three of the points are equal, but your definition of similar triangles does not allow the second kind of degeneracy although I guess it allows the first). Kingdon (talk) 15:01, 17 December 2011 (UTC)

Julien Narboux: It is possible to prove the Pythagorean Theorem, it is actually in Chapter 15 of the Schwabhäuser and Szmielew book, which is cited. — Preceding unsigned comment added by 134.157.88.241 (talk) 09:50, 9 May 2014 (UTC)

There exists a proof of the sentence above that expresses the Pythagorean Theorem. Call this sentence ${\mathsf {PT}}$. As Tarski’s theory is known to be complete, either ${\mathsf {PT}}$ is provable or $\neg {\mathsf {PT}}$ is provable. A model of the theory can be constructed in an obvious manner using $\mathbb {R} ^{2}$ with its standard metric, and as ${\mathsf {PT}}$ is satisfied in this model, it follows that ${\mathsf {PT}}$ is provable. In fact, any sentence expressed in the language of the theory that is satisfied in this model is provable. Leonard Huang (talk) 07:21, 15 October 2017 (UTC)

Completeness vs. arithmetic

I am a non-mathematician with a reasonably good undergraduate math education. I'd really like the article to reconcile the completeness of Tarski's axioms with the fact that you can do arithmetic by constructing line segments of lengths a+b and ab given lengths a and b. I mean, I get that it must have to do with the "not requiring set theory" limitation, but I need the connection spelled out, and I'm guessing there are other readers in the same boat. A related point is that it'd be nice if the article listed familiar theorems that are and aren't provable in this system (in English, I mean, not in formal notation -- I read the section above about the Pythagorean Theorem). Or, if for some reason this doesn't belong in the article, at least please explain it to me! :-) Thanks. Briankharvey (talk) 23:01, 5 July 2013 (UTC)

@Briankharvey: You can do arithmetic of line segments in Tarski's system, and that way you'll get a field, in fact a real-closed field. But you cannot do arithmetic of natural numbers in Tarski's system. There's no way to define integers in his first-order language. And Gödel's incompleteness results only apply to systems in which you can do natural-number arithmetic. So there is no contradiction.

I added a few theorems that can be proven in Tarski's system (essentially Euclid's Book I). The Archimedean property is an example of a theorem that cannot be proven in Tarski's system, again because it refers to natural numbers. AxelBoldt (talk) 00:21, 13 December 2023 (UTC)

Wrong definition of "dense"

In Tarski's_axioms#Discussion, it says "a dense universe of points", but the word "dense" links to Density, the physical concept. What does "dense" mean in this context? Of the items on Density (disambiguation), the most relevant-looking one is Dense-in-itself, but I don't actually know. Thanks if anyone can clarify. :) --DavePercy (talk) 01:48, 11 January 2015 (UTC)

It should be Dense_set. I'll fix it. I can't find it in the text. Briankharvey (talk) 23:47, 17 December 2023 (UTC)

axiom schame of continuity

The definiotion is wrong. Let's take the model $\mathbb {R} ^{2}$ and let the formula $\phi (x)$ such that $\{x:\phi (x)\}=\{(x,0):|x|<1\}$, and the formula $\psi$ such that $\{y:\psi (y)\}=\{(y,0):|y|>1\}$. then exist $a=(0,0)$ such that if $\phi (x)\land \psi (y)$, then $Baxy$, so from axiom of continuity there must be $b$ such that $\forall x\forall y(\phi (x)\land \psi (y)\Rightarrow Bxby)$, but I can't think about something that will do it. בנציון יעבץ (talk) 10:20, 23 July 2021 (UTC)

When $a=(0,0)$ and $x=(1/2,0)$ and $y=(-2,0)$, one has $\phi (x)\land \psi (y)$ but not $Baxy$. JumpDiscont (talk) 00:51, 9 September 2021 (UTC)

Constructibility

This article is a bit confusing because it doesn't give examples or a description of first-order sentences in Tarski's language. I believe ancient Greek geometry had the theorem that there is a classical construction of the regular pentagon, but the regular 17-gon had to wait til Gauss. Today we usually prove these propositions with Galois theory. I had wondered whether they could also be handled by Tarski's decision procedure, and my suspicion is that they can't be written as first-order sentences for that procedure to handle.

You are right: the predicate "point p can be constructed from points a and b using straightedge and compass" cannot be expressed as a first-order formula in Tarski's system, basically because you would have to quantify over the number n of steps in this construction, and Tarski's system doesn't have natural numbers. AxelBoldt (talk) 00:39, 13 December 2023 (UTC)

Otherwise, can neusis constructions be decided the same way, by embedding in real closed fields? The neusis constructability of the regular 11-gon was an open problem til 2014 when Eliot and Schneider gave a construction, and the 25-gon and a few others are still open. So it would be interesting if these problems were solvable by a known decision procedure, that was maybe computationally intractable because of the complexity of quantifier elimination. arXiv:1712.07474's abstract makes me think it may be undecideable, but I haven't read the paper yet. 24.130.116.119 (talk) 02:42, 23 May 2023 (UTC)