Derive Axioms??

Stream: Equational

[Shreyas Srinivas]

When going through docs compilation in CI I got a step that gave me anxiety for a moment:
https://github.com/teorth/equational_theories/actions/runs/11277909576/job/31365188769?pr=421#step:8:1270

[Shreyas Srinivas]

It seems there is a function in the Compactness file that is called deriveAxioms which is thankfully not creating any new axioms

[Shreyas Srinivas]

But is this a good naming choice in a formalisation project?

[Mario Carneiro]

I don't think it's that strange to refer to the 'axioms' of a group or similar structure as axioms

[Shreyas Srinivas]

I am aware of how algebra folks use it, and "axioms" is a reasonably common term in logic and model theory. Ofc in lean there is an extra connotation (in the sense that we really like it when our proofs don't depend on any axioms other than choice, quot_ext, and the third one I can't remember)

[Martin Dvořák]

I'm on the team "don't use the word «axiom» for anything else than the Lean axioms".
FYI, the "good" axioms are [propext, Classical.choice, Quot.sound].

[Martin Dvořák]

PS: I am aware that it is a controversial take.
Also a discussion I had last year on Facebook showed that:
https://www.facebook.com/dvorakMFF/posts/pfbid02cSEB9vP3FQTYWkUTfrCcrurcHUqNTyLjV76dB1ZfbpgLHxNnd4LwyV3c3D8mgrvrl

[Terence Tao]

So if we rename Axioms to Hypotheses in Compactness.lean then there should be no confusion? From what I understand, the functions and definitions using Axioms here are only used to establish the compactness theorem, and are not used externally to this file.

[Shreyas Srinivas]

Yeah I have no doubts about the content. Hypothesis sounds good. I am fine with any word really. The word axiom struck me as odd as a lean user, but it is the standard model theory term as far as I know.

[Cody Roux]

Sure, rename at will (this is the cost of doing metatheory, it sometimes gets confused with object theory)