[FOM] Order types: a proof

[Jeremy Clark]

On Mar 9, 2005, at 7:07 pm, Hendrik Boom wrote:

> On Mon, Mar 07, 2005 at 11:31:22AM +0100, Jeremy Clark wrote:
>>
>> Or you can construct (choiceless) Brouwerian counterexamples to your
>> theorem (trivial ones: subsets of a singleton set, for example, which
>> cannot be shown to be either empty or non-empty: such a set, trivially
>> ordered, would be a counter-example to your theorem), but I don't 
>> think
>> that is what you are asking for.
>
> It would be a counterexample if it were possible to show that it not 
> one
> of the 11 known solutions.  But you can't show it differs from the 
> empty
> solution.

No you can't but that is not the point of a Brouwerian counterexample: 
you can construct a subset of {0} such that if you know either that the 
set is {}, or that it is {0} then you have resolved ... the unsolved 
mathematical problem of your choosing. You have therefore established 
that it is very unlikely that the theorem stating that there are only 
eleven order types will ever be proved, which is all you can hope to 
achieve constructively when a result has a classical proof (as 
Shipman's "11 types" theorem does in the case of the reals): a 
straightforward counterexample is impossible. Are you claiming that the 
term "Brouwerian counterexample" is a misnomer?

Regards,

Jeremy Clark