Automated Reasoning in Higher Order Logic
Mathematics Related Software
Let φ be a proposition. Assume false. Then we have φ.
The following background is necessary to understand this theorem.
(.) "false" is a proposition.
The following background is necessary for the proof.
(.) Let A and x be objects. Then x∈A is a proposition.
(.) ∅ is an object.
(.) false is the proposition given by ∅∈∅.
(.) Let x be an object. Assume x∈∅. Let φ be a proposition. Then we know φ.
Since false, we know ∅∈∅. Using this, we conclude φ.
Test yourself on this item.