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 $.
--
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/2f165b11-ccab-4e13-9afb-5d2b3a0e0b32%40googlegroups.com.
