bj-df-if and df-ifp

[Richard Penner]

As I understand it , there was a proposal was to make bj-dfif5 the primary definition for the logical conditional operator: if- ( ph , ps , ch )  and rename it df-ifp. If so, then the three things to decide are 1) what to call the new definition, 2) how to reorder the new definitions and rebase the proofs on the new definition axiom and 3) where in set.mm to promote the new definitions and related theorems.

Since df-bj-if and bj-dfif3 are also more frequently used than the rest, I propose the following changes, either for Benoit's sandbox or for the eventual home of this somewhere between cases2 and ax-5. (I would suggest right before meredith would allow translations of all wff connectives in terms of  the  logical conditional operator while leaving the axiom-deriving section of meredith as a sort of appendix to the section on propositional logic.)

df-ifp = bj-dfif5 , dfifp2 = df-bj-if , dfifp3 = bj-dfif3 , dfifp4 = bj-dfif2 , dfifp5 = bj-dfif4, dfifp6 = bj-dfif6, dfifp7 = bj-dfif7

This requires a new proof for dfifp2 and a revised proof for dfifp3 which I have supplied below (modulo line wrapping conventions from CONTRIBUTING.md).

Remarkably, this reordering just happens to also order the definitions by date.

  $( Definition of the conditional operator for propositions.  See ~ dfifp2 , ~ dfifp3 , ~ dfifp4 , ~ dfifp5 , ~ dfifp6 , and ~ dfifp7 for alternate definitions.  (Contributed by BJ, 22-Jun-2019.) $)

  df-ifp $a |-

            ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) ) $.

  $( Alternate definition of the conditional operator for propositions.  (Contributed by BJ, 22-Jun-2019.)  (Revised by RP, 21-Apr-2020.) $)

  dfifp2 $p |-

            ( if- ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) ) $=

    ( wif wa wn wo wi df-ifp cases2 bitri ) ABCDABEAFZCEGABHLCHEABCIABCJK $.

  $( Alternate definition of the conditional operator for propositions.  (Contributed by BJ, 30-Sep-2019.)  (Revised by RP, 21-Apr-2020.) $)

  dfifp3 $p |-

            ( if- ( ph , ps , ch ) <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) $=

    ( wif wi wn wa wo dfifp2 imor pm4.64 anbi12i bitri ) ABCDABEZAFZCEZGOBHZACH

    ZGABCINQPRABJACKLM $.

  $( Alternate definition of the conditional operator for propositions.  (Contributed by BJ, 30-Sep-2019.) $)

  dfifp4 $p |-

               ( if- ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( ph \/ ch ) ) ) $=

    ( wif wi wn wa wo dfifp2 pm4.64 anbi2i bitri ) ABCDABEZAFCEZGMACHZGABCINO

    MACJKL $.

  $( Alternate definition of the conditional operator for propositions.  (Contributed by BJ, 2-Oct-2019.) $)

  dfifp5 $p |-

         ( if- ( ph , ps , ch ) <-> ( ( -. ph \/ ps ) /\ ( -. ph -> ch ) ) ) $=

    ( wif wi wn wa wo dfifp2 imor anbi1i bitri ) ABCDABEZAFZCEZGNBHZOGABCIMPO

    ABJKL $.

  $( Alternate definition of the conditional operator for propositions.  (Contributed by BJ, 2-Oct-2019.) $)

  dfifp6 $p |-

            ( if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ -. ( ch -> ph ) ) ) $=

    ( wif wa wn wo wi df-ifp ancom annim bitri orbi2i ) ABCDABEZAFZCEZGNCAHFZ

    GABCIPQNPCOEQOCJCAKLML $.

  $( Alternate definition of the conditional operator for propositions.  (Contributed by BJ, 2-Oct-2019.) $)

  dfifp7 $p |-

               ( if- ( ph , ps , ch ) <-> ( ( ch -> ph ) -> ( ph /\ ps ) ) ) $=

    ( wa wi wn wo wif orcom dfifp6 imor 3bitr4i ) ABDZCAEZFZGOMGABCHNMEMOIABC

    JNMKL $.

[Benoit]

Hi Richard,

I've been meaning to move it to Main for a while but haven't found time/motivation to do it yet... I'll try and do it this week.  My plan was simply to swap bj-df-if and bj-dfif5, since they are proved equivalent by ~cases2, and leave the rest unchanged.  I haven't checked if your method makes the total proof length shorter.  I'll make the PR asap so we can discuss on concrete grounds.

Benoît

[Richard Penner]

Ah. Well my proof of dfifp3 is necessarily longer than that of bj-dfif3 which relies on bj-dfif2 to do half the work. 

The main problem I had with simply swapping bj-dfif5 and df-bj-if is that bj-dfif2 and bj-dfif4 use df-bj-if directly which means to preserve both their proofs and their numbering (other than the definition and "5"), the proofs would have to come in an order corresponding with the partial order  (df) -> 5 -> 2 -> 3 , (df) -> 5 -> 4 , (df) -> 6 -> 7 ; Say (df) -> 5 -> 2 -> 3 -> 4 -> 6 -> 7.

You might be OK with that or you might want to have an ordering consistent with numbering,  in which case we need to free up the dependency of 2 and 4 on 5.

So here is a proof of bj-dfif2 in terms of bj-dfif5 as df-ifp

    ( wif wa wn wo wi df-ifp cases2 pm4.64 anbi2i 3bitri ) ABCDABEAFZCEGABHZNCH

    ZEOACGZEABCIABCJPQOACKLM $.

and here is a proof of bj-dfif4 in terms of bj-dfif5 as df-ifp

        ( wif wa wn wo wi df-ifp cases2 imor anbi1i 3bitri ) ABCDABEAFZCEGABHZNCHZE

    NBGZPEABCIABCJOQPABKLM $.

Good luck with the move.

[Benoit]

This is done in PR #1604 (https://github.com/metamath/set.mm/pull/1604).  Feel free to shorten some proofs and add credits.  By the way: I like your theorems using if- .  I think that you can add this one:

  ( ph /\ ps ) <-> if- ( ph , ps , ph )

it is to ~bj-ifdfan what ~bj-ifdfor2 is to ~bj-ifdfor. And consequently:

  if- ( ph , ps , ph ) <-> if- ( ps , ph , ps )

Benoît