loicd

On a Mac keyboard, Home is Fn+Left arrow, End is Fn+Right arrow, Page up is Fn+Up arrow and Page down is Fn+Down arrow, and as you said, Delete is Fn+Backspace. The Fn key is at the bottom left of the Mac keyboard, which is diametrically opposed to the top right position of the Backspace key. You need to use your two hands to produce any of these combinations. Also, the arrow keys are half the size of the other keys.

Obviously, this is not a problem for most Mac users. Personally, I've used a MacBook Pro for more than a decade, and I eventually found that so annoying that I bought an external keyboard with full size arrow keys and dedicated Del, Home, End, PgUp, PgDn keys.

Not OP, but yes it works. I've used the 'Keyboard manager' tool from Powertoys to remap CapsLock to Esc. Never had a problem with it.

> 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.

> 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.

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.

> 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.

> Even their inventor had trouble writing correct code in their presence

I didn't know that. Could you provide a more specific reference?

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...

In section II.D:

> 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.

> 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.

> 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.

> 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.

> 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.