@MatheinBoulomenos @LeakyNun @Secret: Long time no see.

@MatheinBoulomenos I'm not sure what exactly you are claiming here. I'm doubtful that you can in fact get all the results I've derived in my linked posts by merely considering some uniqueness theorem, and furthermore I think you'd face some difficulty with the complex exponential/trigonometric function. As @LeakyNun asked, where is your proof about periodicity? That is the one place I used the IVT in a non-trivial manner, and I'm intuitively sure that it's unavoidable.

If, however, you have a complete derivation of all the results in my linked post, together with your proof of the uniqueness theorem, and it's shorter than the way I prescribed, then by all means I'm interested. =)

@Secret I can't figure out what this means.

@Secret This has a vaguely similar flavour to my justification for 3-valued logic, but probably nothing more than that. Basically, if anyone is afraid of some 'strong' system, they might think they want to have a 'safe' version and only assume LEM for 'obviously well-defined' objects.

In my viewpoint, I simply use reality as the backdrop for logical reasoning. So every sentence that one can justify to be a factual statement about reality satisfies LEM (simply because it is either true or false about reality practically by definition of "factual").

And every factual sentence in general is not assumed to be about reality, so they are in general 3-valued. Either they are about reality, and have boolean truth value, or they are not. Note that a sentence with the phrase "about reality" may not necessarily be about reality, so the liar paradox will fail to cause a problem.

Now this isn't circular or dubious at all, because it didn't stipulate how one could do such justification. I'd say that's an open question. Some people think that arithmetical sentences are about reality, in which case they will assume LEM for all arithmetical sentences.

It is quite impossible to justify that any higher set-theoretical statement is about reality, so ZFC is way beyond out of the question.

@Secret It would be interesting to know what are those "few places". =)

And note that in general there is this phenomenon that some theorems have vast or elegant generalizations in 'strong' systems, but do not in 'weak' systems. This does not automatically imply that the 'strong' systems are correct. After all, an elegant but false sentence is still a false sentence.

For example, using ZFC, one can prove that every field has an algebraic closure, but so what?

In the end the results that seem to be actually needed in practical real-world mathematics about algebraic closures are provable without any set theory, which weakly supports my claim that ZFC set theory is not real-world.

@LeakyNun I think all you need is basically that the question is well-defined. Namely that any two objects of that type are either extensionally equal or not.

And since it relies on the notion of "decidable", you need at least TC.

TC proves "There is no program H such that, for every programs P,Q whose output is 0 or 1, we have H(P,Q) = 1 iff P ≡ Q.".

Just by using the standard diagonalization and program encoding.

Sorry, you want the whole type (nat→bool). So you must have some type theory at least.

Then just use the general undecidability theorem.

Hey when I did a search I see you asked this before:

@LeakyNun: You can try to do it in my system, then you can see how easy it is. =D

@Joshua Z is not well-ordered. Neither does it make sense to talk about an ordering being recursively enumerable...

Perhaps you want to make your claim a little more precise?

@user21820 hi

Hello!

@JoeShmo Hmmm.... That's a tough question. I know not much model theory, but it's actually very distinct from algebraic geometry. It just so happens that some results have been applied to other fields notably in algebraic geometry, but that's actually a rather small part of model theory itself.

@MatheinBoulomenos How have things been?

Pretty good, thanks. It's exam time right now

Ah.

Prepared for them yet?

kind of, I need to learn more numerical analysis, but other than that, yes

As for trigonometric functions, I'd use the IVT to prove periodicity, too, but I still don't need power series

@user21820 For that, I am trying to figure out how given a sum of vectors is invariant under rotation and a unique vector x that is invariant under said rotation will guarantee the sum of vector is x. Later on after I posted that, I then found that Teds probable solving strategy via invariants of group actions can fail in 3D and I foudn a counterexample to that, hence the missing refers to the proposition that is needed as a sufficient condition for the conclusion to hold given the above premises

btw you missed this question:

I might have to figure why the operation implied by the axiom of pairing $x \mapsto \{x,x\}$ is predicative later

Proof of periodicity: It suffices to show that the cosine has a positive root. Suppose that it doesn't, then $\cos(x) > 0$ for all $x>0$ and so as $\sin'=\cos$, $\sin$ is strictly monotonously increasing, so $\sin(x) > 0$ for $x>0$, thus $\cos$ is strictly monotonously decreasing on $(0,\infty)$ and because $\sin^2+\cos^2=1$, $\sin$ is bounded above by $1$ and $\cos$ is bounded below by $1$, thus the limit $\zeta= \lim_{x \to \infty} \exp(ix)$ exists

By the monotonicity of $\sin$, $\zeta$ is not real, but by the addition formula, we get $\zeta^2=\zeta$, so $\zeta=0,1$ which is a contradiction

I just don't see the point where you need power series

Maybe it's even simpler with power series because you can prove a special case of the uniqueness theorem for exp, but it feels more systematic to use the general uniqueness theorem. My point was mostly that I've seen too much textbooks and courses derive identities like exp(x+y)=exp(x)exp(y) by multiplying power series, which I feel is not the right way

@user21820 anyway, there's a seminar on logic next semester, maybe I'll take that :) (not quite sure yet)

There's no announcement of the topics, yet, so I want to see that first

@MatheinBoulomenos I see. Sorry was away just now.

@Secret I was going to say I don't understand that question. The powerset axiom does not give you a superset of any set that you can't already construct via specification.

@Secret This doesn't make sense. You said "unique vector that is invariant ..." which of course means that there is no others.

@Secret It depends. In my type theory, it isn't. The 'intuitive reason' is simply that it is hard to tell whether an arbitrary type has only member x, because x itself could be arbitrarily complicated. However, for some x the type {x} is predicative. For example, {1,2,3} is predicative.

@MatheinBoulomenos I don't buy your argument. You didn't construct the complex exponential, nor did you prove the addition formulae.

And at first I wanted to say you didn't prove cos(x)^2+sin(x)^2 = 1, but I see that you can prove it for real x from the differential equation, using Rolle's theorem after differentiating both sides.

But see you don't seem to have any complex exponential/trigonometric functions, as I stated earlier.

@MatheinBoulomenos I didn't multiply power series in my proof. Did you read it?

After I construct the complex exponential, for complex parameter x and constant c we have d(exp(x)·exp(−x))/dx = 0 and hence Rolle's theorem extended to complex differentiable functions gives exp(x)·exp(−x) = exp(0)^2 = 1. Similarly d(exp(x+c)·exp(−x))/dx = 0 so exp(x+c)·exp(−x) = exp(c) and hence exp(x+c) = exp(x)·exp(c).

@MatheinBoulomenos Ah yea see the topic first. =)

@user21820 yes, I read it, that's what I meant when I said "proving a special case of the uniqueness theorem for $\exp$". I agree that's simpler than prving the general uniquness and existence theorem.

To prove the addition formula for $\sin$, fix $y \in \Bbb R$, then consider the differential equation $f''=-f$ $f(0)=\sin(y)$ $f'(0)=\cos(y)$, both $\sin(x+y)$ and $\sin(x)\cos(y)+\sin(y)\cos(x)$ satisfy this, so they're equal by the uniquness theorem

The addition formula for $\cos$ follows in the same way

For proving the periodicity of the trigonometric functions, I don't need a complex exponential, I can just consider the function $x \mapsto (\cos(x),i\sin(x))$ and I only need $\cos^2(x)+\sin^2(x)=1$ for real $x$ for the argument

@user21820 I only have type theory. That’s the whole point. I don’t want to build a turing machine inside dependent type theory

You write "First obtain the series for $\exp$ on $\mathbb{C}$ about $0$ where $\exp$ is defined as a function such that $\exp' = \exp$ and $\exp(0) = 1$, and prove that the series converges on all of $\mathbb{C}$. Then for any $w \in \mathbb{C}$ find the series for $z \mapsto \exp(z+w)$ about $0$, which will be just $\exp(w)$ times the series for $\exp$, and thus it also converges on all of $\mathbb{C}$ and so $\exp(z+w) = \exp(z) \exp(w)$ for any $z,w \in \mathbb{C}$"

I think this is an uniquneness argument, but you use power series to show that the solution to $f'=f$, $f(0)=1$ is unique instead of a general theorem on ODEs