@Threnody Yes, floor(r·2^(k+1)) mod 2 is the k-th binary digit. I was lazy to check hahaha.. I don't get your first question about Internal IVT; the usual formulation does assume f(0)<0<f(1). Your second question is a good one; it fails. Consider f = ( ℝ x ↦ x<√2 ? −1 : 1 ). Then there is no rational x such that ∀p∈ℚ ( ( p<x ⇒ f(p)≤0 ) ∧ ( p>x ⇒ f(p)≥0 ) ). It also disproves your claim that you can extend every function from ℚ→ℝ to make it continuous.

In any case, if your claim were true, then I shouldn't be giving you the "fun exercise" because it would have a totally unnecessary condition "f encodes a continuous function".

As for quantifying over ℝ→ℝ, of course you can't. That's why half my explanation was about encoding and decoding because that is the only way to quantify over ℚ→ℝ. In particular:

To understand encoding/decoding, first make sure you understand definitorial expansion.

For example, smallest prime factor is definable over PA, by the predicate Q(k,p) ≡ ( k≤1 ∧ p=0 ) ∨ ∃x∈ℕ ( p>1 ∧ k=p·x ∧ ∀q ( 1<q<p ⇒ ∀y∈ℕ ( k≠q·y ) ) ).

PA proves ∀k∈ℕ ∃!p∈ℕ ( Q(k,p) ), so by (2) of the linked post we can add a new function symbol pfactor to PA and the axiom ∀k,p∈ℕ ( pfactor(k)=p ⇔ Q(k,p) ), and the resulting theory proves exactly the same sentences over the language of PA (i.e. that do not use the new symbol pfactor).

Oops I blundered in defining Q. It should be Q(k,p) ≡ ( k≤1 ∧ p=0 ) ∨ ( k>1 ∧ ∃x∈ℕ ( p>1 ∧ k=p·x ∧ ∀q ( 1<q<p ⇒ ∀y∈ℕ ( k≠q·y ) ) ) ).

The junk case ( k≤1 ∧ p=0 ) is to make sure the "∃!p" holds, because that is required by (2).

And the point of defining new symbols is so that we don't have an utterly gigantic headache when doing encoding and decoding. For instance, after defining pfactor, we can state theorems like ∀k∈ℕ ( k>1 ⇒ pfactor(pfactor(k)) = pfactor(k) ).

If you want to expand that to the original language, it would be ∀k∈ℕ ( k>1 ⇒ ∀p,q∈ℕ ( Q(k,p) ∧ Q(p,q) ⇒ p=q ) ).

But this small example shows the benefit of defining new function-symbols.

Now for the encoding/decoding issue for ℕ→ℝ. I am essentially claiming that there a bijection from ℝ to (ℕ→ℝ) via the described decoding, and we can define a new function symbol extract with signature ⟨ℝ,ℕ⟩→ℝ that agrees with that bijection! That is, for every actual real r and actual natural k, we have decode(r)(k) equal to ( extract(f,k) when ℕ,ℝ are interpreted as the actual naturals and reals ).

For example, ∀f∈(ℕ→ℝ) ∃x∈ℝ ∀k∈ℕ ( f(k)≤x ) expands to ∀f∈ℝ ∃x∈ℝ ∀k∈ℕ ( extract(f,k)≤x ).

@Threnody Finally, about "I gave T too much power", I wanted to say that T does not prove Internal IVT, but I could not prove that T does not prove Internal IVT after thinking for a while, so I gave up and used Internal Sup instead. My goal was to show that what appears to be a good combination of PA and the FOL theory of the reals is not actually enough for basic real analysis, so I needed to find some real analysis theorem that could not be proven by T.

By the way, the power of these kind of theories arise from the axioms that assert existence of reals. The theory of ordered fields doesn't force much to exist except (a copy of) the rationals. But the FOL theory of the reals has some existential axioms, which force closure under algebraic extension and hence force the existence of all algebraic reals. Internal Sup provides a lot more power than that; it forces closure under sup of internal sequences (i.e. sequences coded by some element of ℝ).

Oops, I forgot to add comprehension axioms to SRA. Lol I was more careful in my post on the main site; I used a schema because I was lazy to add comprehension axioms (contrary to what I said earlier in chat). Let me rectify that.

SRA (simple real analysis) can be defined either as:

> SRA (version 1) (following the post on Main): PA for ℕ plus FOL theory for ℝ plus ( ∃x∈ℝ ( f≤x ) ⇒ ∃m∈ℝ ( f≤m ∧ ∀y∈ℝ ( f≤y ⇒ m≤y ) ) for every f with signature ℕ→ℝ that is definable over SRA with parameters.

> SRA (version 2) (what I want to describe here): PA for ℕ plus FOL theory for ℝ plus Internal Sup plus ( ∃f∈(ℕ→ℚ) ∀k∈ℕ ∀x∈ℚ ( f(k)=x ⇔ R(k,x) ) ) for every predicate R with signature ⟨ℕ,ℚ⟩→bool.

I forgot because usually in reverse mathematics we have comprehension axioms for subsets of ℕ (rather than for real numbers), and I thought I could get away with just Internal Sup, but I forgot that I still didn't have a way to construct sequences to start with...

Anyway, here I shall only use version 2. PA for ℕ plus FOL theory for ℝ is the bare minimum that we obviously want to have. The comprehension axiom schema at the end is completely reasonable as well, because it just says that we can construct rational sequences given a defining formula.

So the powerful tool here is Internal Sup. For example, let H = ( ℕ k ↦ ( the k-th TM halts on input 0 ) ? 1 : 0 ). H is known as the halting oracle. Note that H is definable over PA. Then SRA can construct an element of ℝ encoding H: Let f = ( ℕ k ↦ Sum { H(i)/2^i : i∈{1..k} } ). Then f is a definable rational sequence over SRA so we can construct it in SRA (i.e. there is an element of ℝ that encodes it). And Internal Supremum says it has a supremum, which we know is uncomputable like H.

@user76284 I'm not sure why you have "φ(x) ↔ φ(x+1)". This makes the whole thing contradictory.

You want Q(0) ∧ ∀x∈ℝ ( ( x<1 ⇒ ¬Q(x) ) ∧ ( x≥0 ⇒ ( Q(x) ⇔ Q(x+1) ) ) ).

But although Q does pick on ℕ from ℝ over RCF, it is not definable over RCF otherwise RCF would interpret PA− and hence be incomplete, which is false because RCF is complete (even decidably so).

@user21820 I see.. I'm not sure why we're specifying uniqueness in (2). I'm also not entirely sure I'm grasping the difference in function, between inlining and definitorial expansion.

@user21820 Ooooh I see roughly what's going on.

@user21820 I see - the supremum's uncomputability is a direct consequence of H's... because we cannot compute H(i) and hence cannot compute the partial sum

But what even is 'the k-th TM' anyway?

Are we assuming some well-ordering of the TMs?

@Threnody If you do not have uniqueness, the function-symbol is not necessarily definable.

Because being able to add newly defined function-symbols given a defining predicate for which you can only prove existence will cause ZF to become ZF plus GC (global choice), and of course ZF+GC proves AC.

@Threnody Correct. Always think of TMs as programs in some idealized programming language. You can list all valid programs one by one in order of length-lexicographic order. This is a computably enumerable list, and that is all that is important. The k-th program is defined as the k-th program in that list.

@user21820 Does this have anything to do with 'well defined' as I usually see it in textbooks? i.e. x = y => f(x) = f(y)

@user21820 Oh... I see. I always had the misconception that TMs are just possibly unrestricted grammars (i.e. chomsky grammars) that can recognise programs not be the program

Or are they both?

@Threnody No. Textbooks that use the phrase "well defined" and lead you to write what you just did are lousy.

Given any objects x,y such that x=y, we always have f(x) = f(y) for any function f whatsoever. If you don't then your proof must have gone bonkers somewhere.

For example of a bonkers poof: Let f : ℚ→ℕ such that f(a/b) = a for every a,b∈ℤ such that b>0. (WRONG! You cannot construct such an f. Nothing else to say here.)

For example of a correct proof: Suppose we have the naturals ℕ but not integers and we want to construct integers. Let ~ be a relation on ℕ^2 defined by ⟨a,b⟩ ~ ⟨c,d⟩ iff a+d = b+c. Then ... Thus ~ is an equivalence relation on ℕ^2. Let ℤ = { { p : p∈ℕ^2 ∧ p~q } : q∈ℕ^2 }. Let ⊕ be a function on ℤ^2 such that p+q = { ⟨a+c,b+d⟩ : a,b,c,d∈ℕ ∧ ⟨a,b⟩~p ∧ ⟨c,d⟩~q }, for every p,q∈ℤ. Note that I didn't say ⊕ : ℤ^2→ℤ because we haven't proven it yet! Then ... Thus ∀p,q∈ℤ ( p⊕q∈ℤ ). Furthermore ...

Observe carefully that in a proper rigorous proof you do not ever need to use the term "well-defined", because every object you construct in a true proof is already well-defined (because the soundness of an FOL deductive system guarantees it).

Oh oops the definition of ⊕ I wrote above is incorrect. Sorry I'm sleepy... Correct version:

... Let ⊕ be a function on ℤ^2 such that p+q = { r : r∈ℕ^2 ∧ ⟨a,b⟩∈p ∧ ⟨c,d⟩∈q ∧ ⟨a+c,b+d⟩~r }, for every p,q∈ℤ. Then ...

Ok I've checked it. Please read it very very carefully and make sure you fully understand it. All instances of manipulation of equivalence classes must be handled properly if one wants to be mathematically rigorous.

@user21820 So the elephant in the room, when being asked to show that "f is well defined", is that: You couldn't have constructed f were it not well defined in the first place. I think I see what you mean.

i.e. the problem is that one shouldn't think functions exist just because you can write them down 'formally' and not through a formal construction (existence proof?)

@Threnody Correct.

@Threnody It is possible to rigorously construct a relation first and prove it encodes a function later. But if a textbook does not do that either, then it is almost surely non-rigorous or simply wrong. You can ask in Basic Mathematics if you see any such example and you want my comment on it.

Actually it may be of interest to you to note that you can introspect yourself to be able to understand what I say concerning "well-defined" much faster than I think most students can, simply because you have a better understanding of formal deduction.

Some students when told that you cannot define something just by writing down what you want it to be like because it is not allowed, ask, "why not?" and are not satisfied with answers like "because it may not exist and so we do not allow you to do such a thing". In some sense, many people have the erroneous notion that what they can describe must exist...

@user21820 I'm trying to follow through your reply, I think here you meant to write p ⊕ q?

@Threnody Yes, sorry about that.

I see... I've never seen Z constructed this way... well to be fair I've never seen Z constructed in any way.

@user21820 So in the formal sense of 'well-defined', we also care about soundness? So it's not just about construction? i.e. if we did not have soundness, we'd just stop calling things we construct well-defined?

I guess we care about soundness all the time. If we show a function exists from a false premise, then we didn't really show much, of course. Thank you :)

Yea.

=)

@MaliceVidrine @user2103480: I'd like to request you two to read my linked answer just to check if I made some dumb mistake. I don't think so, but I can't be too sure! =)

@user21820 Why does it make it contradictory?

Oh oops

I should’ve said phi(x) iff phi(x + 1) and phi(0) and 0 < x < 1 implies not phi(x), which picks out the integers.

What’s the strength of the resulting theory?