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

[Benoit]

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]

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]

> 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]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2D0AB54B-942F-4ECD-907D-0E6439EC654D%40dwheeler.com.

[David A. Wheeler]

> 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]

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