empty domain

set.mm

@@ -15564,6 +15564,42 @@ only postulated (that is, axiomatic) rule of inference of predicate
   $}
 
 
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  The empty logical domain
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+
+  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.  (Contributed by Gerard Lang,
+     5-Feb-2024.) $)
+  empty $p |- ( -. E. x T. <-> A. x F. ) $=
+    ( wfal wal wtru wn wex df-fal albii alnex bitr2i ) BACDEZACDAFEBKAGHDAIJ $.
+
+  $( 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 emptyex 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 emptyal nftht syl ) CBDEABFABGABHABIJ $.
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Axiom scheme ax-5 (Distinctness) - first use of $d
@@ -541306,31 +541342,12 @@ extends this idea to multiple additions (TODO).
        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.) $)
+       empty logical 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 ) $=