Independence of statement from axioms in Lean

Stream: general

[Donald Sebastian Leung]

In the study of incidence geometry, the Euclidean parallel postulate is independent of the axioms of incidence geometry. Is there a way to state this directly in Lean (or in CoIC in general), or is it more of a metatheorem?

[Reid Barton]

probably the most succinct answer is to link to https://github.com/flypitch/flypitch/

[Johan Commelin]

I think you can. Just build an example where it holds and another one where it doesn't

[Donald Sebastian Leung]

Reid Barton said:

probably the most succinct answer is to link to https://github.com/flypitch/flypitch/

Awesome, I think I found the answer I wanted, thanks @Reid Barton !

[Reid Barton]

Johan's answer is the sensible mathematician's one, if you take for granted the existence of the syntax of formal logic, proof theory, model theory to the extent of having a soundness theorem which reduces the question to the existence of models of the other axioms which either satisfy or do not satisfy the parallel postulate.

[Reid Barton]

It is a matter of how you interpret the phrase "is independent of the axioms of" formally

[Reid Barton]

and in particular whether it is a statement about the syntax of proofs or the semantics of models

[Reid Barton]

Same way as if a mathematician asks "does commutativity follow from the axioms of a group", what they mean is probably "is every group commutative", not "in some (unspecified but) fixed formal system, does there exist a logical derivation which starts with the group axioms and deduces commutativity"