- #26
- 472
- 63
Although the discussion has run its course, there is a small point that should be pointed out. If we look at the wiki definition:Yes, basically I think if we define a predicate WO(x) (where x∈ℕ), which should describe whether the program corresponding to index x(computing a function ℕ2 to {0,1}), describes a well-order (of ℕ with any order-type) or not . Then we can define the smallest ordinal α such that: "theory T can't prove any computable well-order relation with order-type α as a well-order."
Though I am not fully sure whether this is the standard definition, if there is one (or whether there are multiple definitions?).
"a well-order on a set S is a total order on S with the property that every non-empty of S has a least element in this ordering."
So, while the above definition would fit perfectly well when T can talk about "every non-empty subset of", it seems that it isn't straight-forward when that is not the case.
For example, quantification over ℕ (like in PA) really has to be insufficient to describe the property "WO(x)" that was described in the quote above. If that was true, then the set containing the elements for which WO(x) is true would be an arithmetic set (which is known to be false).
So, if there is no explicit way to describe the property WO(x) for some T, then it seems the definition would definitely have to be different in that case (in one way or another).