Reopened: How to define 'Not Free'

[ookami]

Hi,

I recently uploaded a couple of theorems to my Mathbox, starting with http://us2.metamath.org:88/mpeuni/wl-section-nf.htm, that demonstrate how things could have developed, if one had picked http://us2.metamath.org:88/mpeuni/nf2.html instead of http://us2.metamath.org:88/mpeuni/df-nf.html as the defining term for 'Not Free (Ⅎ)'.

The results show, that one can expect in predicate logic an overall reduction of the usage of http://us2.metamath.org:88/mpeuni/ax-10.html, and perhaps a marginal decrease in use of http://us2.metamath.org:88/mpeuni/ax-12.html.

This certainly positive result is due to the more symmetric structure of nf2 wrt to negation, and the avoidance of mixed quantified and not quantified variables. But it comes with a price, too:

• There is more friction in the transition between hb* and nf* style theorems;
• Axioms like ax-5 need the old style for full exploitation, so there is a sort of disruption in technique present.

You will find more details in a http://us2.metamath.org:88/mpeuni/wl-section-nf.html.

But these are my thoughts. Let me hear how you think about a change of definition of 'Not Free'.

Wolf Lammen

[ookami]

I was asked somewhere else to elaborate more on

> There is more friction in the transition between hb* and nf* style theorem;

Yes, it is still technically possible to convert from hb* to nf* via nfi.  But nfi, proved from nf2, depends both on ax-10 and ax-12 (see wl-nfi). Such a use counteracts our goal of minimizing axiom usage.  Hence, in some cases, different proofs
 for both versions are inevitable.  One such example is nfth. We cannot base its proof on nfi, but instead have to replay the proof replacing ph with E. x ph in an a1i step.  This is demonstrated in wl-nfth, already available on github, but not yet on the web site.

Wolf

[Benoit]

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

[ookami]

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

[ookami]

I'd love to hear whether you support, or disagree with, a change of the definition of 'not free'.

[Jim Kingdon]

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).

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/bb93ceea-fd6a-446a-b761-152b7d2275c3n%40googlegroups.com.

[Benoit]

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

[ookami]

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.