> The formal first order proofs from ZFC that you mention depend on the axioms of ZFC. Which in turn are assumed. What is actually proven is, "If these are true

> The formal first order proofs from ZFC that you mention depend on the axioms of ZFC. Which in turn are assumed. What is actually proven is, "If these are true, then that is the conclusion." But the axioms must be assumed. What is proven is that the axioms lead to the conclusion. And not that the axioms are true or the conclusion matches our naive notions of truth or existence. That is true of every kind of mathematics. Ex nihilo nihil. There is no argument that can be made without any sort of axiom (you can derive tautologies, but only if you agree on at least the inference rules you're going to use - if you don't even agree on that you're out of luck). You don't like the axioms of ZFC, or LEM, or whatever - fine. But you can't argue that whatever you want to use instead doesn't suffer from exactly the same problems. Maybe you find your axioms "more intuitive". Okay, and you're free to do mathematics in whichever way you prefer. But I guarantee that someone else will come along and tell you that your own axioms don't look all that intuitive to them. In fact, it seems like you assume that the integers exist. But an ultrafinitist would look at you in disbelief because they don't think that infinite sets exist at all (after all, where are the infinite sets in nature?). So which axioms are the "true" ones? Personally, I'm not interested in metaphysical questions about what is "mathematically true". It's satisfying enough that a) we can constructively prove that classical proofs are valid chains of inferences from their axioms to their conclusions, b) nobody has found a contradiction in ZFC for over 100 years, c) the results we get from applying mathematics to the real world are astonishingly useful in all sorts of domains. Many mathematicians consider that a win and then move on without pondering about metaphysical things that we can never have an answer to. > This view only seems strange to us because it is impossible to study higher mathematics without being indoctrinated into the classical mathematical approach. Calling other people "indoctrinated" doesn't make your argument stronger. For the record, there's enough constructivist advocates hanging around programming-related communities, so it's not like these voices aren't heard here. edit: And in any case, you did massively shift the goalposts here, because first you claimed that "we can't reason about the reasoning used in classical mathematics" (wrong, we can do all sorts of reasoning about classical reasoning without even having to resort to infinities and other weird things), now you're claiming that classical mathematics isn't "true" (or not provably so) - but that's an entirely different discussion.