Hi all ! I'm new to chat so please tell me if I'm doing something wrong :)

@user21820: I'd like indeed to ask you further about the question I asked.

I'm still considering Euclid's postulates. There is something "different" about the 5th one, and from the start Euclid was trying to prove it using the other 4.

Then someone came and "ignored" it. By "ignoring", I mean he took a step back, and created an alternate 5h postulate.

So there is a new foundation, with 5 axioms, which leads to spherical geometry (or hyperbolical heomretry).

Now, if I'm not mistaken, our Universe is not flat. It has a slightly negative curvature as the expansion is accelerating.

So here, by taking a step back and changing an axiom, it's possible to come up with a "meaningful" theory, ie one which describes our actual Universe.

So my question is: is there intrinsically something "different" about this 5th postulate ?

Now, just to see if I understood your comments properly: what you're saying (and I totally agree) is that any theory is "sound", ie we can move forward up to some points and prove more and more theorems.

And mathematics are self-consistent, in the sense that a theory will not include any inconsistencies (even if, according to Gödel, it means it will always be incomplete, and we will always need some "out of the box view" to go further)

Did I get that right ?

@xdutoit No, unfortunately it seems that most of what you wrote has a lot of misconceptions.

Any formal system (including FOL systems) are just systems that generated theorems according to some precise syntactic rules. This is just a matter of syntax, and whether a formal system is meaningful at all is a separate matter.

For example, the game of chess can be seen as a formal system that generates (all valid) chess games, each of which is a sequence of moves. Is this formal system (i.e. chess) meaningful?

We may attempt to design a formal system whose theorems can be interpreted to assert something about reality. Whether we succeed or not can never be proven. We can merely test it empirically to increase our confidence (or hope) that we succeeded.

Before we even get into a mathematical discussion of Euclid's postulate, we need to realize the fact that Euclid's so-called axioms are extremely imprecise almost to the point of meaninglessness. You should look up Hilbert's or Tarski's axiomatizations of euclidean geometry to see that basically Euclid did not do a good job, which is also why there are logical errors everywhere.

This is not to say that Euclid did not contribute much to mathematics; he did because his rudimentary attempt to formalize geometric reasoning was an important first step, and his writings instructed many generations of mathematicians. But now, if you want to actually want to have a proper discussion of euclidean geometry, you basically need to discard those 'axioms' that do not really mean anything and instead look at an actual proper axiomatization.

@xdutoit I never once said that any theory is "sound". Not at all. Soundness has to do with truth/semantics, but as I said earlier a formal system may be completely meaningless (and hence there is no useful notion of truth for it), in which case asking whether it is "sound" is not even meaningful.

@xdutoit And in the setting of a proper axiomatization of euclidean geometry, there is nothing different about a suitable representation of the fifth postulate, other than the fact that people felt it was different and tried to prove it from the others plus all the missing axioms that Euclid failed to include to support his reasoning. The sole point of the alternative models of those axioms minus that one is to show that we cannot prove that one from the rest. It says nothing about reality.

Again, I want to emphasize that nothing you do in playing with formal systems can ever tell you some new truth about reality. The most it can tell you is that formal systems that are inconsistent cannot be correct about reality no matter how they are interpreted.

@xdutoit Finally, nobody knows whether ZFC (the current foundational system for mathematics) is consistent or not, and Godel's theorems shows that you cannot claim that mathematics is self-consistent unless you are using illogical reasoning (such as circular reasoning)...

Essentially all professional logicians believe that PA is consistent and sound, and even something stronger than PA called ATR0. However, beyond that point soundness starts to get unclear, and a few logicians are not sure that Z2 (second-order arithmetic with full comprehension) is sound. Still, most are confident that ZFC (which is way stronger than Z2) is consistent, but I have never seen any good justification for Z2 or ZFC even on an intuitive basis.

Nevertheless, nobody has found any contradiction in ZFC so far.

Thanks a lot for this detailed answer !

I'm not an native english speaker, I guess I shouldn't have used the word "sound" (I meant in fact "coherent")

@xdutoit I see.. Yes, we can say that regardless of whether a formal system is meaningful, we can still play the symbol-pushing game, just like we can play chess. In that sense it is still a coherent or well-defined system.

Still, no way to establish consistency. We can only hope and sometimes check empirically.