empty domain

set.mm

@@ -15564,6 +15564,69 @@ only postulated (that is, axiomatic) rule of inference of predicate
   $}
 
 
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  The empty logical domain
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+
+  The empty logical domain is certainly a limit case, that is in contradiction
+  with set theory because ~ ax-nul postulates the existence of at least one
+  set, ~ ax-pr postulates the existence of at least two sets, and finally
+  ~ ax-inf postulates the existence of an infinite number of sets. It is
+  nevertheless interesting to shortly develop this case because the results are
+  exactly meeting our intuition. Every universally quantified wwf is provably
+  true, and every existentially quantified wwf is provably false. Otherwise,
+  nothing can be said. Reciprocally, in the case that every universally
+  quantified wwf is true, then ~ ax-6 is negated, but ~ ax-gen , ~ ax-4 ,
+  ~ ax-5 , ~ ax-10 , ~ ax-11 , ~ ax-12 and ~ ax-13 are automatically true, and
+  so are also every universal quantification of ~ ax-7 , ~ ax-8 and ~ ax-9 .
+$)
+
+  ${
+    $d x y $.
+    nax6im.1 $e |- ( -. E. x x = y -> ph ) $.
+    $( The following series of theorems are centered around the empty domain,
+       where no set exists.  As a consequence, a set variable like ` x ` has no
+       instance to assign to.  An expression like ` x = y ` is not really
+       meaningful then.  What does it evaluate to, true or false?  In fact, the
+       grammar extension ~ weq requires us to formally assign a boolean value
+       to an equation, say always false, unless you want to give up on
+       ~ exmid , for example.  Whatever it is, we start out with the
+       contraposition of ~ ax-6 , that guarantees the existence of at least one
+       set.  Our hypothesis here expresses tentatively it might not hold.  We
+       can simplify the antecedent then, to the point where we do not need
+       equation any more.  This suggests what a decent characterization of the
+       empty logical domain could be.  (Contributed by Wolf Lammen,
+       12-Mar-2023.) $)
+    nax6im $p |- ( -. E. x T. -> ph ) $=
+      ( wtru wex weq trud eximi nsyl4 con1i ) AEBFZBCGZBFLAMEBMHIDJK $.
+  $}
+
+  $( In an empty logical domain existential quantification never holds, not
+     even for false expressions.  (Contributed by Wolf Lammen, 21-Jan-2024.) $)
+  nax6ex $p |- ( -. E. x T. -> -. E. x ph ) $=
+    ( wex wtru trud eximi con3i ) ABCDBCADBAEFG $.
+
+  $( In an empty domain the for-all operator always holds, even when applied to
+     a false expression.  This theorem actually shows that ~ ax-5 is provable
+     there.  Also we cannot assume that ~ sp generally holds, except of course
+     in the form of ~ sptruw .  Without the support of an ~ sp like theorem it
+     seems difficult, if not impossible, to arrive at a theorem allowing to
+     change the bounded variable in the antecedent.  Additional axioms need to
+     be postulated to further strengthen this result.
+
+     A consequence of this result is that ` E. x ph ` is not true for any
+     ` ph ` .  In particular, ` E* x ph ` does not hold either, a somewhat
+     counterintuitive result.  (Contributed by Wolf Lammen, 12-Mar-2023.) $)
+  nax6al $p |- ( -. E. x T. -> A. x ph ) $=
+    ( wtru wex wn wal nax6ex alex sylibr ) CBDEAEZBDEABFJBGABHI $.
+
+  $( All expressions are free of the variable used in the antecedent.
+     (Contributed by Wolf Lammen, 12-Mar-2023.) $)
+  nax6nfr $p |- ( -. E. x T. -> F/ x ph ) $=
+    ( wtru wex wn wal wnf nax6al nftht syl ) CBDEABFABGABHABIJ $.
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Axiom scheme ax-5 (Distinctness) - first use of $d
@@ -541292,45 +541355,6 @@ extends this idea to multiple additions (TODO).
       AEZCAFZGPABHAICAJOPAKLABMN $.
   $}
 
-  ${
-    $d x y $.
-    wl-nax6im.1 $e |- ( -. E. x x = y -> ph ) $.
-    $( The following series of theorems are centered around the empty domain,
-       where no set exists.  As a consequence, a set variable like ` x ` has no
-       instance to assign to.  An expression like ` x = y ` is not really
-       meaningful then.  What does it evaluate to, true or false?  In fact, the
-       grammar extension ~ weq requires us to formally assign a boolean value
-       to an equation, say always false, unless you want to give up on
-       ~ exmid , for example.  Whatever it is, we start out with the
-       contraposition of ~ ax-6 , that guarantees the existence of at least one
-       set.  Our hypothesis here expresses tentatively it might not hold.  We
-       can simplify the antecedent then, to the point where we do not need
-       equation any more.  This suggests what a decent characterization of the
-       empty domain could be.  (Contributed by Wolf Lammen, 12-Mar-2023.) $)
-    wl-nax6im $p |- ( -. E. x T. -> ph ) $=
-      ( wtru wex weq trud eximi nsyl4 con1i ) AEBFZBCGZBFLAMEBMHIDJK $.
-  $}
-
-  $( In an empty domain the for-all operator always holds, even when applied to
-     a false expression.  This theorem actually shows that ~ ax-5 is provable
-     there.  Also we cannot assume that ~ sp generally holds, except of course
-     in the form of ~ sptruw .  Without the support of an ~ sp like theorem it
-     seems difficult, if not impossible, to arrive at a theorem allowing to
-     change the bounded variable in the antecedent.  Additional axioms need to
-     be postulated to further strengthen this result.
-
-     A consequence of this result is that ` E. x ph ` is not true for any
-     ` ph ` .  In particular, ` E* x ph ` does not hold either, a somewhat
-     counterintuitive result.  (Contributed by Wolf Lammen, 12-Mar-2023.) $)
-  wl-nax6al $p |- ( -. E. x T. -> A. x ph ) $=
-    ( wtru wex wn wal trud eximi con3i alex sylibr ) CBDZEAEZBDZEABFNLMCBMGHIAB
-    JK $.
-
-  $( All expressions are free of the variable used in the antecedent.
-     (Contributed by Wolf Lammen, 12-Mar-2023.) $)
-  wl-nax6nfr $p |- ( -. E. x T. -> F/ x ph ) $=
-    ( wtru wex wn wal wnf wl-nax6al nftht syl ) CBDEABFABGABHABIJ $.
-
   $( This specialization of ~ hbae does not depend on ~ ax-11 .  (Contributed
      by Wolf Lammen, 8-Aug-2021.) $)
   wl-hbae1 $p |- ( A. x x = y -> A. y A. x x = y ) $=