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.
