From 6ace865857fb0fafacb9441b06f9bfa7037e1560 Mon Sep 17 00:00:00 2001 From: Wolf Lammen Date: Sun, 21 Jan 2024 23:22:43 +0100 Subject: [PATCH] typos --- set.mm | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/set.mm b/set.mm index c42eea0d4..d593430be 100644 --- a/set.mm +++ b/set.mm @@ -15574,10 +15574,10 @@ only postulated (that is, axiomatic) rule of inference of predicate 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, + exactly meeting our intuition. Every universally quantified wff is provably + true, and every existentially quantified wff 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 , + quantified wff 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 . $) @@ -15587,13 +15587,13 @@ only postulated (that is, axiomatic) rule of inference of predicate 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. + $( In an empty logical 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