Independence questions in set.mm (partial independence of ax-11 and ax-13)

82 views
Skip to first unread message

Benoit

unread,
Feb 22, 2022, 3:58:00 PMFeb 22
to Metamath

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

Thierry Arnoux

unread,
Feb 27, 2022, 11:47:23 AMFeb 27
to meta...@googlegroups.com, Benoit

Hi Benoît,

That's a very interesting paper!

I mentioned it in an answer on "proofassistants.stackexchange", maybe that counts as your first citation ;-)

Do you have plans to publish it?

BR,
_
Thierry

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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5ed340b6-22d7-4e13-8406-503121cff958n%40googlegroups.com.

David A. Wheeler

unread,
Feb 27, 2022, 8:12:15 PMFeb 27
to Metamath Mailing List


> On Feb 22, 2022, at 3:58 PM, Benoit <benoit...@gmail.com> 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).

I just briefly skimmed it & it's really interesting! Thanks for writing it!

I think we should modify some set.mm comments to specifically cite this work.
At the least, modifying some of the axiom statements (like ax-11) to note that they've
been proven (partially) independent & then citing this paper makes sense.
Benoit: If you have suggestions, or even better pull requests, that'd be great.

A nit: in the introduction we see "classical classical" in:
> In this article, “first-order logic” means classical classical1 one-sorted first-order logic with equality and no terms.
But that's a trivial text error & doesn't take away the quality of the result.

--- David A. Wheeler

Mario Carneiro

unread,
Feb 27, 2022, 9:51:26 PMFeb 27
to metamath
The "classical classical" is deliberate, as explained in the footnote.

--
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 metamath+u...@googlegroups.com.

David A. Wheeler

unread,
Feb 28, 2022, 9:53:03 AMFeb 28
to Metamath Mailing List


> On Feb 27, 2022, at 9:51 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> The "classical classical" is deliberate, as explained in the footnote.

Ah! Got it! Serves me right for just skimming :-).

--- David A. Wheeler

Benoit

unread,
Feb 28, 2022, 5:06:44 PMFeb 28
to Metamath
Thanks Thierry and David.  I will probably submit it for publication, though I have not decided on the journal yet.

David: yes, some comments in set.mm and on mmset.html or award2003.html will have to be updated.  I will propose something soon.  On a related note, after exchanging on my paper,  Norm made a few changes in set.mm last August and adopted the phrase "scheme completeness" instead of "metalogical completeness" (only a cosmetic change, but a nice mark of appreciation from him).

Benoît
Reply all
Reply to author
Forward
0 new messages