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
<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
<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]
<mailto:[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/e4c8d638-5fe6-45dd-99d6-7503f0a24815%40panix.com.
