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/b61d830c-5303-4af7-9ed6-4ba89921fc2an%40googlegroups.com.
