Mathworks (Not the main chat!)

7:42 AM

2

Q: Predicative definition and existence of ordinal numbers

I was thinking about ordinal numbers recently, after I have read the wiki article about impredicativity. Now I have trouble to find a predicative definition of ordinal numbers, or even a "predicatively valid" ZFC-proof, that omega_1 (the first uncountable von Neumann ordinal) exists. Let me expla...

Hmm...

user21820

7:58 AM

@Secret Very interesting find.

Especially Noah's comment:

On the philosophical side of things, I believe that neither Replacement nor Powerset are usually viewed as predicatively acceptable. (I could be wrong.) But to address the question "Is there a predicative proof that $\omega_1$ exists?", I would need a precise definition of predicativity. (In particular, I don't think getting rid of Replacement entirely is a good idea - without Replacement, we can't even prove that the ordinal $\omega+\omega$ exists! So it's really a sensitive question, axiomatically speaking.) — Noah Schweber Oct 31 '16 at 0:40

Secret

ncatlab.org/nlab/show/predicative+mathematics

user21820

Like what I told you earlier, the standard set theorist answer is to use Replacement, but as Noah pointed out there, it's not usually considered predicative. He didn't give any reason, but my reason is the same as for the specification schema. Both schemas give the existence of an object that reifies some definable predicate/function. The problem is that any reification of such definable things essentially has 'access' to the entire universe, but it is a member of it.

So unrestricted reification over classical logic leads to the reified object being able to diagonalize against itself.

Secret

I am not even sure if the reals exists in predicative mathematics since blowing up powerset axiom removes a way to access it. O wait, maybe not, dedekind cuts are still valid, but I think we end up with the reals being a proper class instead

user21820

@Secret There are predicative ways to get reals as a type but not as an indicator function on the universe.

Of course, we need the power-type/set for that, but that's okay as long as we don't assume too much about the power-type.

Notice how a lot of theorems in real analysis involve quantifying over reals, but never about non-reals. That's the key to observing that they can still hold in a predicative setting.

Do you get what I mean, or should I explain in more detail?

Secret

Right so reals will be predicative regardless. However I am quite interested on what if we want to blow up power objects entirely, what can we said about the reals?

user21820

8:14 AM

Well you could use computable reals instead.

Secret

Well that's always countable then

user21820

Yeap, and they satisfy the same first-order theory of the reals.

What goes out the window is the completeness property.

So simple things like IVT already fail.

You still can have restricted versions though...

Secret

that's sound very bad from an analysis perspective, so we do need finite applications of power objects to model most of analysis

I guess for analysis we need up to $\Bbb{R}^{\Bbb{R}}$ to define real functions

user21820

Wait I think IVT still holds: Given any computable continuous function f on computable reals, if f(a) < 0 and f(b) > 0 for some computable reals a,b then f(c) = 0 for some computable real c.

Secret

Type theory is very convenient at defining functions

yeah, the computable reals, which must contain the rationals, will have to be dense

so we can always find something between two elements

We just need to define continuity over the computable reals instead of all reals

and topology will do the job (though I have not read about topology in type theory yet, but I heard they use categories to construct them)

user21820

8:21 AM

Yea, so what I was vaguely recalling was due to other things that cannot be computed, such as the limit of a bounded monotonic sequence in general.

3

Q: Is there a “nice” “constructive” field of numbers?

I am wondering about this. I've had some interest in “constructive” mathematics, although also some rather strong opinions against those who want to insist that everything else is “wrong” in favor of it. One constructive object is the “computable real number line” as an alternative to the usual ...

real-analysis computability constructive-mathematics

@Secret This one is okay. Just add computable in front of every quantifier for reals.

Anyway, I think we can even recover more analysis by allowing finite Turing jumps, since even monotone convergence theorem (MCT) will hold.

Secret

There's different degree of computability for the irrationals?

user21820

Just allow the programs to call jump oracles. Chaitin's constant is not computable but you can compute it using the first jump.

Secret

Are all reals 1st uncomputable?

user21820

I'm not sure what you mean by that. Some reals are computable.

Secret

8:36 AM

I mean, is there a maximum number of oracles needed to produce all reals?

user21820

It's going to be uncountable, because if you only have countably many jumps, you're also going to have countably many programs.

At least, that's what set theory says.

Hahaha.

@Secret In any case, I believe that if you are careful with what the power-type means, you can not only have Cauchy-completion, which seems predicative enough to me, but also have a countable model that is the reals computable via finite Turing jumps. For example, if ( S → T ) denotes the functions from S to T that are computable using finite jumps, then reals R could be identified with certain members of ( N → bool ) and then every member of ( N → R ) would be computable using some jump.

And hence you can compute an accumulation point of every member of ( N → R ) using the next jump. So MCT holds in this precise sense.

It's an interesting question and closely related to the fact that ACA suffices for all practical real analysis. ACA is equivalent to having N plus the ability to construct any set computable using finite jumps, plus full induction!

Secret

Hmm... I am starting to wonder whether the notion of uncountability is meaningful in predicative mathematics. It does seems this notion only exists because we have a cardinality larger than countable, which is usually a result of powersets. While the computable reals with finite Turing jumps is countable, do we ever need to use uncountable objects in proofs that contains no other uncountable objects?

user21820

@Secret Indeed in my opinion it's meaningless in the sense of size, but is still meaningful in the sense of complexity. Specifically, we can predicatively prove Cantor's theorem in the following form: There is no surjection from N onto N→bool. The proof is highly constructive in the sense that it holds relative to any reasonable notion of computability. For example: There is no computable surjection from N onto computable members of N→bool.

And the reason for this is that the proof corresponds to a program.

Namely G = function(F) { return function(k) { return !(F(k)(k)); }; }.

Secret

8:56 AM

I had a similar thought. Note how both Turing jumps and the ordinal $\omega$ (or perhaps, any limit ordinal) has a similar property in that both cannot technically be reached from below step by step. So we can argue that one Turing jump is equivalent to countable steps of computation

user21820

Given any F ∈ N → (N→bool), you can see that G(F) is a function that is not equal to F(k) for any k ∈ N, because F(k)(k) ≠ G(F)(k). So G constructively witnesses Cantor's theorem.

The catch is that you cannot claim that there is no injection from N→bool into N.

It's instructive to see how the standard set-theoretic argument is constructively invalid.

So in this viewpoint surjections represent complexity while injections still represent size.

Secret

Right, so everything is countable, but we still have a hierarchy of complexity

So if I understood correctly, we have cantors theorem hold, but everything stays countable since we cannot rule out injection from a "smaller" thing to a "larger" thing

user21820

Yea. To be precise, we cannot eliminate the possibility that the universe is the same size as the naturals, but we can show that there are things more complicated than the naturals. Phrased this way it seems obvious and natural. As for the limit ordinal thing, I've thought about it but am not sure what is a reasonable end point. According to this FOM post ACA actually has the ω-jump, but I'm not sure how much more it has.

Secret

Therefore contours theorem become a theorem that show that finitely uncomputable object's exists instead of uncountably large objects exists

This means, predicative mathematics don't naturally have uncountablity, but has almost everything from non constructive mathematics (the usual views)

user21820

Yeap. In this particular predicative viewpoint we must distinguish between size and complexity. It collapses in set theory. This may also explain the size-related paradoxes such as Skolem's paradox.

And this kind of distinction is exactly what I will have in my foundational system.

Secret

9:11 AM

So in predicative type theory, we will have subjection and injections having very different implications while in ZF, the two coincides as a measure of size

user21820

Yea.

Incidentally, I wanted to call my system "predicative type theory", but it seems people are already using that term haha..

Secret

9:26 AM

(Something else) Are higher order intuitionist logic predicative?

i will imagine since there exists countably long proofs in higher order logic in general, it may not be considered predicative?

user21820

Higher order logic refers to having different sorts, and does not generally refer to things with infinite proofs.

plato.stanford.edu/entries/logic-higher-order

Secret

There are many things from a set theoric background that I want to inveistgate further, but I am not sure if they are predicative (they don't seemed to be constructive though, as so far searched turned out empty). If they are predicative, then good we can put them into this model we are constructing, if they are not, they will be dealt with later.

My major reason of Topic 1 in Mathworks is to try to construct a foundation of mathematics that can allow me to learn as much as I can about infinity and I think ZF is not "big" enough. Then I made aware of predicative mathematics caused me to wonder how much weirdness of infinity we can capture in this sub-foundation

The following lists some entities that are tied to the nature of infinity that I knew:

1. Induction, transfinite induction, potential infinity

2. Computability, Turing jumps, oracles, complexity

3. Countable cardinality, uncountable cardinality (now known to be not naturally predicative)

4. Well ordering, well foundness, linear ordering, partial ordering

5. Infinite dedekind finite sets, amorphous sets, nonmeasurable sets (Requires choice axioms, impredicative and non constructive)

6. Natural numbers, Rational numbers, algebraic numbers, Computable numbers, semi-computable numbers (those that require finite Turing jumps), definable number, real number, complex number, space of all functions etc.

In particular, infinite dedekind finite sets seems to be some of the most weird things in the ZF framework, but it seems non constructive thus it may be impredicative

I also prefer higher order intuitionist logic (those that quantify over predicates as well) than axiom schemas and I am not afraid of losing compactness theorem since I want to deal with all aspects of infinity and thus in my vision, it is a world where infinite computation is possible

Had I not aware of predicative mathematics, the original goal is to find a foundation that is a non conservative extension of ZF. Now since I am aware of predicative mathematics, the refined goal is a type theory or high order arithmetic or some other foundation that captures all possible weird and predicative features of infinity

user21820

9:56 AM

@Secret It is likely that any computable formal system will have some kind of completeness theorem, and hence compactness theorem. You're conflating between semantics and syntax. Higher-order logic can easily be expressed within first-order logic by adding one predicate for each sort.

The kind of specification axioms you add to construct higher-order objects will determine the nature of the system. For example ACA is nothing more than predicative 2nd-order arithmetic.

Because ACA only allows construction of a 2nd-order object (set of naturals) that is specified by a formula that quantifies only over 1st-order objects (naturals).

This is the higher-order logic way of reifying definable predicates/functions, simply by putting them into a higher order.

Z2 is fully impredicative 2nd-order arithmetic.

Secret

3:05 PM

[A type theoric construction of second order arithmetic]

Universe Type $\mathscr{U}$

::Import Intuitionist type theory::

$\mathscr{U}_{I} : \mathscr{U}$

$\text{Finite}, =, \equiv, \text{Ind}, \text{Func}, \sum, \prod :\mathscr{U}_I$

::Defining the injective type for injective functions::

$f: A \to B, \text{func}$

$\prod_{f : \text{func}, a:A, b:B} f(a)=f(b) \iff a=b : \text{inj}$

::Defining the naturals::

$0,1,2:\text{Finite}$
$0\equiv \text{False}, 1 \equiv \text{True}, 2 \equiv \text{Bool}$
$0,1:\text{Bool}$
$m,n,0 : \Bbb{N}$

$(a:A)()^+ : A \to A, \text{inj}$

$(n^+ = 0) \equiv \bot$

$(a:A)+: A^2 \to A$

$0+n=n$

$n^++m=(n+m)^+$

$(a:A) \cdot : A^2 \to A$

$m0=0$

$mn^+=mn+m$

${}^+\circ^0 0 \equiv 0$

${}^+\circ^1 0\equiv 0^+ \equiv 1$

${}^+ \circ^{n+1}0 > {}^+ \circ^{n}0$

TBC, need to figure how to define the type for something analogoue to subsets of naturals

Transcript for

$Mathematics$ Mathworks (Not the main chat!)