Re: [Metamath] Reopen: How to define 'Not Free'

[Mario Carneiro]

> (a) There is more friction in the transition between hb* and nf* style theorems

Could you elaborate on this? I would assume that once you have nfi and nfri you can easily convert between the two styles.

On Sun, Sep 12, 2021 at 9:16 AM 'ookami' via Metamath <meta...@googlegroups.com> wrote:

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. (a) There is more friction in the transition between hb* and nf* style theorems; (b) 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

--
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/65eeae41-40f2-40dd-9f36-2b8847c8b498n%40googlegroups.com.

[ookami]

> Could you elaborate on this? I would assume that once you have nfi and nfri you can easily convert between the two styles.

The conversion ist still possible. But nfi uses both ax-10 and ax-12, sth that I'd like to avoid if possible. This in some cases inevitably lead to different proofs for both versions.

Wolf

[ookami]

I deleted this conversation, because of awful formatting.  For some unknown reason, I was not allowed (or able) to edit my text. In the end, I deleted the one you posted to, and opened a new one with improved  style.  If possible, please react to the updated conversation.