How to implement projective geometry in MMA? - Mathematica Stack Exchange most recent 30 from mathematica.stackexchange.com 2019-10-16T18:36:34Z https://mathematica.stackexchange.com/feeds/question/189208 https://creativecommons.org/licenses/by-sa/4.0/rdf https://mathematica.stackexchange.com/q/189208 3 How to implement projective geometry in MMA? user64494 https://mathematica.stackexchange.com/users/7152 2019-01-10T14:31:39Z 2019-01-10T14:52:31Z <p>I'd like to implement 2D projective geometry in Mathematica, making use of the <code>FindEquationalProof</code> command. Up to <a href="https://ru.wikipedia.org/wiki/%D0%9F%D1%80%D0%BE%D0%B5%D0%BA%D1%82%D0%B8%D0%B2%D0%BD%D0%B0%D1%8F_%D0%BF%D0%BB%D0%BE%D1%81%D0%BA%D0%BE%D1%81%D1%82%D1%8C" rel="nofollow noreferrer">Wiki ru.wikipedia.org</a> (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.</p> <p>P1. Through two different points P and Q of the plane P passes a straight line, and only one.</p> <p>P2. Any two lines have a common point.</p> <p>P3. There are three points not lying on one straight line.</p> <p>P4. Each line contains at least three points.</p> <p>Additional axioms are the following:</p> <p>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.</p> <p>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.</p> <p>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.</p> <p>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.</p> <pre><code>axioms={ForAll[{p,q} ∈ points,p!= q,Exists[m ∈ lines, el[p,m]&amp;&amp;el[q,m]]], ForAll[{m,k} ∈ lines,Exists[ p ∈ points,el[p,m]&amp;&amp;el[p,k]]], Exists[{p,q,r} ∈ points, ForAll[k ∈ lines, Not[el[p,k]]||Not[el[q,k]]||Not[el[r,k]]]],...} </code></pre> <p>I stop at axiom P3 because of</p> <pre><code>Exists[{p, q, r} ∈ points,ForAll[k ∈ lines, Not[el[p, k]] || Not[el[q, k]] || Not[el[r, k]]]] </code></pre> <blockquote> <p>Exists::ivar: {p,q,r}∈points is not a valid variable.</p> </blockquote> <p>Constructive criticism is welcome.</p>