Axiomatic projective geometry

Stream: new members

[Stepan Holub]

Hello.

Here in Prague we start a new seminar on axiomatization of projective geometry (roughly along axioms by Veblen and Young , 1910 and 1917). I have quite extensive experience with Isabelle but in this seminar we are toying with the idea to formalize the axiomatic system in Lean where we are all complete beginners. The ultimate goal is to show that the theory is complete and decidable, but the formalization would be interesting even without that.
Is there anything similar in Lean already? Both in the field of projective geometry, but also in the logical direction of showing any theory to be complete and/or decidable? I am superficially aware of a related work in Coq (GeoCoq), and I also found in the chat that in 2019 there were some plans to work on projective geometry.

Any comment or suggestion will be appreciated.

Stepan

[Anthony Bordg]

@Stepan Holub
If you're familiar with Isabelle but not with Coq, you could have a look at the entry Projective Geometry in the AFP and import it in Lean, possibly with some modifications depending on your goals. This formalisation was itself adapted from a similar formalisation in Coq.

[Yaël Dillies]

Let me cc @Bhavik Mehta who has been recently working on getting some of the results of the Coq paper on PG(3, 2) by Magaud (https://dpt-info.di.unistra.fr/~magaud/talk-itp2022-magaud.pdf) without bash.

[Bhavik Mehta]

I also converted a lot of GeoCoq into Lean, but mostly focusing on the geometric results rather than logical facts

[Ruben Van de Velde]

Better to focus on the illogical facts?

[Adam Topaz]

I had a student over the summer develop some projective geometry in mathlib, but focusing only on projective spaces associated to vector spaces over fields, not the axiomatic approach. He has a branch somewhere which gives the necessary tools one needs to prove the axioms of an abstract projective geometry for such projective spaces (among many other things). Our plan was to advance toward the fundamental theorem of projective geometry.

I’ll try to look around and post some links to this stuff later today.

[Junyan Xu]

I'm not sure whether these axioms are what you have in mind, because they don't seem to be complete in the normal model theoretic sense docs#first_order.language.Theory.is_complete, because there are finite models of different cardinalities.

Since this is a finite axiomatization, completeness (in the normal sense) trivially implies decidability. Maybe by completeness you mean it only has the intended models, i.e. projective spaces over division rings?

[Stepan Holub]

@Anthony Bordg
Anthony, your AFP entry will certainly be useful. Thanks.

[Stepan Holub]

@Junyan Xu
Specifically, I meant the theory of real projective plane being complete. (Yes, complete implies decidable here. The stress on decidable is unnecessary but motivated by interest in efficient decision procedures.)