There seems to be no objection to redefine 'not free' to nf2. If nobody objects, I'll start the transition from the next week on.
I need the upcoming weekend (2/3 Oct) to look into the mentioned Wikipedia article, and see whether it offers extra details. Benoit schrieb am Samstag, 25. September 2021 um 00:08:46 UTC+2: > 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/60d74073-14ac-47c6-b6d7-5a32bd013f80n%40googlegroups.com.
