[FOM] Re:Clarification on Higher Set Theory

[Harvey Friedman]

>In the postings of Sean Stidd of 12 and 14 Feb and of Harvey 
>Friedman of 13 Feb
>different ways are given to motivate belief in higher set theory.
>This can be done by proving theorems using large cardinals,but unprovable in
>any other way,if these theorems are widely believed or are formulated by
>topologists within topology,etc.,(Stidd),or if it are propositions in discrete
>mathematics which reach a certain level of beauty,depth,and breadth 
>(Friedman).
>I think there is also a other way to motivate the belief in the utility of
>higher set theory.
>Laver, Steel and Dehornoy have given an example where higher set theory (the
>large cardinal axiom I3, or the existence of self simular ranks) reveals new
>theorems in the theory of self distributive systems and in topology (braid
>theory), and they give proofs wich are much more beautiful and much less
>complex as any proof within the domain itself.
>(see also my posting of 27 Jan: Set theory as a revealer)
>I think that topologists which have studied these results are now much more
>interrested in higher set theory as before.
>However I must admit that I have no knowledge of other results of 
>the same kind.
>
>                 Wim Mielants


In my case, I would rather say on the part of mathematicians: 
"recognition of large cardinals as a legitimate proof technique" than 
"belief in large cardinals".

The Laver example is a very interesting example of REMOVABLE use of 
large cardinals (not meeting one of the criteria put forth by Stidd). 
I also don't know of other such results of this kind.

There have been a number of uses of model theory in algebra and 
number theory. My impression is that almost all of these uses have 
been removed by logicians and mathematicians to the mathematician's 
satisfaction - in the sense that they feel relieved that they do not 
have to learn model theory. In some remaining cases, where the model 
theory has not yet been satisfactorily removed, there are ongoing 
programs to remove the model theory, some of these programs being 
carried out by model theorists.

Of course in the case of model theory, we never even had the prospect 
of sharp unremoveability, as we have in some cases with large 
cardinals. But nevertheless the model theory experience does indicate 
that absolute unremoveability will be a very important feature in how 
this all plays out.

On the other hand, if Laver type results become very powerful and 
very widespread in very diverse concrete settings, then they could 
ultimately have the impact we are looking for.