I don't deny that reading Japanese written in kana alone is currently more painful than with kanji. However, it seems to me that the current writing system is a local optimum and not a global one. If people started writing Japanese using kana alone, some adjustments would eventually be made to make it more readable, and the end result would in my opinion be superior to the current kana/kanji combination. The same thing happened with the latin alphabet. We don't use it the same way the romans used it 2000 years ago: we introduced minuscule letters, spacing, punctuation, accents... At the end of the day, Japanese is a spoken language like all other languages, and there are no reasons why a purely phonetic system should not work for writing it.
In a Japanese dictionary, you can find homonym clusters as long as something like 12 words.
Native speakers get confused in conversations and have to refer to kanji regarding which word they mean. Except they don't write down the kanji; they think of a very common word which has that kanji and say things like, "the shō syllable in my word is the same (kanji) as in shōrai".
The vast majority of the Japanese vocabulary consists of word roots made from the combination of two kanji. The language-making itself is not separable from kanji.
Japanese is only spoken language like others basically only for small children and idiots. Literate, grown-up Japanese is a written language first.
> Japanese is only spoken language like others basically only for small children and idiots. Literate, grown-up Japanese is a written language first.
I seriously doubt that. Literacy levels rose in Japan during the Meiji era and that produced pressure towards simplification of the writing system. Sure, Japan didn't go all the way to a pure kana system or to a latin-derived script, but the reasons are political and cultural (and there is nothing wrong with that) rather than linguistic.
In any cases, you didn't disprove my point, which is that the need for kanji is self-fulfilling. It feels necessary, precisely because its usage prevents the evolution of the phonetic kana system into something useful.
Well, yes? The language is built on kanji. In a 100,000 word dictionary, the vast amount of content is words that someone made up by putting together kanji. It is kanji-first. None of it makes sense when you strip away the kanji, and formation of new words is blocked. Kanji is a cultural cornerstone.
Before literacy, commoners had 5000 word vocabularies cradle to grave. Anything beyond that was the domain of the erudite elite.
> the phonetic kana system
The kana system is quasi-phonetic. It doesn't capture phonetics accurately, like IPA, and has ambiguities of its own.
But, again, phonetics doesn't help when twelve words have identical phonetics!
Sure, you can fix all this if you just change Japanese into another language.
> But, again, phonetics doesn't help when twelve words have identical phonetics!
You keep missing the point, so I'll try one last time. Look at a picture of the Rosetta stone. I can read Greek but I find the Greek part hard to read. It's written entirely in capital letters with no spacing and no punctuation. (Maybe there were people like you at the time claiming that hieroglyphs were easier to read than Greek.) Modern Greek still uses the Greek alphabet but it has evolved into something much more readable. The same thing happened to latin.
I claim that the Japanese kana system is stuck in its own figurative Rosetta era. There are no reasons why it could not evolve into something readable and not purely phonetic. With all due respect, I don't consider seriously your argument that Japanese is an exceptional language uniquely based on combination of foreign characters that can only be considered a spoken language by children and idiots. There are arguments for kanji that I find convincing, yours has to be the worst.
As for homophones, why would that be a problem? They are not unique to Japanese! For instance, in French, the only reason why 'a' and 'à' are spelt differently is to make it easier to tell them apart in writing. They are pronounced exactly the same. French has a lot more examples like that, and actually, using wrong spellings for words notoriously makes French much harder to read, even if the spelling is phonetically correct. French writing is not purely phonetic, it's only one way: if you know how to write a word, you usually know how to pronounce it but the converse is not true. Yet, it is still a much simpler system than the Japanese one. Children can fully read at age 6, although writing with few spelling mistakes takes more time.
Lol. Flashback to me having this exact conversation with a new Gaijin-kun アメリカの人 at about his second or third month in Tohoku...32 years ago. "They could just do it all in Romaji and save so much work."
and even today some of my Japanese friends joke with me about how hard 漢字 can be, they laugh because they know its hard for them and admit they wouldnt do it if they had been born anywhere else.
So, it is absolutely baked in and kanji first. without kanji the following tongue twister is indecipherable.
Thank you, thats a fun one. I particularly like the play on niwa and wani.
As for the other premise that modifying the phonetics to accomplish a simplification is based on a narrow view of the reason for retaining kanji literacy... there are important and substantive records for business, legal, and actively functional culture which exist in kanji and require kanji literacy to maintain agreement in society that is one of the differences between Japan and most other places. Who else still operates on contractual obligations from written records of the 17th century? Many current farming leases for large parts of the country are backed with the actual stamped, brush stroke written land records from then, stored at the prefecture on the original papers. Losing the ability to read and write kanji would be detrimental to ongoing cultural stability, and so it will not and should not be entertained by anyone living in that system. People living in a 'for now' mindset are irrelevant to actuality.
> There are uncountably many correct mathematical theorems. Almost all of them can't even be written in symbols.
What are you talking about? A theorem is a statement that has been proved from some axioms. A statement itself is a finite sequence of symbols satisfying some syntactical rules. The set of symbols for set theory, arithmetic, etc is finite, so the set of statements, and a fortiori the set of theorems, is at most countable. Where do you get the uncountability?
I suspect you are confusing theorems and theories. Assuming the set theory ZF (for instance) is consistent, then a consequence of Gödel's incompleteness theorem is that there are indeed uncountably many inequivalent extensions of ZF that are complete and consistent. Also, not a single one of these extensions can be described in symbols in the sense that there does not exist a computer program that enumerates a possible set of axioms for the extension.
As for your general point about arbitrariness, the late 19th century was a period when mathematicians started being concerned with the rigorous formalization of mathematics. Sure, there are some arbitrariness in the particular choice of formalization in the same way that the particular form of a programming language like C is arbitrary. However, the Gödel stuff has nothing to do with that arbitrariness, it is about the limit of formalization itself. The programming analogue is the undecidability of the halting problem. Saying that mathematics are arbitrary sounds to me a bit like saying that an algorithm like Quicksort is arbitrary because you saw an implementation in C and the particular form of the C language is arbitrary. Obviously, if you don't like the C language, you can implement Quicksort in another language. The same is true for mathematics. If some day, somebody finds a contradiction in ZF, or simply a new formalization that people find more convenient, then most mathematics will simply get translated and very little will change.
The distinction you make is correct in the sense there is indeed a fundamental difference between proving P by assuming not-P and reaching a contradiction and on the other hand proving not-P by assuming P and reaching a contradiction. However, both are called proof by contradiction. It is just plain wrong to say that the second kind is not proof by contradiction. It has been called like that for more than two millenia, whereas intuitionism is a 20th century idea. Besides, if you insist on the difference, then you have to distinguish between positive and negative mathematical properties. For instance, in your example, "finite" is positive and "infinite" is not-finite, so negative. For a classical mathematician, which is most of them, this is actually an undesirable distinction that depends on how things are defined, and is not intuitively clear.
In addition to $TERM, I wish there was a standard variable defined by terminal emulators that would contain the background color. This would let programs choose their colors accordingly, rather than try for a one-size-fits-all.
The QWERTY layout has a funny difference with for instance the french AZERTY layout. On an AZERTY keyboard, the parentheses () are directly accessible whereas the square brackets [] are not. On a QWERTY keyboard, this is the opposite : you need SHIFT for the parentheses () but not for the square brackets []. I've always wondered why the QWERTY layout favored the square brackets over the parentheses. Naively, parentheses are more common and should be more easily accessible...
I’ve always set up a custom keyboard for exactly that! () on their own keys, [] on shift and {} above 0 and 9. It always struck me as the most natural alignment for prose and programming.
Thankfully between Ukelele [0] and MSKLC [1] it’s pleasantly simple to do
And if anyone wants to go really custom, it's worth checking out the QMK firmware supported by many mechanical keyboards. Aside from the level of customisation made possible by QMK, another benefit is that everything lives on the keyboard - no need to install keyboard profiles on each machine you might connect the keyboard to.
> If one rejects the ERH, one could argue that our universe is somehow made of stuff perfectly described by a
mathematical structure, but which also has other properties that are not described by it, and cannot be described
in an abstract baggage-free way. This viewpoint [...]
would make Karl Popper turn in his grave, since those
additional bells and whistles that make the universe non-mathematical by definition have no observable effects
whatsoever.
I don't think that follows. It could be that the universe is asymptotically mathematical, in the sense that any mathematical structure falls short of perfectly describing the universe, but there is always a more sophisticated mathematical structure that is a closer approximation. The problem of course is that a mathematical description is made of a finite number of symbols. It could be that the external reality hypothesis holds, but the universe can only be described in a baggage-free way with an infinite number of symbols.
> Systems of mathematics cannot be both complete and consistent
No. They can't be at the same times complete, consistent, decidable and powerful enough to express arithmetic. You can do complete, consistent and decidable though.
Exactly. A statement is true by definition if and only if it is satisfied in every model. Also, Gödel also proved the completeness theorem that states that a statement is true if and only if it is provable. So, another way to look at undecidability is this: a statement is undecidable if and only if it can be neither proved nor disproved.
UPDATE: since first writing this comment, I’ve checked four quasi-randomly selected books from my shelves (Leary and Kristiansen Introduction to Mathematical Logic, Hodges Model Theory, Manzano Model Theory, Avigad Mathematical Logic and Computation), and they all use valid/validity rather than true/truth to describe formulae that are true in all models, as I originally pointed out below. To be clear, I’m not at all trying to score points by appealing to the literature, but I think it’s really important to clarify that your definition isn’t standard because it will confuse people; I myself was confused by this exact point when I studied logic having previously read the “true but unprovable” description of Gödel 1.
> A statement is true by definition if and only if it is satisfied in every model.
I don’t think this is a standard definition.
Every treatment I’ve seen refers to truth with respect to a model; if no model is specified, it is assumed to be obvious from context. Outside of formal treatments (i.e. in the setting where the 99% of mathematicians who aren’t logicians do their work), the model is the standard model.
First-order formulae that are true in every model are validities.
Well, I suppose it depends on your definition of standard. That's how I have been taught logic. I also believe it is the historical notion. Honestly, "true but unprovable" sounds like a bad way to explain undecidability to me. Would you have been confused by "neither provable nor disprovable" instead? Also, this introduces a bias: the axiom of choice is neither provable nor disprovable in ZF. Are you going to say it is "true but unprovable" or "false but unprovable"?
> Every treatment I’ve seen refers to truth with respect to a model
That's called satisfiability.
> Outside of formal treatments (i.e. in the setting where the 99% of mathematicians who aren’t logicians do their work), the model is the standard model.
I simply cannot agree to that. What exactly is supposed to be the standard model of ZFC? For most mathematicians, what is true is what has been proved.
> Well, I suppose it depends on your definition of standard.
Of course :) I believe my distinction between validity and truth is the one generally used in the literature (I have listed four examples above), and the one that would be understood by most working mathematicians and analytic philosophers who care about mathematical logic.
We both agree that there is a clear distinction between formulae that are true in some model (specified, or inferred from context) and formulae that are true in all models; the latter are not particularly interesting to most mathematicians once one has agreed on the logic (e.g. classical, constructive, etc.) in which one operates, hence I think it’s reasonable to use “true” to refer to the former, as indeed many authors do.
> That's called satisfiability.
Many logicians say that a formula is true in a model (sometimes true in a structure) if it’s satisfied in that model under all assignments.
Can you find me a reference in the literature where “true” is used to mean “true in all models” consistently?
> We both agree that there is a clear distinction between formulae that are true in some model (specified, or inferred from context) and formulae that are true in all models; [...]
Sure. But I feel we are deviating from the subject. We have obviously been educated differently so it is pointless to argue about that, but there is a language issue. You insist on comparing what I mean by "true" (alone) with "true in a model". However, that's an apple to orange comparison. We should be comparing what I mean by "true" (alone) with what you mean by "true" (alone), and by that, you mean: "true in the standard model". (I don't think your references validate that use, although I don't have access to all of them at the moment.) The obvious problems with that are:
- I don't think there is such a thing as a standard model in set theory (actually you cannot prove that a model of set theory exists).
- When most mathematicians say something like "X is true", what they mean is "X can be proved from the axioms of set theory", which in logical terms means "X is valid". Are you really arguing against that?
- And of course (back to the original point), you get that confusing idea that "undecidable" means "true but unprovable" (I had never heard of the incompleteness theorem being presented that way before.). I argue "undecidable" is "neither provable nor disprovable".
EDIT: "X is valid" should read "X is valid in set theory".
> When most mathematicians say something like "X is true", what they mean is "X can be proved from the axioms of set theory".
I'm just one mathematician, but I certainly don't mean that.
Before we can prove anything about sets, we need to pick some axioms. Zermelo set theory (Z) would be enough for most of ordinary mathematics. If we need something stronger, there's Zermelo–Fraenkel set theory with the axiom of choice (ZFC). Or if I need something even stronger, there's, for example, Tarski–Grothendieck set theory (TG).
What I mean by "X is true" is technically difficult to define. The statements
(1) X is provable in Z.
(2) X is provable in ZFC.
(3) X is provable in TG.
are all increasingly accurate characterizations of "X is true", but none of them capture everything about it. And that's kind of the point. There is no proof system P such that "X is provable in P" would work as a faithful definition of "X is true". So the best we can get is this tower of increasingly sophisticated axioms that still always fail to capture the full meaning of "truth".
There is a convention among mathematicians: Anything up to ZFC you can assume without explicitly mentioning it, but if you go beyond it, it's good to state what axioms you have used. ZFC is not a bad choice for this role. It is quite high in the tower. In most cases ZFC is strong enough, or in fact, overkill. But still, it is not at the top of the tower (there is no top!), so sometimes you need stronger axioms. The fact that ZFC has been singled out like this is ultimately a bit arbitrary - a social convention. "X is provable in ZFC" may be the most common justification for "X is true", but that doesn't make it the definition of "X is true".
I think there are two points of disagreement here:
1. The definition of “truth”; and
2. My claim that most mathematicians who aren’t logicians use “true” in the sense of being true in some model, not in all of them.
Re. 1, I accept that this is just naming, but I will insist that your usage of “true” is nonstandard, and should carry a disclaimer as such :)
I think this is evidenced by the fact that “true but unprovable” is a very widely used characterisation of the Gödel sentence for a logic, and it is completely wrong given your definition of “true”, and further evidenced by the references I provided that use “valid” for true in all models.
I think point 2 is a lot more fuzzy because we’re trying to talk about what is happening inside other people’s minds, in particular their view of what a mathematical result actually is; I’m happy to concede that I may be guessing wrong regarding what most mathematicians are actually thinking.
As per 1, my position is that there is no such thing as “true alone”, at least not in mathematical logic as it is conventionally presented English speaking world (and apparently in the Spanish speaking world, if one source is enough to generalise); truth only exists in the context of a model.
Accordingly, when we talk about the truth of a formula, we have a model (or possibly a class of models) in mind; I claim that when a mathematician says the Gödel sentence is true, they mean it is true in the standard model of the naturals, which is why the “true but unprovable” characterisation is used. I don’t know if my references support this, since it’s harder to find than just looking for the definition of “validity” in the index, but if you Google “truth of the Gödel sentence” you’ll find a lot of people using “true” to mean true in the standard model (of the naturals).
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 certainly believe the naturals are real, and I believe that non-standard models of the naturals are not the (real) naturals, even though I’m perfectly happy to “play” with non-standard models as an intellectual exercise. I claim that most mathematicians have other (real) objects in mind when dealing with things other than the naturals, and those form the meta-mathematical model for the notion of truth.
> When most mathematicians say something like "X is true", what they mean is "X can be proved from the axioms of set theory", which in logical terms means "X is valid". Are you really arguing against that?
That doesn’t mean “X is valid”; if something follows from the axioms of set theory then it holds in all models of set theory (yes, assuming a sound deductive calculus, but that’s a given), but that’s not enough to consider it valid, it would need to hold in all models compatible with the language. So yes, I’m arguing against that, I think what you have written is factually wrong, unless it’s a typo?
> you get that confusing idea that "undecidable" means "true but unprovable"
I don’t think I ever said this, I agree that this is confusing, and in fact it’s just wrong as stated (under my usage of “truth”), since of course there are undefinable sentences that are false (but irrefutable), such as the negation of the Gödel sentence.
> As per 1, my position is that there is no such thing as “true alone”, at least not in mathematical logic
Yes I agree. There is always some context implied if we are being rigorous. But we do use the word "true" alone. 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.
Personally, I am not sure whether I qualify as a platonist. I do have a mental model that I use to evaluate mathematical statements, but that mental model is fluctuating. It is sometimes wrong (i.e. inconsistent) and therefore in needs of an update. Because of the mere possibility of errors, I (and this may be my personal bias) only consider statements "true" those that are proven (from some agreed upon axioms).
On the other hand, if you consider mathematicians as a community, I believe that mathematicians don't share the exact same mental model. So, a statement that mathematicians (as a community) will agree is "true", will be a statement that is satisfied in all their mental models. This is therefore a notion of validity rather than satisfiability. Of course, the mental models of mathematicians are unlikely to exhaust all possible models of a given theory. However, the ultimate arbiter of truth in the mathematical community is the satisfiability in all possible models of the theory, i.e. the proof.
> 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.
> 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.
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.
> 3. The definition I suggested, where we say P is true iff it holds in some “standard model”;
By the way, I wish you would answer my previous objection about that definition in the context of set theory. What is the standard model of ZFC? (or ZF?) As far as I know, you can't prove that a model for ZF exists (unless you assume some powerful axioms, in which case you won't be able to prove that a model for the extended theory exists).
Edit: Another situation where that definition is problematic is the case of an inconsistent theory. Obviously, an inconsistent theory cannot have a standard model since it does not have a model at all. Whereas with my definition, we get the usual "Ex falso" as expected.
The standard model that most set theorists have in mind is something like the Von Neumann Universe, V. Note that this is a proper class, so it's not a structure as usually considered in model theory.
We (hopefully) can't prove V is a model of ZF in ZF, because that would amount to proving consistency and fall foul of Gödel 2, but the axioms of ZF come from an attempt to axiomatise our understanding of set theory in the sense of it being the study of the objects that make up the Von Neumann Universe.
> Obviously, an inconsistent theory cannot have a standard model
Indeed. Paraconsistent logics are an attempt to deal with inconsistency from a proof-theoretic stance, but I'm far from an expert and I don't know what models of paraconistent theories look like.
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.
I think we're understanding the phrase "true in all models" in different ways.
I understand it to mean: "true in all structures compatible with the language".
On the other hand, I think you understand it to mean: "true in all models of some latent theory left implicit", where the theory may be ZF(C) or something else depending on context?
I'm basing that on your comment:
> For me, "true" (alone) means satisfied in all models of the theory, and equivalently by completeness, provable from the theory. [...] That would be your definition 1 [...]
That isn't my definition 1, because I'm refering to all structures compatible with the language, not all models of some theory. This is probably an abuse of terminology on my part because usually we reserve the term model for structures that model a theory [1], sorry for the confusion!
> And by the way, your notion of "true" (alone) as "satisfied in the standard model" is equivalent to requiring that the theory be complete.
Please can you explain this? I don't think that's what I mean. We know that PA isn't complete, but when I say the Gödel sentence is true I mean that it's true in the standard model of the naturals.
> 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
I completely disagree with the idea that this context always existed, it's too Formalist. There is a rich history of mathematics before the concept of a formal language and a formal theory existed; if you were to ask Gauss if he worked in ZF or ZFC or TG I don't think he would have an answer, but clearly he had some concept of mathematical truth.
[1] : Although all structures are vacuously models of the empty theory, so technically they are models, but that's not very convincing or useful...
> On the other hand, I think you understand it to mean: "true in all models of some latent theory left implicit", where the theory may be ZF(C) or something else depending on context?
Yes, that's what I mean. (For me, "structure" is preferred to "model" when nothing is implied.)
> The standard model that most set theorists have in mind is something like the Von Neumann Universe, V.
Now I am getting confused. Isn't that equivalent to requiring the axiom of regularity? I have a book on set theory by JL Krivine with the theorem: "V is the whole universe iff the axiom of regularity holds". This book also proves that if "U is a universe (i.e. a model of ZF) then the collection V inside U satisfes ZF+axiom of regularity" (which proves the relative consistence of the axiom of regularity).
To talk about the Von Neumann Universe, you must assume some "surrounding" universe which is a fixed but arbitrary model of ZF. Thus, X is true in the Von Neumann Universe if and only if X is satisfied in all models of ZF+axiom of regularity. That certainly matches my idea of "true", albeit with a weaker set of axioms... (I proposed ZF+DC as a least common denominator because a large part of analysis can't be done without some form of axiom of choice.)
> Please can you explain this?
Let us call S your standard model of PA. I understood your idea of "X is true" as "S satisfies X". Now, let T be the set of all statements satisfied by S. Then T is a complete, consistent theory that extends PA and "X is true" if and only if "T proves X". (Of course, T is much larger than PA, and in fact, by incompleteness, there are no recursively enumerable theories equivalent to T.) This correspondence between complete consistent theories and models is not one-to-one though, a complete consistent theory may have infinitely many models.
> if you were to ask Gauss if he worked in ZF or ZFC or TG [...]
Fair enough, but I think he was familiar with Euclid's elements, and would have agreed on the fact that there are things that are assumed to be true because they are intuitive and things that are proved to be true. In my view, ZF is the culmination of an effort to minimize that intuitive part. By constrast, the notion of model (and Tarski's notion of truth) are more modern.
> That doesn’t mean “X is valid”; if something follows from the axioms of set theory then it holds in all models of set theory
Yes, I was being elliptic. That should read "X is valid in set theory". The point being that it is a notion of validity (ie valid in all models of set theory) rather than a notion of satisfiability (ie valid in a particular model of set theory).
For some reason the "reply" buttons past a certain level of nesting were missing for me, but that appears no longer to be the case, so I'm moving a previous comment here
The notion of relative validity is just semantic entailment, no? I have never seen that referred to in terms of validity, which has been reserved strictly for formulae that are true in all models, not in some class of models.
I’m a Platonist, and I suspect most mathematicians fall towards that end of the spectrum, so I disagree that most Mathematicians see ZFC as the arbiter of truth. They certainly aren’t doing formal proofs in ZFC, and in fact I suspect that most non-logician mathematicians would have difficulty reciting the axioms of ZFC.
That’s not to say I don’t appreciate proof theory and the desire to work in an axiomatic framework, indeed in a past life I spent most of my time formalising various things in Coq, but I don’t think it’s relevant to fundamental mathematical truth, which I believe exists outside of axiomatisation (and I think most mathematicians would agree).
> For some reason the "reply" buttons past a certain level of nesting were missing for me, but that appears no longer to be the case, so I'm moving a previous comment here
If I understand correctly, HN throttles reply speed by hiding the reply button for some time after a comment was posted. The deeper the thread the longer this timeout gets.
If you don't have any axioms, the statements that are true in every model are exactly the tautologies (by definition). Usually though, one is interested in a particular set of axioms, typically ZFC. Then "every model" implicitely means "every model of ZFC", so "true" statements are the statements that are true in every model of ZFC, or equivalently by Gödel's completeness theorem, the statements that are provable from the axioms ZFC (and only ZFC). As for examples of such statements, well, that's virtually all mathematics. (The use of exotic axioms is quite specialized within mathematics.)
Now you're moving the goalposts! You can't claim that's it's even "widely accepted" that the axiom of choice is "true". I can see this as a fine way of distinguishing DeMorgan's laws from the continuum hypothesis, but the meaning of "true" is a stickier subject.
> You can't claim that's it's even "widely accepted" that the axiom of choice is "true".
I have never claimed anything like that. The original comment was a reaction to the notion of "true but unprovable" which is wrong because what is true is precisely what is provable. You may have an intuitive notion of "true", but with logic, the devil is in the details. In my experience, it is better to stick to the mathematical definitions, especially when talking about things like the incompleteness theorem.
Now, the mathematical notions are as follows. First, you agree on some deduction rules, then some axioms (aka a theory), and by definition, what is true is what is satisfied by every model of the theory. A completeness theorem is then a theorem that states that what is true is precisely what is provable. (Proved by Gödel for classical logic.)
Of course, you may disagree with the choice of axioms. However, when introducing a new axiom, mathematicians don't argue whether it is "true" or not, they have to justify in one way or another that it is relatively consistent. The same thing is true for the deduction rules. In other words, consistency, not truth, is the right metric for axioms and deduction rules. Finally, observe that mathematicians who argue against the axiom of choice or the law of excluded middle do not claim that these are false, they claim that these are not constructive. Yet another notion not to be confused with truth.
> You may have an intuitive notion of "true", but with logic, the devil is in the details. In my experience, it is better to stick to the mathematical definitions, especially when talking about things like the incompleteness theorem.
> A completeness theorem is then a theorem that states that what is true is precisely what is provable. (Proved by Gödel for classical logic.)
As I pointed out in another comment, you are actually using a nonstandard definition of “true”/“truth” yourself; what you are calling “truth” is generally referred to as “validity”.
> However, when introducing a new axiom, mathematicians don't argue whether it is "true" or not
This is not representative of the historical development of mathematical logic and analytic philosophy at all.
Where are you getting this definition of truth? I don't think things are a neat and simple as you're making out. Are you familiar with Tarski's work on (semantic) truth?
I think it would make more sense to measure the longest computation in the number of cycles executed rather than in seconds. If I'm not mistaken, Voyager 2 had a processor running at 4MHz. So a modern 2 GHz processor will execute more cycles in a couple months than a 4MHz processor in 50 years...
reply