empty domain

[wlammen]

Gérard Lang suggested in a private mail adding a small extension at the end of paragraph ax-4 describing simple properties of the empty logical domain. See the comment at the beginning of this PR completely written by him. For minimal results he suggested to move wl-(nax6im, nax6al, nax6fr) from my mathbox to main, extended by nax6ex, which I provided here with a quick proof.

In set theory the logical empty domain cannot play a significant role, since you need objects serving as sets. So I was not really in support of adding this niche to set.mm. But this is the second request in this direction, following an idea of @benjub , if I remember right, so lets give it a chance here. This is meant as a draft for discussion. Once it is accepted and has matured, changes-set.txt needs to be updated for theorems moved from mathboxes. This is not done in this draft.

[benjub]

• Possibly, the statements labeled in this proposal nax6ex, nax6al, and nax6nf could have an interest (and maybe one could add ... -> -. E! x ph and ... -> E* x ph), but not nax6im.
• Having a subsection dedicated to them may not be necessary.
• Comments would have to be rewritten.

[benjub]

A proposal:

$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
  The empty domain of discourse
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-

  This database develops mathematics from first-order logic, which has only
  nonempty models.  Before stating axioms excluding the empty model
  (typically, ~ ax-6 in logic and ~ ax-nul in set theory), we state in this
  short subsection a few results relative to the empty domain, which we
  characterize by the assumption ` -. E. x T. ` .  As expected, on the empty
  domain, every universally quantified formula is true ( ~ emptyal ) and every
  existential formula is false (~ emptyex ), and every variable is effectively
  nonfree in any formula ( ~ emptynf ).

$)

  $( Two characterizations of the empty domain. $)
  empty $p |- ( -. E. x T. <-> A. x F. ) $=
    ? $.

  $( On the empty domain, any existentially quantified formula is false.
     (Contributed by Wolf Lammen, 21-Jan-2024.) $)
  emptyex $p |- ( -. E. x T. -> -. E. x ph ) $=
    ( wex wtru trud eximi con3i ) ABCDBCADBAEFG $.

  $( On the empty domain, any universally quantified formula is true.
    (Contributed by Wolf Lammen, 12-Mar-2023.) $)
  emptyal $p |- ( -. E. x T. -> A. x ph ) $=
    ( wtru wex wn wal nax6ex alex sylibr ) CBDEAEZBDEABFJBGABHI $.

  $( On the empty domain, any variable is effectively nonfree in any formula.
     (Contributed by Wolf Lammen, 12-Mar-2023.) $)
  emptynf $p |- ( -. E. x T. -> F/ x ph ) $=
    ( wtru wex wn wal wnf nax6al nftht syl ) CBDEABFABGABHABIJ $.

[wlammen]

Thanks for your suggestion. I informed Gerard Lang, and he approves this change.

[wlammen]

If you want to prove ¬ ∃𝑥⊤ → ¬ ∃𝑦 ⊤, i.e. the independence of the quantified variable, you need ax-5.

[benjub]

If you want to prove ¬ ∃𝑥⊤ → ¬ ∃𝑦 ⊤, i.e. the independence of the quantified variable, you need ax-5.

Indeed. Since ax-5 holds on the empty domain, this could be done. Do you think we should link from that new section to https://us.metamath.org/mpeuni/bj-cbval.html ?

[benjub]

Thanks @wlammen

[wlammen]

Indeed. Since ax-5 holds on the empty domain, this could be done. Do you think we should link from that new section to https://us.metamath.org/mpeuni/bj-cbval.html ?
In case of the empty domain the proof is very simple: ∃𝑦⊤→⊤(trud) and ⊤→ ∃𝑥⊤ (ax5e) from which
¬ ∃𝑥⊤ → ¬ ∃𝑦 ⊤follows. If you want this result be part of the empty domain section, one should rather let it end the section ax-5 than that of ax-4

[benjub]

In case of the empty domain the proof is very simple: ∃𝑦⊤→⊤(trud) and ⊤→ ∃𝑥⊤ (ax5e)

This is not an instance of ax5e (which is |- ( E. x ph -> ph ) , DV(x, ph)). Furthermore, ⊤→ ∃𝑥⊤ is not true on the empty domain.

[wlammen]

This is not an instance of ax5e... Yes. I should not post while busy with daily tasks.

Then of course, linking to bj-cbvalimi should be done. Or adapting it with ph, ps, ch set to F.? I'll have a closer look later.

EDIT: The problem with bj-cbval is that it needs an expression A. y E. x ph with some constant expression ph. At the point of ax-4 we only have T. and F. available for this constant. x = y is possible, too, as a syntactic correct expression, but without any semantics yet (could actually mean x =/= y).

[benjub]

Yes, bj-cbval is a bit different, so maybe we can link to it. For now, we can merge this MR as is IMO.