Using his diagram-checker for E, Ben Northrop has determined that our third Pasch rules follows from the other diagrammatic rules. Details can be found in his MS thesis. There is a link to the thesis on the "Students" part of Avigad's web page.
Marcos Cramer and Richard Schüller have pointed out that our first superposition rule is not sufficient prove Euclid's Proposition 4. What we really need is a single rule combining the force of the two. In other words, take the set Pi to be {a' = d, angle a'b'c' = angle abc, ab = a'b', bc = b'c', ca = c'a', on(b',L), not between(b',d,g), same-side(c',h,L)} in the statement of the rule.
Moreover, we should have made it clear that in the superposition rule, the elements a', b', c' should be fresh variables, which is to say, they should not occur in Gamma, Delta, or Delta' (or, perhaps, better: one should restrict the conclusion to a subset Delta'' of Detla' which has this property). In other words, the rule should obey something like the "eigenvariable condition" on the elimination rule for the existential quantifier in natural deduction.
Rob Arthan has pointed out that in Section 4.5 the diagram to Proposition I.12, while not incorrect, is misleading: the point q need not lie on the line pd. (But see the discussion in Section 7.3 regarding misleading diagrams!)
On page 732, we say that, in contrast to Tarski's and Hilbert's axiomatizations of geometry, we use a strict version of betweenness. In fact, Hilbert used strict betweenness as well. We are grateful to Michael Beeson for pointing this out.
Alberto Marcone and Beatrice Anzil have pointed out that there is an error in our translation of the negation of the intersection of two circles on page 750 of our paper. The difficulty is that if two circles can fail to intersect in two distinct ways: they can be separated by a line, or one can be inside the other. It takes some effort to express this without having to introduce a disjunction. But it seems that this can be done; we sketch a solution below.
Define separation to be the following four place order relation of points on a line: two points x and y separate z and w iff either z or w lie between x and y but not both.
Suppose the line joining the centers of two circles alpha and beta intersects alpha in the points a, a' and intersects beta in points b, b'. Then a necessary and sufficient condition for the intersection of alpha and beta is that a and a' separate b and b'.
So if we can formulate a sentence in Tarski's theory that expresses that a and a' do not separate b and b', then we have formulated a sentence that expresses the non-intersection of the two circles. The trick, of course, is to formulate the sentence so that it has the right logical form --i.e. a sentence that asserts a conjunction of primitive relationships of a,a', b, b' with other points asserted to exist.
A way to do this is to assert with the sentence the existence of a (very complicated) configuration that implies that there is a projective transformation between points a, a', b, b' to collinear points x,y, z and w such that B(xyz) and B(yzw). Separation is an invariant in projective geometry, and x and y do not separate z and w by stipulation. So such a sentence would express that a and a' do not separate b and b'.
Any projective transformation between two lines can be understood as the composition of three perspectivities. A perspectivity between lines L and M is a mapping defined by a point p off of L and M such that q on L maps to r on M if the line joining p and q intersects M in r. Since the notion only uses the notions of points, lines and incidence, and these are expressible in Tarski's system in the right way, we can formulate a sentence that expressses that there is a perspectivity mapping one set of points on one line to another set of points on another line in the right way. The particular sentence we want, then, would assert that there are three perspectivities between a, a', b, b' and x,y,z,w such that B(xyz) and B(yzw).
That this sentence works follows from some facts about separation and projective transformations. We need to show that a and a' do not separate b and b' iff there is a composition of three perspectivities mapping a, a', b, b' to x,y,z,w such that B(xyz) and B(yzw). If a and a' do not separate b and b', then there are three cases. i) the pair a, a' does not lie inside the interval (b, b') and the pair b, b' does not lie inside the interval (a,a') ii) the pair a, a' lies inside (b,b') iii) the pair b, b' lies inside (a,a'). In the first case, we can just choose x,y, z and w to be a,a', b, and b'. The three perspectivies would just be the identity (L=M). To argue that in ii) and iii) the desired three perspectivities exist, we need to invoke the fact that any three points on a line can be mapped to any other three points on another line via a projective transformation. Given x,y,w such that B(xyw) there is thus a projective transformation T mapping a to x, a' to y, and b or b' to w. By choosing which of b or b' is mapped by T to w appropriately, we can force the image z of the remaining point (b' or b) to lie between y and w. T is the composition of three projectivities, so we are done. (That there are no points of infinity in models of Tarksi's elementary geometry does not matter. There is enough freedom in choice of points x,y,w and the perspectivities to avoid points at infinity in the perspectivities.)
Now if a and a' do separate b and b', then there can be no projective transformation between a, a, b, b' and x,y,z,w such that B(xyz) and B(yzw) because separation is a projective invariant. There are thus no three perspectivies whose composition is such a transformation.