Cantor's theorem: Difference between revisions

Revision as of 21:28, 6 October 2021

Revision as of 21:52, 6 October 2021

Line 38:

Despite the simplicity of the above proof, it is rather difficult for an [[automated theorem prover]] to produce it. The main difficulty lies in an automated discovery of the Cantor diagonal set. [[Lawrence Paulson]] noted in 1992 that [[Otter (theorem prover)|Otter]] could not do it, whereas [[Isabelle (proof assistant)|Isabelle]] could, albeit with a certain amount of direction in terms of tactics that might perhaps be considered cheating.<ref name="Paulson1992"/>

[[File:Cantor's Theorem Visual|thumb|A visual showing the two possible ways x could map to its image. In neither case can it map to B. Green arrows represent possible mappings and red arrows impossible mappings.]]

==When ''A'' is countably infinite==

Let us examine the proof for the specific case when <math>A</math> is [[countably infinite]]. [[Without loss of generality]], we may take {{math|1=''A'' = '''N''' = {{mset|1, 2, 3, …}}}}, the set of [[natural number]]s.