4 ms·

> Thus, the question is what is the implied context? I claim that this context consists of commonly agreed upon axioms. If I understand correctly, you claim it

> Thus, the question is what is the implied context? I claim that this context consists of commonly agreed upon axioms. If I understand correctly, you claim it is a mental model. As I mentioned in a sibling comment, I dispute your claim that most mathematicians work from foundational axioms such as ZFC. I think the number of mathematicians who can actually write down the axioms of ZFC is far smaller the number who claim that mathematics is founded on ZFC, and the number who actually do rigorous proofs in ZFC a discipline other than logic far smaller still. If a mathematician has never seen a rigorous proof of a theorem from the axioms of ZFC, and either seen it machine checked, or hand verified it (probably intractible for most real maths), can they say it's true if they subscribe to your approach to truth? I don't think they can. Given that these proofs don't even exist for most theorems (there are efforts to build libraries of machine checked proofs, but even ignoring the fact that the most recent of these don't start from ZFC, they are by no means complete) it would seem to me that most mathematicians must adopt a more Platonist approach. To be clear, I like the idea of axiomatisation and I'm a fan of the introduction of proof assistants (indeed I've used Coq pretty heavily in the past), but I dispute that rigourous proof is what actually determines truth; the human understanding of the naturals predates it's formulation in PA, if PA cannot prove something that we know to be true from our understanding of the naturals then that is a limitation of the axiomatic process, we should not start changing our notion of the naturals to fit the axioms. > This is therefore a notion of validity rather than satisfiability. As I mentioned in another reply, I have not seen the term validity used in this context, only in cases where the formula is true in all models; this is regular semantic entailment. Note that your original claim, however, was > A statement is true by definition if and only if it is satisfied in every model. Did you mean to say "satisfied in every model that satisfies ZFC"? I am more comfortable with this as a valid mathematical position (although I still claim it is nonstandard terminology); I disagree, but my disagreement is purely philosophical, whereas I hold that the original claim is so nonstandard as to be incorrect.

loicd 3y ago
> I suspect that most mathematicians are Platonists (this may be my bias creeping in) and they believe the objects they work with are real > [...] I dispute that rigourous proof is what actually determines truth [...] This is perhaps a bit out of topic, but to me these two statements are contradictory. I suppose that you should define what you mean by "real" (and Platonism). I certainly think that mathematical objects are real, but by that, I mean that they exist independently of my own mind. However, they can't exist independently of a mind if truth is determined by evaluation against a mental model. Even if that mental model is shared within a community, because that would turn mathematics into a belief system. Also, the human mind is fallible and prone to mistakes, so in my view, it is reasonable to doubt what comes out of it. Sure, mathematicians agree on axioms for things like natural numbers, and deduction rules. However, I think that the reality of natural numbers and proofs (as mathematical objects) does not stem from a shared mental model, but from their finitary nature, which makes it possible to implement them on a computer. I am also skeptical that the human mind has any innate model for most advanced concepts in mathematics (I even doubt that it is true for real numbers). I think that the intuition we have of most mathematical objects is formed after exposure to simpler mathematical notions. That intuition is shaped by what is proved and disproved from prior mathematical knowledge. Yes, proofs written by mathematicians don't look very formal (and often, the more advanced are the maths, the less formal and detailed are the proofs), but I dispute that they are not rigorous and can't be translated into a formal framework. In my view, this is mostly a matter of efficiency and practicality. To illustrate what I say, consider Mochizuki's claimed proof of the abc conjecture[1]. Here we have a claimed proof so difficult that most specialists fail to determine whether it is correct or not, although Scholze&Stix believe there is a gap. I say that most mathematicians don't have a mental model that allows them to determine whether the abc conjecture is true or not, and because of the fallibility of the human mind, it is reasonable to doubt those that claim they do. One can of course take sides, but in that case, we are no longer doing mathematics. The only thing that can resolve the issue will be a more readable and more rigorous proof. That's what determines truth. [1]: https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs
- denotational 3y ago
  I don’t think my position is contradictory: I believe that (non-technical, unqualified/alone) “true” is a property that exists independently of whether we are able to formally prove something in some kind of logic. This is because we are making assertions about “real” objects (e.g. the naturals), and I believe that these statements are either true or false. I think this is a philosophical disagreement that we’re unlikely to resolve. It’s not clear to me which definition of (non-technical, unqualified/alone) “true” you are using. We’ve had a few: 1. Your original definition, where we say P is true iff it holds in all compatible models (which I claim is highly nonstandard); 2. The definition you started using later, where we say P is true iff it holds in all models of ZFC (which I claim is still nonstandard); 3. The definition I suggested, where we say P is true iff it holds in some “standard model”; 4. Something else. Let’s consider the naturals; what is your opinion on the truth of the Gödel sentence for ZFC (let’s assume consistency, otherwise definition 2 cannot possibly be useful)? Under definition 3 is is true, but under definition 2 it isn’t. If you think it isn’t true then you are saying that we don’t really understand the naturals intuitively and we can only understand them by axiomatisation. I cannot counter that position mathematically, only philosophically, but I will say that we have seemingly used and understood the naturals for a very long time before they were first effectively axiomatised, so it seems to be a bold claim. This is very far away from my original point, however, which was purely about your position that “true” means “true in all models” (i.e. definition 1), however it seems you are no longer adopting this position (in favour of definition 2)? When used in a technical sense, as far as I am aware “true” is always qualified with respect to some specific model, which may be obvious from context and thus not explicitly stated, but there is always a formal model in mind; truth is generally seen as a model-theoretic concept, not as proof-theoretic one. Re. ABC and IUTT, I’m fully behind Buzzard et al. pushing for machine verified proofs, as I say, I have been a big user of Coq. I just don’t think we can ever say that proof is what determines truth given we know from Gödel that proof is fundamentally limited. Proof is a good way of convincing ourselves something is true, indeed anything we prove true is in fact true by soundness, but it’s not the arbiter of truth.
  - loicd 3y ago
    > This is very far away from my original point Yes, the discussion has deviated, and I don't think we will resolve the disagreement, but I wanted to make my position clearer w.r.t to the claim that "most mathematicians are Platonists [...] and they believe the objects they work with are real". > It’s not clear to me which definition of (non-technical, unqualified/alone) “true” you are using. I may be elliptic and not very clear, but I have not changed my definition. We can't do mathematics in a vacuum. There is always a context, which consists of a language, i.e. a fixed set of constant, function and relation symbols, and a theory, which is a fixed set of statements of the language. Typical theories are ZF, ZFC, PA, etc. For me, "true" (alone) means satisfied in all models of the theory, and equivalently by completeness, provable from the theory. (And by the way, your notion of "true" (alone) as "satisfied in the standard model" is equivalent to requiring that the theory be complete.) That would be your definition 1, except for the "non-technical" part. Now, the discussion deviated towards set theory because to compare my idea of "true" (alone) with yours, I used your comment: > “True in the standard model” is generally what most working mathematicians who are not logicians mean by “true”. which lacked context and seemed to me to be especially problematic in the context of set theory. And also, "most working mathematicians who are not logicians" implies a context of set theory. So the "non-technical" definition would be your definition 2 although I think ZF+DC (the axiom of dependent choice) is closer to what most mathematicians won't have a problem with than ZFC (depends on the discipline I suppose). Probably a mistake to talk about "most mathematicians" though. > If you think it isn’t true then you are saying that we don’t really understand the naturals intuitively and we can only understand them by axiomatisation. I mean something more subtle. I think we understand the naturals intuitively but only to some extent. Enough to write some axioms, but not enough to reliably answer many seemingly simple questions about them. I also think that our intuitive understanding is not static but grows as we study mathematics. > we can ever say that proof is what determines truth given we know from Gödel that proof is fundamentally limited. This is perhaps where the disagreement is? I don't have a problem with the fact that proofs are fundamentally limited.

loicd 3y ago

> I suspect that most mathematicians are Platonists (this may be my bias creeping in) and they believe the objects they work with are real > [...] I dispute that rigourous proof is what actually determines truth [...] This is perhaps a bit out of topic, but to me these two statements are contradictory. I suppose that you should define what you mean by "real" (and Platonism). I certainly think that mathematical objects are real, but by that, I mean that they exist independently of my own mind. However, they can't exist independently of a mind if truth is determined by evaluation against a mental model. Even if that mental model is shared within a community, because that would turn mathematics into a belief system. Also, the human mind is fallible and prone to mistakes, so in my view, it is reasonable to doubt what comes out of it. Sure, mathematicians agree on axioms for things like natural numbers, and deduction rules. However, I think that the reality of natural numbers and proofs (as mathematical objects) does not stem from a shared mental model, but from their finitary nature, which makes it possible to implement them on a computer. I am also skeptical that the human mind has any innate model for most advanced concepts in mathematics (I even doubt that it is true for real numbers). I think that the intuition we have of most mathematical objects is formed after exposure to simpler mathematical notions. That intuition is shaped by what is proved and disproved from prior mathematical knowledge. Yes, proofs written by mathematicians don't look very formal (and often, the more advanced are the maths, the less formal and detailed are the proofs), but I dispute that they are not rigorous and can't be translated into a formal framework. In my view, this is mostly a matter of efficiency and practicality. To illustrate what I say, consider Mochizuki's claimed proof of the abc conjecture[1]. Here we have a claimed proof so difficult that most specialists fail to determine whether it is correct or not, although Scholze&Stix believe there is a gap. I say that most mathematicians don't have a mental model that allows them to determine whether the abc conjecture is true or not, and because of the fallibility of the human mind, it is reasonable to doubt those that claim they do. One can of course take sides, but in that case, we are no longer doing mathematics. The only thing that can resolve the issue will be a more readable and more rigorous proof. That's what determines truth. [1]: https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs

denotational 3y ago
I don’t think my position is contradictory: I believe that (non-technical, unqualified/alone) “true” is a property that exists independently of whether we are able to formally prove something in some kind of logic. This is because we are making assertions about “real” objects (e.g. the naturals), and I believe that these statements are either true or false. I think this is a philosophical disagreement that we’re unlikely to resolve. It’s not clear to me which definition of (non-technical, unqualified/alone) “true” you are using. We’ve had a few: 1. Your original definition, where we say P is true iff it holds in all compatible models (which I claim is highly nonstandard); 2. The definition you started using later, where we say P is true iff it holds in all models of ZFC (which I claim is still nonstandard); 3. The definition I suggested, where we say P is true iff it holds in some “standard model”; 4. Something else. Let’s consider the naturals; what is your opinion on the truth of the Gödel sentence for ZFC (let’s assume consistency, otherwise definition 2 cannot possibly be useful)? Under definition 3 is is true, but under definition 2 it isn’t. If you think it isn’t true then you are saying that we don’t really understand the naturals intuitively and we can only understand them by axiomatisation. I cannot counter that position mathematically, only philosophically, but I will say that we have seemingly used and understood the naturals for a very long time before they were first effectively axiomatised, so it seems to be a bold claim. This is very far away from my original point, however, which was purely about your position that “true” means “true in all models” (i.e. definition 1), however it seems you are no longer adopting this position (in favour of definition 2)? When used in a technical sense, as far as I am aware “true” is always qualified with respect to some specific model, which may be obvious from context and thus not explicitly stated, but there is always a formal model in mind; truth is generally seen as a model-theoretic concept, not as proof-theoretic one. Re. ABC and IUTT, I’m fully behind Buzzard et al. pushing for machine verified proofs, as I say, I have been a big user of Coq. I just don’t think we can ever say that proof is what determines truth given we know from Gödel that proof is fundamentally limited. Proof is a good way of convincing ourselves something is true, indeed anything we prove true is in fact true by soundness, but it’s not the arbiter of truth.
- loicd 3y ago
  > This is very far away from my original point Yes, the discussion has deviated, and I don't think we will resolve the disagreement, but I wanted to make my position clearer w.r.t to the claim that "most mathematicians are Platonists [...] and they believe the objects they work with are real". > It’s not clear to me which definition of (non-technical, unqualified/alone) “true” you are using. I may be elliptic and not very clear, but I have not changed my definition. We can't do mathematics in a vacuum. There is always a context, which consists of a language, i.e. a fixed set of constant, function and relation symbols, and a theory, which is a fixed set of statements of the language. Typical theories are ZF, ZFC, PA, etc. For me, "true" (alone) means satisfied in all models of the theory, and equivalently by completeness, provable from the theory. (And by the way, your notion of "true" (alone) as "satisfied in the standard model" is equivalent to requiring that the theory be complete.) That would be your definition 1, except for the "non-technical" part. Now, the discussion deviated towards set theory because to compare my idea of "true" (alone) with yours, I used your comment: > “True in the standard model” is generally what most working mathematicians who are not logicians mean by “true”. which lacked context and seemed to me to be especially problematic in the context of set theory. And also, "most working mathematicians who are not logicians" implies a context of set theory. So the "non-technical" definition would be your definition 2 although I think ZF+DC (the axiom of dependent choice) is closer to what most mathematicians won't have a problem with than ZFC (depends on the discipline I suppose). Probably a mistake to talk about "most mathematicians" though. > If you think it isn’t true then you are saying that we don’t really understand the naturals intuitively and we can only understand them by axiomatisation. I mean something more subtle. I think we understand the naturals intuitively but only to some extent. Enough to write some axioms, but not enough to reliably answer many seemingly simple questions about them. I also think that our intuitive understanding is not static but grows as we study mathematics. > we can ever say that proof is what determines truth given we know from Gödel that proof is fundamentally limited. This is perhaps where the disagreement is? I don't have a problem with the fact that proofs are fundamentally limited.