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.
