Is it possible to prove that a disk is convex using only Tarski's axioms of geometry?
Specifically, I'm looking for a proof of:
$\forall a\,\forall b\,\forall c\,\forall d\,\forall e\,[ ab \equiv ac \land Badc \land Bbed \implies \exists f\,(ab \equiv af \land Baef)]$
Visually, this corresponds to the statement that $e$ lies within the disk.
I've been looking at the axioms listed on Wikipedia, but I haven't figured out which of them implies that a disk is convex. Existing proofs of this and related problems seem to be mostly done using a metric on $\mathbb{R}^2$, which isn't available to me.
Yes it is possible. Sorry I don't have time to explain the proof, but you can read it from our formal proofs. See the Lemma bet_inc2__incs in our formalization in Coq of foundations of geometry (https://github.com/GeoCoq/GeoCoq/blob/290642eff83097858f99084da9a149b021887473/Tarski_dev/Annexes/circles.v line 185) the main lemma used in this proof follows from results from chapter 5 of Mathematishe Methoden in der Geometrie. ( formalized in Coq here: https://github.com/GeoCoq/GeoCoq/blob/290642eff83097858f99084da9a149b021887473/Tarski_dev/Ch05_bet_le.v ).