3:51 AM
@user76284 Lol I shouldn't have used the same symbol "ℕ" inside the induction axiom. This wasn't suppose to mean the meta-level ℕ but rather just the symbol for the domain. So, no, the second-order induction axiom is enough.
I was careless to say "applying that axiom to the domain" and "forces the domain to be ℕ". What I should have said was: It forces the domain to be order-isomorphic to ℕ, by applying the axiom to the interpretation of { "0", "1", "1+1", ... }, which must be equal to the domain by the axiom, and hence shows that ℕ is order-isomorphic to the domain via interpretation of the numeral encoding of ℕ.
Order-isomorphic if the language includes < and the theory proves ∀k∈N ( k<k+1 ). Isomorphic with respect to + if the theory proves ( num(k)+num(m) = num(k+m) ) for every (meta) naturals k,m, where num(k) denotes the numeral for k. Same for ·.
Obviously, if you just have the induction axiom alone and nothing else to constrain the language, then it is just isomorphic in the sense of a bijection. Once you constrain the language in some way that the meta ℕ is constrained (because in MS we simply have ℕ as a model of PA), then the essentially unique model of the theory would be forced to look like the real ℕ with respect to that constraint.
For example, if the theory has the second-order induction axiom plus associativity for + and identity 0 for +, then it proves ( num(k)+num(m) = num(k+m) ) for every (meta) naturals k,m, and we can show this by (meta) induction. We didn't even need commutativity of +.
@user76284 I realize you're asking specifically about the linked axiomatization. What I wrote above applies in general, but yes if you want to use that particular axiomatization, and you apply the induction axiom to the terms { "0" , "S(0)" , "S(S(0))" , ... }, then you need the first two axioms listed to get order-isomorphism. And for isomorphism with respect to + or · or < you also need some other axioms.
4:22 AM
If the reals and the computable reals have the same first order theory - then where does the distinction between the two emerge?
2 hours later…
8 hours later…
2:34 PM
2 hours later…
4:12 PM
@Threnody It makes sense. As MaliceVidrine said, the very fact that we can prove the existence of a non-computable real is because we are not working entirely within the theory of the reals, but are working within MS in which we construct the reals via say Cauchy sequences of rationals and can prove that there are uncountably many of them, whereas obviously there are only countably many computable reals.
However, you might ask various related questions, such as whether we can prove what we want that has say real-world applications. Well, we can't handle anything more than computable reals in practice. We sometimes even just only manipulate rationals. So in many cases we do not need the full strength of MS, and can make do with weaker theories. Even then, we cannot just work within the first-order theory of ℝ because it is just too weak.
For foundational purposes, at the very least, you want to have the axioms of PA for ℕ for plus the usual first-order axioms about ℝ. Someone has indeed thought about such a question:
1
To expand on my answer, first let T be the theory with sorts ℕ,ℝ (you can think of a sort as a predicate-symbol and interpret "x∈T" as "T(x)") and the axioms of PA for ℕ plus the first-order real axiomatization for ℝ, and ℕ⊆ℝ (i.e. ∀x∈ℕ ( x∈ℝ ) ). This is not enough, because T does not prove IVT, which we would like to have. So that is where the extra axiom Sup comes in.
It seems to me that to even state IVT we need to be able to encode and decode every sequence of reals as a single real, and that to do so I think we need to extend the induction schema of PA to all properties over T and not just arithmetical properties.
For example, by the extended induction schema we can prove ∀x∈ℝ ( 0<x ∧ ∀k∈ℕ ( k<x ⇒ k+1<x ) ⇒ ∀k∈ℕ ( k<x ) ).
This is great! It implies that floor and ceiling are definable for every positive real that has an integer upper bound!
That's good, because then we can use real numbers in the range [0,1) to encode binary sequences because we can extract the k-th binary digit in its binary expansion using some definable function over T. And once we have (countably infinite) binary sequences, we can easily encode any sequence of binary sequences, which we can interpret as a sequence of reals.
The reason is that for each real r∈[0,1) we can extract the k-th binary digit by looking at floor(r·2^k) mod 2.
> Internal IVT: ∀f∈(ℚ→ℝ) ( f encodes a continuous function on ℝ ∧ f(0)<0<f(1) ⇒ ∃x∈ℝ ∀p∈ℚ ( ( p<x ⇒ f(p)≤0 ) ∧ ( p>x ⇒ f(p)≥0 ) ) ).
Okay that was a mouthful, and I still haven't told you what "encodes a continuous function" means. But I want to state it to get the intuition going first. We don't have ability to quantify over all functions from ℝ→ℝ, so we will use functions from ℚ→ℝ as a proxy, because every continuous function can be encoded by its values on ℚ. Also, we can't evaluate f∈(ℚ→ℝ) on arbitrary real x but we can evaluate it on the rationals before and after x.
@XanderHenderson: Let me know if you're lost at any point, because I'm trying to make it understandable with minimal background in reverse mathematics. =)
Back to encoding continuous functions. By the earlier described encoding of sequences of reals, the quantification "∀f∈(ℚ→ℝ)" is essentially just a "∀f∈ℝ" with suitable decoding of f to extract the values of the decoded function on ℚ. So we are not going beyond the capability of the theory T.
We define that f encodes a continuous function iff ∀e∈ℝ+ ∃d∈ℝ+ ∀x∈ℝ ∀a,b∈ℚ ( |a−x|+|b−x|<d ⇒ |f(a)−f(b)|<e ). It is a fun exercise to show (in your favourite foundations for mathematics) that this is equivalent to the usual definition of continuity, in the sense that every f∈ℚ→ℝ that encodes a continuous function can be extended to a continuous function from ℝ→ℝ.
5:13 PM
Okay we are done stating Internal IVT. Guess what? I just realized that I cannot show that T does not prove IVT... I gave T too much power. But at least I can show that T cannot prove the internal supremum axiom:
> Internal Sup: ∀f∈(ℕ→ℝ) ( ∃x∈ℝ ( f≤x ) ⇒ ∃m∈ℝ ( f≤m ∧ ∀y∈ℝ ( f≤y ⇒ m≤y ) ), where "f≤x" is defined as "∀k∈ℕ ( f(k)≤x )".
Here it is stated as a single axiom (in my linked post I had stated it as a schema because I did not extend the induction axiom so I could not use encoding of sequences of reals). Note that it is internal; it does not say anything about sequences from ℝ that the external meta-system can see; in a model it only quantifies over sequences that are encoded as some real in the model.
T is satisfied if ℕ is interpreted as the naturals and ℝ is interpreted as the set C, because C satisfies the FOL theory of ℝ and the induction schema is already true in this interpretation.
But that interpretation fails to satisfy Internal Sup, because there is an upper-bounded computable sequence of reals whose supremum is not computable. I just checked; wikipedia says Specker is the first known person to have constructed such a sequence.
So for foundational purposes we want T plus Internal Sup. Interestingly enough, this is in fact "half decent" @MaliceVidrine and you will find that you can do practically all basic real analysis within this system!
And yet, T plus Internal Sup (like the system in the linked post) has a model with ℝ interpreted as the finite-jump-computable reals.
@Threnody So just to say something about "mathematical practice", in practice we actually only need T plus Internal Sup. I am lazy and from now on will call this theory SRA (simple real analysis).
1 hour later…
6:46 PM
Wow this answer is massive! Thank you :) I got stuck at a bunch of places starting from here.. I can reason through it informally however. Even saying it out loud makes sense.
floor(r·2^k) mod 2. - I take it this is binary multiplication? i.e. multiplying by 2 is a shift to the left, and then we use mod 2 to collapse it to a single digit 0 or 1. Shouldn't it be k-1?
Internal IVT : Aren't you assuming f(0) < f(1) here? ( p<x ⇒ f(p)≤0 ) ∧ ( p>x ⇒ f(p)≥0 ) ) : We're quantifying over all p in Q. I wonder what would happen if instead of x in R, we write x in Q?
floor(r·2^k) mod 2. - I take it this is binary multiplication? i.e. multiplying by 2 is a shift to the left, and then we use mod 2 to collapse it to a single digit 0 or 1. Shouldn't it be k-1?
Internal IVT : Aren't you assuming f(0) < f(1) here? ( p<x ⇒ f(p)≤0 ) ∧ ( p>x ⇒ f(p)≥0 ) ) : We're quantifying over all p in Q. I wonder what would happen if instead of x in R, we write x in Q?
As an aside - what does 'internal' here mean? I'm familiar with IVT but not 'internal IVT'. I'm also confused by the fixation on '0' in the statement of Internal IVT
7:10 PM
« first day (1480 days earlier) ← previous day next day → last day (1342 days later) »
