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

82 views

### Benoit

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.

Best regards,
Benoît

### Thierry Arnoux

Feb 27, 2022, 11:47:23 AMFeb 27

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.

### David A. Wheeler

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

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

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