# How to implement projective geometry in MMA?

I'd like to implement 2D projective geometry in Mathematica, making use of the FindEquationalProof command. Up to Wiki ru.wikipedia.org (This topic is better written in Russian edition than in English one.), the classical projective plane P is defined by the following axioms. The first four of these are required.

P1. Through two different points P and Q of the plane P passes a straight line, and only one.

P2. Any two lines have a common point.

P3. There are three points not lying on one straight line.

P4. Each line contains at least three points.

P5. Axiom of Desargues. If triangles ABC and A'B'C 'are such that straight lines AA', BB 'and CC' intersect at point O, then the intersection points of the pairs of corresponding sides AB and A'B '(P), BC and B'C' ( R), AC and A'C '(Q) lie on one straight line.

P6. Pappus Axiom. If l and l 'are two different lines, A, B, C are three different points on the line l, and A', B ', C' are three different points l ', and all these points are different from O - the points of intersection of lines l and l ', then the intersection points of the pairs of corresponding sides AB' and A'B (P), BC 'and B'C (R), AC' and A'C (Q) lie on the same line.

P7. Fano's axiom. Let A, B, C, D be points, no three of which lie on the same line. Let's draw all six straight lines connecting these points (AB, AC, AD, BC, BD, CD). Denote the intersection point of AB and CD by P, AC and BD by Q and AD and BC by R (diagonal points). These diagonal points do not lie on one straight line.

It is not so simple to formulate the above axioms in Wolfram language. There are two types of objects of projective plane: points and lines. There is a relation: a point belongs to a line. Here is my attempt.

axioms={ForAll[{p,q} ∈ points,p!= q,Exists[m ∈ lines, el[p,m]&&el[q,m]]],
ForAll[{m,k} ∈ lines,Exists[ p ∈ points,el[p,m]&&el[p,k]]],
Exists[{p,q,r} ∈ points, ForAll[k ∈ lines,
Not[el[p,k]]||Not[el[q,k]]||Not[el[r,k]]]],...}


I stop at axiom P3 because of

Exists[{p, q, r} ∈ points,ForAll[k ∈ lines,
Not[el[p, k]] || Not[el[q, k]] || Not[el[r, k]]]]


Exists::ivar: {p,q,r}∈points is not a valid variable.

Constructive criticism is welcome.

• Look at the documentation of Exists and Element: The proper syntax is Exists[{p, q, r}, (p|q|r) ∈ points, ...] – Lukas Lang Jan 10 at 15:35
• @Lucas Lang: Thank you. Unfortunately, the changed code produces another errorExists::msgs: Evaluation of {(p|q|r)[Element]points,\!(*SubscriptBox[([ForAll]), (k [Element] lines)](((! el[p, k]) || (! el[q, k]) || (! el[r, k]))))} generated message(s) {ForAll::ivar}. – user64494 Jan 10 at 15:45
• Look at the documentation of ForAll: your syntax wrong here as well – Lukas Lang Jan 10 at 16:53
• @Lucas Lang: Are you serious? I am waititing fog for a serious constructive answer. – user64494 Jan 10 at 19:21
• Sorry if I came across too harsh - the comment was intended to be constructive. Your syntax error is exactly the same for ForAll as it was for Exists. If you look at the documentation, you'll see that the syntax for both is ForAll[vars,conds,expr]. – Lukas Lang Jan 10 at 19:43