Indeed, nf2 is simpler, since it has no nested quantifiers (this is the main reason), and there are several natural definitions equivalent to it over propositional calculus only (see the previous thread here that I mentioned, and also ~wl-nf3 ~wl-nf4, ~wl-nf5), which argues for its greater naturality over df-nf.
Jim: in that previous thread, we had discussed the intuitionistic aspect of the changes, since not all proposed definitions are equivalent in intuitionistic logic, but as you noted, nf2 is. When df-nf and nf2 are not equivalent (that is, before the introduction of ax-10 and ax-12), which one better captures non-freeness ? An interesting viewpoint is to look at modal logic and Kripke semantics (wikipedia has a good page on it). In Kripke semantics, nf2 at some world expresses that if ph holds in some world accessible from it, then it holds in all worlds accessible from it, while df-nf at some world expresses that, for all worlds accessible from it, if ph holds at that world, then it also holds at all worlds accessible from that latter world, a condition which is arguably less natural. Benoît On Tuesday, September 21, 2021 at 10:34:40 PM UTC+2 [email protected] wrote: > The change makes sense to me. I mean, I'm not sure I'm up on all the > implications but I don't see any downsides. > > For what it is worth, http://us.metamath.org/ileuni/nf2.html also holds > in iset.mm (although I don't have much to say about what axioms it > depends on, given how different the predicate logic axioms are in iset.mm > compared with set.mm). > On 9/21/21 2:19 AM, 'ookami' via Metamath wrote: > > I'd love to hear whether you support, or disagree with, a change of the > definition of 'not free'. > > ookami schrieb am Dienstag, 21. September 2021 um 11:16:50 UTC+2: > >> The past few days I built up bootstrapping theorems around an alternative >> definition of 'not free' based on nf2. They show, that in the presence of >> ax-10 and ax-12, the current and the new nf2 based definition are >> equivalent, so nothing really changes in higher levels of mathematics. In >> the earlier parts of predicate logic both definitions can differ, though. >> >> The current definition unfolds its power only after the introduction of >> ax-10. Before it is of limited use. Technically speaking, this is due to >> the nested usage of the for-all operator, and its mixed usage of qualified >> and unqualified wff-variables. The nf2 based definition is simpler >> constructed, and so a couple of properties (e.g. validity across >> propositional connectives) can be moved closer to the definition. This >> leads to an overall reduction in axiom usage. >> >> Besides the axiom usage balance, why should it matter else? Let me draw >> your attention to the nature of ax-10 to ax-13. They are described as >> metalogical, i. e. each instance is provable from prior axioms. This >> heavily relies on an operation that Norm calls 'implicit substitution'. It >> is described by the term ' ( x = u -> ph <-> ps ) '. In essence, for a >> given ph not containing u, you must be able to find a corresponding ps, >> that does not contain x, and is equivalent to ph under the assumption x = >> u. The search is a no-brainer: You pick a set variable u not appearing in >> ph, and then do a textual replacement of x with u. The resulting ps is a >> wff with the desired property, at least as long as your wffs are built out >> of primitives around = and ∈. Unfortunately, this simple textual process >> cannot be described within our current means of logic. The closest we can >> come is ps <-> [ u / x ] ph. This immediately rises the question whether >> the disjoint condition of x and ps is not an overkill. Is there in the end >> more demanded than actually needed? Such a question leads you naturally to >> the replacement of the disjoint condition by Ⅎ x ps. You can imagine how >> disappointed I was to learn there is nearly no support of 'not free' at >> this stage. >> >> Wolf >> >> Benoit schrieb am Montag, 13. September 2021 um 01:43:41 UTC+2: >> >>> To put things in context, there has been a discussion on this topic here >>> two years ago: >>> https://groups.google.com/g/metamath/c/Ovxv2aXJOIM/m/9WRk8TgHBwAJ and >>> at that time I added a few staple theorems regarding this new definition ( >>> http://us2.metamath.org/mpeuni/df-bj-nf.html and following ones; see >>> the comment of ~df-bj-nf). It came from that discussion that indeed ~nf2 >>> would be a better definition and would globally reduce axiom usage (though >>> of course, in some cases, axiom usage would increase). The main reason is >>> that ~nf2 does not involve nested quantifiers, so usage of ~ax-10 is >>> reduced. Unfortunately, I kept postponing the plan to change the >>> definition to ~nf2, but I'm happy if you can do it. >>> >>> 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/bb93ceea-fd6a-446a-b761-152b7d2275c3n%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/bb93ceea-fd6a-446a-b761-152b7d2275c3n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4218d9ff-6529-404e-923c-1b7a9cc04757n%40googlegroups.com.
