Metamath Proof Explorer

Definition df-ifp

Description: Definition of the conditional operator for propositions. The expression if- ( ph , ps , ch ) is read "if ph then ps else ch ". See dfifp2 , dfifp3 , dfifp4 , dfifp5 , dfifp6 and dfifp7 for alternate definitions.

This definition (in the form of dfifp2 ) appears in Section II.24 of Church p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's [ ps , ph , ch ] corresponds to our if- ( ph , ps , ch ) (note the permutation of the first two variables).

This form was chosen as the definition rather than dfifp2 for compatibility with intuitionistic logic development: with this form, it is clear that if- ( ph , ps , ch ) implies decidability of ph , which is most often what is wanted.

Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system { if- , T. , F. } is complete: for the induction step, consider a formula of n+1 variables; single out one variable, say ph ; when one sets ph to True (resp. False), then what remains is a formula of n variables, so by the induction hypothesis it is equivalent to a formula using only the connectives if- , T. , F. , say ps (resp. ch ); therefore, the formula if- ( ph , ps , ch ) is equivalent to the initial formula of n+1 variables. Now, since { -> , -. } and similar systems suffice to express the connectives if- , T. , F. , they are also complete.

(Contributed by BJ, 22-Jun-2019)

		Ref	Expression
	Assertion	df-ifp	$⊢ if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$wff φ$
1		wps	$wff ψ$
2		wch	$wff χ$
3	0 1 2	wif	$wff if- (φ, ψ, χ)$
4	0 1	wa	$wff (φ \land ψ)$
5	0	wn	$wff \neg φ$
6	5 2	wa	$wff (\neg φ \land χ)$
7	4 6	wo	$wff ((φ \land ψ) \lor (\neg φ \land χ))$
8	3 7	wb	$wff (if- (φ, ψ, χ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ)))$