Theorem biigb 159

Description: This proof of bii 158, 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 147, compared to over 800 steps were the proof of bii 158 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.

Assertion

Ref	Expression
biigb	⊢ ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))

Proof of Theorem biigb

Step	Hyp	Ref	Expression
1		df-bi 147	. 2 ⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
2		ax-1 4	. . 3 ⊢ (χ → (θ → χ))
3		ax-1 4	. . . . 5 ⊢ (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))))
4		df-bi 147	. . . . . . . . 9 ⊢ ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))
5		ax-1 4	. . . . . . . . 9 ⊢ (¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → (¬ ¬ (χ → (θ → χ)) → ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))))
6	4, 5	ax-mp 7	. . . . . . . 8 ⊢ (¬ ¬ (χ → (θ → χ)) → ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))))
7		ax-3 6	. . . . . . . 8 ⊢ ((¬ ¬ (χ → (θ → χ)) → ¬ ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ))))
8	6, 7	ax-mp 7	. . . . . . 7 ⊢ (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ)))
9		ax-1 4	. . . . . . 7 ⊢ ((((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ))) → (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ)))))
10	8, 9	ax-mp 7	. . . . . 6 ⊢ (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ))))
11		ax-2 5	. . . . . 6 ⊢ ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → (((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))) → ¬ (χ → (θ → χ)))) → ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))) → (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ)))))
12	10, 11	ax-mp 7	. . . . 5 ⊢ ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ((((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))) → ¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))) → (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ))))
13	3, 12	ax-mp 7	. . . 4 ⊢ (¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ)))
14		ax-3 6	. . . 4 ⊢ ((¬ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))) → ¬ (χ → (θ → χ))) → ((χ → (θ → χ)) → (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))))
15	13, 14	ax-mp 7	. . 3 ⊢ ((χ → (θ → χ)) → (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))))
16	2, 15	ax-mp 7	. 2 ⊢ (¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) → ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))))
17	1, 16	ax-mp 7	1 ⊢ ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain