I'm self-studying proof theory, and working on the following problem:
Consider $s\in\mathbb{R}$, with $s>0$. Apply the Intermediate Value Theorem to prove the existence of $\sqrt{s}$.
I figure I can use the theorem to prove the existence of a root $r$ for $f(x)=x^2-s$. So, $r^2-s=0 \iff r^2=s \iff r=\sqrt{s}$.
Now, in order to apply the theorem to my function, I need to define a closed interval $[a,b]$ such that $f(a)<0$ and $f(b)>0$. If I let $a=0$, then $f(a)=-s<0$ (since $s>0$), and I'm good. But for $b$ things are not so clear. Here's what I have so far: $$f(b)>0 \iff b^2-s>0 \iff b^2>s$$ I'm not sure I can take the square root of both sides of $b^2>s$, as that would rely on the existence of $\sqrt{b}$, which is essentially what I'm trying to prove in the first place. Thinking about it intuitively, I realize that if $s>1$, then $s^2>s$, and if $s \leq 1$, then $s^2 \leq s$. Thus, $$s>1 \implies f(s)=s^2-s>0,$$ in which case I could simply set $b=s$ and know that $f(b)>0$. But if it turns out that $s \leq 1$, I'm in trouble, since $$s \leq 1 \implies f(s)=s^2-s \leq 0$$ I imagine I should set $b$ equal to something like $s+1$, or $s+\frac{1}{2}$, and it looks like $\frac{1}{2}$ is the minimum I can add to satisfy all conditions, but I'm not sure how to show that explicitely.