Using Tarski's axioms or Hilbert's axioms, Euclidean geometry can be described synthetically (in a way that can even be formalized in Coq), i.e. within a theory of first-order logic, or second-order logic if we take an axiom of continuity. I was wondering whether the geometry of conic sections, as studied by Appolonius of Perga for example, can be formulated axiomatically.
Are Tarki's axioms/Hilbert's axioms sufficient to deal with conics/quadrics? If not, what needs to be added? If anyone has any useful reference in mind about the axiomatisation of conic sections, I would also be grateful.
This question is certainly linked to this one, but I have not been able to find a list of axioms that could encompass the geometry of conics systematically (or a reason explaining why the current axiomatisations of Euclidean geometry are enough).
Using coordinates, pretty much everything in the classical theory of conics can be expressed easily in the first-order theory of the ordered field $\mathbb{R}$: a conic is just the set of ordered pairs $(x,y)\in\mathbb{R}^2$ that satisfy some degree $2$ polynomial equation (and such degree $2$ polynomial equations can themselves be described using finite tuples of real numbers, namely their coefficients). If you fix a pair of oriented perpendicular lines to serve as axes and a unit distance, then Tarski's axioms become bi-interpretable with the complete first-order theory of $\mathbb{R}$ as an ordered field. So, everything about conics can be done using Tarski's axioms.
(OK, not literally everything about conics; there are some non-first order statements about conics. For instance, Tarski's axioms can't talk about the circumference or area of an ellipse since those can only be defined by some limiting process. So, Tarski's axioms can probably do everything that Appolonius did with conics, but not everything that Archimedes did. But there are more basic statements in ordinary Euclidean geometry using only lines that are not first order in a similar way. For instance, Tarski's axioms can't state any general theorems about polygons with arbitrary numbers of sides; they can only state theorems about $n$-gons for fixed values of $n$.)