Metamath Proof Explorer

Theorem bj-stabpeirce

Description: This minimal implicational calculus tautology is used in the following argument: When ph , ps , ch , th , ta are replaced respectively by ( ph -> F. ) , F. , ph , F. , F. , the antecedent becomes -. -. ( -. -. ph -> ph ) , that is, the double negation of the stability of ph . If that statement were provable in minimal calculus, then, since F. plays no particular role in minimal calculus, also the statement with ps in place of F. would be provable. The corresponding consequent is ( ( ( ps -> ph ) -> ps ) -> ps ) , that is, the non-intuitionistic Peirce law. Therefore, the double negation of the stability of any formula is not provable in minimal calculus. However, it is provable both in intuitionistic calculus (see iset.mm/bj-nnst) and in classical refutability calculus (see bj-peircestab ). (Contributed by BJ, 30-Nov-2023) (Revised by BJ, 30-Jul-2024) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-stabpeirce	$⊢ ((((φ \to ψ) \to χ) \to θ) \to τ) \to (((ψ \to χ) \to θ) \to τ)$

Proof

Step	Hyp	Ref	Expression
1		jarr	$⊢ ((φ \to ψ) \to χ) \to (ψ \to χ)$
2	1	imim1i	$⊢ ((ψ \to χ) \to θ) \to (((φ \to ψ) \to χ) \to θ)$
3	2	imim1i	$⊢ ((((φ \to ψ) \to χ) \to θ) \to τ) \to (((ψ \to χ) \to θ) \to τ)$