On Monday, March 15, 2021 at 4:36:39 PM UTC-4 Benoit wrote: > On Monday, March 15, 2021 at 8:02:23 PM UTC+1 di.... wrote: > >> As an aside, it's much simpler to look at dedth instead, which uses an >> explicit "if" expression instead of a combination of logical operators. I >> think there were some plans to add "ifp" to set.mm but I guess it didn't >> make it into the statement of this theorem. >> > > It is currently http://us.metamath.org/mpeuni/bj-dedthm.html > I'd be happy to move it to Main. > > I think you should go ahead and move it there. Maybe we should replace the (very confusing) con3th proof with your bj-con3thALT and update the mmdeduction.html page accordingly.
Off and on I've been playing with some weak deduction theorem ideas in my mathbox. dedths + elimhyps provide a very compact statement of the w.d.t. using explicit substitution notation. Unfortunately proofs using it can be significantly longer - compare renegclALT to renegcl. (Longer proofs seem to be a general characteristic of proofs involving explicit substitutions, which is why we almost always use implicit substitutions, i.e. substitutions implied by hypotheses like |- ( x = y -> ( ph <-> ps ) ) in cbvalv.) Another experiment was deriving the deduction form http://us2.metamath.org/mpeuni/nfunidALT.html directly from the inference form nfuni. This didn't use the w.d.t. as we usually state it; I was exploring possible alternatives to w.d.t. that might provide shorter proofs. In this case, the proof of nfunidALT from nfuni ends up being slightly shorter than the proof of nfunid, which starts from a definition of union and also requires that the deduction form for the definition pieces already be proved. Norm -- 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/0011969d-48b3-4217-9292-5fc6567a88c5n%40googlegroups.com.
