@BillyRubina Only useless systems can allow you to do that. It's all to do with the incompleteness theorems, about which I believe I gave you this link before. Any system that can be considered foundational must be able to do basic arithmetic, or equivalently basic reasoning about finite strings, or equivalently verify any given terminating computation, and every such system has undecidable provability.

Funny that crazy math is more interesting than well-behaved math. xD

There are systems that are not foundational and hence can evade those criteria. Such as Tarski's axiomatization of synthetic geometry, related to RCF (theory of real-closed fields).

RCF turns out to be not only complete and decidable, but also satisfies quantifier-elimination with a computable elimination procedure.

Unfortunately, this procedure leads to super-exponential blowup in the length of the sentence, and hence in the length of the proof that you can obtain via this method.

But it gives you a very weak partial answer to your question: You can put an upper bound on the proof of a theorem of Tarski's axiomatization of geometry.

Does this make you happier? =)

Yes.

In fact, I have encountered some geometry software that was designed to use this procedure to prove (some) geometry theorems. As you might suspect though, it didn't work on complicated problems.

@user21820 Mathematica?

@BillyRubina As for crazier being more interesting, I think the converse is more accurate; interesting structures are typically crazier than boring ones. Not sure if you have seen this before, but here is a crazy video of the mandelbrot set that your comment reminded me of:

@BillyRubina It was a free software but I cannot recall its name now (too many years ago).

There are plenty of crazy things that simply aren't interesting, but it seems that being interesting almost surely implies crazy. Even RCF seems to be mocking us, being decidable but forever outside our reach because super-exponential growth cannot be handled no matter how advanced our technology gets.

@user21820 Very hypnotic.

@BillyRubina Yea haha, but I think it's safe. Though I forgot to give the standard warning for epilepsy.

I asked about Mathematica because they implemented this:

reference.wolfram.com/language/tutorial/SyntheticGeometry.html

Seems very interesting. I don't know, but at least for my limited knowledge, it was kinda magic to see synthetic geometry done in computers.

@BillyRubina The algorithm I described is very old so I won't be surprised if a ton of geometry software have tried to implement it. But I am surprised that the wolfram webpage does not claim to have an automated prover, but only says it can guess conjectures.

Anyway I don't have a good impression of wolfram, given the extremely Wrong Answers I got from wolfram alpha.

@user21820 What kind of stuff do you ask in W|A that gives such wrong answers?

@BillyRubina I ask for the limit of something, and it falsely says "does not converge". I ask for the limit of something else, and it gives a wrong limit.

Oh, yeah. Limits in W|A are not trustworthy.

At one point I gave feedback thinking that it was a bug and they would fix it, but then further testing revealed that they merely wrote some if-statements to get rid of the specific limit I mentioned.

Worse still, they did not even do that rubbish properly! At one point, the website would at first say "limit is ..." and then a few seconds later change to "limit does not exist".

I also noticed that when I gave examples on Math SE of their wrong limits, after a few months it would get rubbishly fixed. So I henceforth kept my counter-examples to myself. =D

I remember of having asked a question about how W|A could figure out the limits. People suggested that it uses an heuristic that does not guarantee the limt actually exists nor that it doesn't.

@BillyRubina That is correct. For all you know, it could have been me who told you that. Unfortunately, there are some crazy people on Math SE who do not like me criticizing WA so they downvote/delete my posts pointing that out.

But ultimately it is a sign of a bigger problem; the designers never aimed for mathematical correctness at all.

It seems that finding limits with generality would be equivalent to some unsolved/undecidable problem. I don't remember very well.

Sure, but a program can easily return an answer for limits that it can correctly compute and say "I don't know" for other limits.

@user21820 I just read a question: mathoverflow.net/q/374089/23600

I got quite surprised because Axiom actually says something like "I don't know".

@BillyRubina That's very good to see! =)

Not exactly for limits tho.

@user21820 I am now watching this with this music: youtu.be/w2UlDIw-9GI

If S is consistent, then by incompleteness there are two theorems A,B such that S proves A but S does not prove B, so A, B, A∧A, B∧B, A∧A∧A, B∧B∧B, ... is a sequence of strings that witness that f has no limit since their length is unbounded.

What is the meaning of 1 : 0 in "f(n) = ( the n-th string is provable over S ? 1 : 0)"?

@BillyRubina ( C ? E : F ) is the usual C/Java conditional expression, equal to E if C is true but equal to F if C is false.

Logic has all sorts of tantalizing stuff. I hope I get more free time to study it better.

I bought Manin's book on Mathematical Logic but I'm not reading it yet. I'll read some more elementary books.

On the other hand, if we can prove that f has a limit then we can prove that it must be 0 or 1, and it cannot be 0 because we can prove that S proves "0=0", so it must be 1, implying that S proves everything, so let Z = "0=1" and then look at the sequence Z, Z∧Z, Z∧Z∧Z, ... and note that f eventually is constant 1 so one of these is provable, implying that Z is provable.

I made a slight error above: we can prove that if f has a limit then we in fact can prove "0=1"...

The proof shows this.

Going to be away for quite a while. See you around! I'll move the music stuff to another chat-room. =)

Ok.

→ Music stuff moved to This is the Realm of Simply Beautiful Art =)