Hi Benoît, That's a very interesting paper!
I mentioned it in an answer on "proofassistants.stackexchange" <https://proofassistants.stackexchange.com/questions/801/what-is-known-about-minimal-sets-of-axioms#comment1570_811>, maybe that counts as your first citation ;-) Do you have plans to publish it? BR, _ Thierry On 23/02/2022 04:58, Benoit wrote:
Hi everyone, I uploaded yesterday a preprint to the arXiv titled "Independence questions in a finite axiom-schematization of first-order logic" (https://arxiv.org/abs/2202.10383). Although the axiomatization studied in that paper differs slightly from that of set.mm, when applied to the set.mm axiomatization of first-order logic, setmm := {ax-mp, ax-gen, ax-1 to ax-13}, it proves: - independence of ax-11 in setmm \ {ax-12, ax-13}, - independence of ax-13 in setmm \ {ax-12}, and adapts classical results to prove: - independence of ax-mp, ax-gen, ax-1 to ax-9, ax-12 in setmm, - independence of ax-10 in setmm \ {ax-5, ax-12}. There are a few other results, and also an introductory section presenting the formal systems used, which may be useful as a companion introduction to Metamath for set.mm-like databases (its content will not be new to regular contributors of this mailing list). The main new ingredient to prove partial independence of ax-11 and ax-13, which I called supertruth and discovered in August 2020, modifies the set of instances that a given scheme may have, hence can prove independence of schemes which are redundant at the object-level (see the paper for the definition). I rapidly let Norm and Mario know about this, and that discovery slowly extended, thanks to their comments and over a bit more than a year, to the present paper, of which Norm knew the almost-final form. The paper is dedicated to his memory. I also extend my thanks here to Mario, whose comments were very useful. I also mention Wolf in the acknlowledgments, since his work on reducing axiom dependencies was also useful to clear things up. Of course, your comments are welcome. Best regards, Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5ed340b6-22d7-4e13-8406-503121cff958n%40googlegroups.com <https://groups.google.com/d/msgid/metamath/5ed340b6-22d7-4e13-8406-503121cff958n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fd98e68f-6df8-317e-b0e2-f764808c49f0%40gmx.net.
