Michael Beeson's Research

Tarski Formalization Project Archives

Chapter 9: Sides of a line, and outer Pasch from inner Pasch.

There are two major results in this chapter: the opposite-sides theorem (related to the idea that a line divides a plane into two regions), and the fact that inner Pasch implies outer Pasch. Both these results, like the main results of Chapters 7 and 8, are due to Gupta (1965).

Hilbert and Tarski agree that "p and q are on the opposite side of Line(a,b)" means that there is a point on the line strictly between p and q.

Tarski defined "p and q are on the same side of line L" to mean that there is some point c such that both segments pc and qc meet line L, and none of p,q,c lie on L. Hilbert just said it meant that pq does not meet L. Tarski's definition has the advantage of working in n-space. It also allows "plane" to be a defined concept: Three non-collinear points a,b,c determine the plane consisting of all points that are on the same side of Line(a,b) as c, or on the opposite side. But then, are the points on same side as c all on the opposite side from any one point on the opposite side? Yes, they are, according to Satz 9.8, and moreover, being on the same side of a given line is a transitive relation (Satz 9.13).

These results assert the existence of certain intersection points of lines, and hence they are intimately bound up with Pasch's axiom, which is the fundamental principle that a line entering a triangle (in the same plane as the triangle) must also exit the triangle. There are two forms of Pasch's axiom that are considered in Tarski's geometry: inner Pasch, and outer Pasch. (See my paper "A constructive version of Tarski's geometry" for diagrams.)

Both are good choices for an axiom, since their logical form is simple and they do not rely on an upper dimension axiom to be true, i.e. they are true in n-space as well as in the plane. Tarski originally took outer Pasch as an axiom, since it was known that outer Pasch implies inner Pasch. Gupta showed that inner Pasch implies outer Pasch, which is Satz 9.6. After that, Szmielew took inner Pasch as an axiom (as is done in SST), although Tarski argued in a famous letter that the development might be easier with outer Pasch as an axiom.

The theorem that inner Pasch implies outer Pasch rests on the opposite-side theorem Satz 9.5; its fairly short proof uses nothing else from Chapters 7,8, or 9. Once both forms of Pasch are available, the derivation of the properties of "sameside" is not difficult.

The opposite-side theorem (Satz 9.5) rests on what SST calls Lemma 9.4. That "Lemma" gave Otter a lot of trouble, so much that we upgraded it from "Lemma" to "Satz". We had to break it into three cases and prove them separately, and then derive Satz 9.4 from the three separately-proved cases, and even that was not trivial.

The posted input files are now all mechanically generated from a master list of theorems.

The times shown in the following table are not the times required to find the proof, but rather the maximum time allocated to Otter to find the proof. The time is shown only when it had to be longer than the default, which was often 20 seconds when hints were used and 120 seconds when hints were not used.

For more information about our methodology see the top page of this project.

Input File	Proof	Length	Strategy	Seconds	Commentary
Satz9.2	Satz9.2.prf	10			If $a$ and $b<$ are on opposite sides of line $L$, then $b$ and $a$ are on opposite sides of $L$.
Satz9.3a	Satz9.3a.prf	25	subformula	46	The case of Satz 9.3 in which $T(r,b,a)$. We had to prove this separately, and then use it to prove Satz 9.3.
Satz9.3	Satz9.3.prf	50	hints		called Lemma 9.3 in the book, used for 9.4. If $b$ and $a$ are on opposite sides of line $L$, and the midpoint of $ac$ lies on line $L$, and $r$ is on $L$, and $b$ is a point on the ray from $r$ through $a$, then $b$ and $c$ are on opposite sides of $L$.
SideReflect	SideReflect.prf	26	subformula	49	$ sameside(a,b,c) \rightarrow sameside(s(m,a),s(m,b),s(m,c))$. This is used in the proof of Satz 9.4, but Szmielew fails to state or prove it.
Satz9.4a	Satz9.4a.prf	40	hints		Satz 9.4 (see below), with assumptions $r\neq s$ and $ac \le ra$, and conclusion $sameside(u,r,a) -> sameside(s(m,u),s,c)$
Satz9.4a2	Satz9.4a2.prf	35	hints		Satz 9.4 (see below), with assumptions $r\neq s$ and $ac \le ra $, and conclusion $sameside(s(m,u),s,c) -> sameside(u,r,a)$
Satz9.4b	Satz9.4b.prf	42	hints		Satz 9.4 assuming $r=s$.
Satz9.4	Satz9.4.prf	9		450	First part of Lemma 9.4 in the book (line 1 implies left-to-right of line 2), here derived from its cases 9.4a, 9.4a2, and 9.4b.
Satz9.4c	Satz9.4c.prf	41	hints		Second half of Lemma 9.4 in the book (line 1 implies line 3). Assumes $sameside(u,r,a)$ and $sameside(v,s,c)$, and concludes $opposite(u,p,q,v)$, where $p,q$ give the line called $A$ in the book.
Satz9.5	Satz9.5.prf	30	subformula	820	Opposite sides theorem: if $a$a and $ b$ are on the same side of point $r$ (i.e., on the same ray from $r$), and $a$ and $c$ are on opposite sides of line $L$, then $b$ and $c$ are on opposite sides of $L$.
Satz9.6	Satz9.6.prf	98	subformula	186	Inner Pasch implies outer Pasch (Gupta 1965), This was one of Quaife's challenge problems.
Satz9.8	Satz9.8.prf	63	subformula	1646	If $a$ and $c$ are on opposite sides of line $L$, and $a$ and $b$ are on the same side of $L$, then $b$ and $c$ are on opposite sides of $L$ .
Satz9.9	Satz9.9.prf	6		4000	If $a$ and $b$ are on opposite sides of line $L$, then $a$ and $b$ are not on the same side of $L$ .
Satz9.13	Satz9.13.prf	65	hints		$samesideline$ is a transitive relation.
Satz9.16	Satz9.16.prf	14			If $a$ and $b$ are on the same side of $Line(p,q)$, and $a$ and $r$ are on the same ray emanating from $q$, then $r$ and $b$ are on the same side of $Line(p,q)$. This theorem is not in the book, but we needed it for Satz 11.15b. (The number 9.16 is used for a remark in the book.)
Satz9.19b	Satz9.19b.prf	8			If $p$ is on line $L$, and $a$ and $b$ are on the same ray emanating from $p$ and $a$ is not on $L$, then $a$ and $b$ are on the same side of $L.$This is the right-to-left part of Satz 9.19.

Back to top of archive