Skip to main content
Source Link
Toby Bartels
  • 2.8k
  • 23
  • 39

In intuitionistic mathematics, a non-constant function from $ \mathbb R $ to $ \{ 0 , 1 \} $.

Many classical theorems can be proved to fail intuitionistically by showing that they imply this or something much like it. (Probably the most common thing is to show that the classical theorem implies the theorem $$ \forall \, x , y \in \mathbb R , \; x = y \; \vee \; x \ne y \text , $$ which doesn't look like the existence of a thing; but this is equivalent to the existence, for each real number $ x $, of a function $ f $ from $ \mathbb R $ to $ \{ 0 , 1 \} $ such that $ f ( y ) = 1 $ iff $ x = y $.)

More generally, in constructive mathematics, we don't usually assume that such functions don't exist, but we also understand that we can't prove that they do. So this still demonstrates that classical theorems can't be proved constructively (at least, not without being modified).

In a more neutral framework, we might speak of a non-constant continuous function from $ \mathbb R $ to $ \{ 0 , 1 \} $, or of a non-constant computable function from $ \mathbb R $ to $ \{ 0 , 1 \} $.

Post Made Community Wiki by Toby Bartels