Only definitions dfif6 and dfif7 fail the true/false theorems: you can prove ( -. ph -> ( if- ( ph , ps , ch ) <-> -. -. ch ) ) in these cases. As Jim says none of the different variations are particularly useful unless ph is decidable, but I have a preference for dfif5 because it is the only one that *implies* that ph is decidable, so you can put it to use in negative position as well.
On Sat, Oct 5, 2019 at 11:16 AM Jim Kingdon <[email protected]> wrote: > 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 > . > -- 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/CAFXXJSs6m4132W1Qrv6A1xCAh7iz54KCvJQWm95GjkYLCTHA2A%40mail.gmail.com.
