On 10/5/19 3:53 AM, Benoit wrote:
Finally, there are several possible definitions (~df-bj-if, ~bj-dfif2 through ~bj-dfif7). Which one to take as *the* definition ? The current one might be the easiest to understand. On the other hand, I think that one should take one for which the two theorems ~bj-iftru and ~bj-iffal still hold intuitionistically. I haven't checked all variants, but I think this works for ~bj-dfif2, which furthermore has no negation in it. This would favor that one.
Using bj-difif2 would (intuitionistically) gain bj-iffal but (I think) lose bj-casesif (and probably a lot of other ways of demonstrating if(ph, ps, ch)).
I suspect that none of this is very useful intuitionistically unless ph is decidable (see for example http://us2.metamath.org:88/ileuni/pm2.54dc.html ). Which probably makes me lean towards the more straightforward df-bj-if
-- 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/afb962aa-8b41-cdad-2ffa-e6dd4f6e8c93%40panix.com.
