Since my name is mentioned in the opening post, I am going to give a quick answer here:
Am Dienstag, 28. Mai 2019 17:47:27 UTC+2 schrieb Benoit: > > ... > Indeed, there is a common pattern that the use of a non-freeness > $e-hypothesis instead of a dv-condition requires ax-11 (typically from > nfal) and ax-13 (typically from hbs1). Wolf has certainly already seen > that, but I wanted to give it more publicity by posting it on the > discussion group. I also think that in this case, both the "nf-version" > and the "dv-version" can coexist in the main part of set.mm, given that > they are in a relatively early part of set.mm, that each have their use, > that the nf-version is slightly more general, and that the dv-version > requires fewer axioms. > You are right, I know that nfal is a key theorem injecting a dependency on ax-11. I avoid it to the utmost possible. As far as ax-13 is concerned, almost all sb theorems use this axiom. Thjs is necessary because of the 'bundling' nature of df-sb. I use the tautology [ y / x ] T. as reminder of this fact. Note that T. is free of both x and y, but this won't help, as long as you don't know that x and y are different variables on substitution. I think one has to derive a complete theory of a 'substitution light' being A. x ( x = y -> ph ) or E. x ( x = y /\ ph ) (don't know what to prefer) along with a dv condition on x and y, in order to see how far you get without ax-13. > > Two remarks: > * I think that some dependencies on ax-12 can be removed (as well as some > dependencies on ax-10) by adopting an alternate definition of non-freeness, > see df-bj-nf and its comment, and compare bj-nfn with nfn. > * With the same goal as Wolf, I recently added vtoclg1f in order to remove > dependency on ax-11 and ax-13 from the important vtoclg and several > theorems depending on it (including sbc8g). > > Yes, nf2 is a good replacement for df-nf. > > Benoit > While I am at it, I'd like to point out that the propositional section is in some sense incomplete. I know for some years, that all propositional expressions can be dissected into implication chains like Ph -> ( Ps -> ... -> Ka )..) where each node in the chain is either a wff variable, or the negation thereof. An expression (like (( ph -> ps ) -> ch) can map to more than one such chain ( ps -> ch and -. ph -> ch ). In any case, this process is reversible (see ja, bija for example). This lets the above chains appear as normalized expressions covering the whole propositional logic. A few basic operations on chains like reordering (com12, con1i), adding (a1i) or dropping (syllogisms, pm2.18, pm2.61) nodes are sufficient to do all you need in propositional logic. Why do I emphasize this? Should you ever strive for automated theorem proving, then such normalized chains are a good operational base. Wolf -- 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/5d578e34-e044-4630-8525-161de7c95e08%40googlegroups.com.
