dfbi1ALT

Description: Alternate proof of dfbi1 . This proof, discovered by Gregory Bush on 8-Mar-2004, has several curious properties. First, it has only 17 steps directly from the axioms and df-bi , compared to over 800 steps were the proof of dfbi1 expanded into axioms. Second, step 2 demands only the property of "true"; any axiom (or theorem) could be used. It might be thought, therefore, that it is in some sense redundant, but in fact no proof is shorter than this (measured by number of steps). Third, it illustrates how intermediate steps can "blow up" in size even in short proofs. Fourth, the compressed proof is only 182 bytes (or 17 bytes in D-proof notation), but the generated web page is over 200kB with intermediate steps that are essentially incomprehensible to humans (other than Gregory Bush). If there were an obfuscated code contest for proofs, this would be a contender. This "blowing up" and incomprehensibility of the intermediate steps vividly demonstrate the advantages of using many layered intermediate theorems, since each theorem is easier to understand. (Contributed by Gregory Bush, 10-Mar-2004) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	dfbi1ALT	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$

Proof

Step	Hyp	Ref	Expression
1		df-bi	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
2		ax-1	$⊢ χ \to (θ \to χ)$
3		ax-1	$⊢ \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
4		df-bi	$⊢ \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
5		ax-1	$⊢ \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to (\neg \neg (χ \to (θ \to χ)) \to \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))))$
6	4 5	ax-mp	$⊢ \neg \neg (χ \to (θ \to χ)) \to \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
7		ax-3	$⊢ (\neg \neg (χ \to (θ \to χ)) \to \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))) \to (((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg (χ \to (θ \to χ)))$
8	6 7	ax-mp	$⊢ ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg (χ \to (θ \to χ))$
9		ax-1	$⊢ (((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg (χ \to (θ \to χ))) \to (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to (((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg (χ \to (θ \to χ))))$
10	8 9	ax-mp	$⊢ \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to (((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg (χ \to (θ \to χ)))$
11		ax-2	$⊢ (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to (((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))) \to \neg (χ \to (θ \to χ)))) \to ((\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))) \to (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to \neg (χ \to (θ \to χ))))$
12	10 11	ax-mp	$⊢ (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))) \to (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to \neg (χ \to (θ \to χ)))$
13	3 12	ax-mp	$⊢ \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to \neg (χ \to (θ \to χ))$
14		ax-3	$⊢ (\neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))) \to \neg (χ \to (θ \to χ))) \to ((χ \to (θ \to χ)) \to (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
15	13 14	ax-mp	$⊢ (χ \to (θ \to χ)) \to (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))$
16	2 15	ax-mp	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))$
17	1 16	ax-mp	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$

Metamath Proof Explorer

Theorem dfbi1ALT

Proof