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.
HN user
loicd
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.
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
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.
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).
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".
I don’t think this is a standard definition.
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.
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.
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.)
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.
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...
Nice! I got a bit enthusiastic about this: "Modern large language models are powerful but often slow to use and lack information about current events."
One of my first questions was "What is the most important thing that happened yesterday?" and I got as an answer "The most important thing that happened yesterday was President Biden holding his first press conference since taking office."
So I guess there is still work to do... Still impressive
OK, I suppose I have to dig deeper into Rust to determine whether I really disagree with that, or maybe this is too vague. The question is: who applies your workarounds? If this is always the compiler, then I agree, but if the programmer has to do any work, then your analogy fails.
Compilers already solve multiple NP-complete problems in the course of compilation after all, for example register allocation.
The NP-complete problem is optimal register allocation (through graph coloring). Register allocation in itself is not NP-complete. You can always use a suboptimal but fast algorithm because optimizations are optional. On the other hand, type checking is not optional, so having to solve a NP-complete problem for that would indeed be problematic.
The nature of the elements of the set does not matter, since the existence of a choice function on the set A guarantees the existence of a choice function on the set B as soon as there is a bijection between A and B. Thus, no matters how counter-intuitive or unnatural one finds the elements of a set, or whether they model physical reality, what matters for the axiom of choice is whether one can construct a bijection with a set that has a known choice function.
By the way, it is worth keeping in mind how Gödel proved the consistency of the axiom of choice. Roughly speaking, the steps are: start with a model of ZF, build from it an inner model where all sets are definable (in a sense) in terms of ordinals, that model (called the "constructible universe") satisfies the axiom of choice. In other words, the axiom of choice holds as soon as you assume that all sets are constructible.
There are weaker forms, those accepted in intuitionistic logic. The law of excluded middle usually appears in mathematical proofs in the form of reasoning by contradiction:
To prove A, assume not-A and reach a contradiction
To prove not-A, assume A and reach a contradiction
To prove A, reach a contradiction (without assuming not-A)
The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.
Exactly. There is also the matter of efficiency: it is easier to know why something must be true than to know how it's true. Constructibility in mathematics usually means proving things the hard way.
The idea that the axiom of choice is guilty of all the non-constructible, weird stuff in mathematics is incorrect. The actual source of non-constructibility is always the law of excluded middle (aka the difference between classical and intuitionistic logics). What is true however is that the axiom of choice amplifies in a non-trivial way the non-constructibility of the law of excluded middle.
To pick an analogy, consider the 2022 world cup. There will be a winner, but we don't know it yet. Thus, in a sense, the existence of the winner is non-constructible. In classical logic, we accept as true the following statement:
Either France is the winner or the 2022 world cup, or it is not,
In the end, the reason why the axiom of choice 'won' is the same as the reason why classical logic 'won' over intuitionistic logic: because constructibility gets in the way.
I am not OP, but it seems to me that there is an obvious problem with it. If you select a truly random set of citizens to rule a country, there are no guarantees that you will get a representative sample of the citizenry. That's simply not how statistics work. Without any further selection, you will eventually (and sooner than you would expect) put terrible or incompetent people in power. Now, if the randomly selected citizens must go through a selection process or be moderated by experts, then the actual power is in the selection process and moderation, and there is nothing democratic about it.
For what it is worth, I am French, and my country recently made a sortition experiment[1] that I found less than convincing. This was in response to the yellow vest movement. I did not feel represented by that 'citizens convention'. I do not know what part of their propositions come from them, and what part come from the experts advising them. Some of their propositions (like putting a more stringent speed limit on highways) were not implemented because, ironically, they were impopular. The whole thing felt like a failed experiment to me.
[1] https://en.wikipedia.org/wiki/Citizens_Convention_for_Climat...
The problem is that averages are constructs of the mind. It is a fallacy to think that random citizens are average citizens. You can average numbers, you cannot average people.
The idea is that you can reuse instructions for signed integer comparisons. This is explicitely mentioned in the standard, section 5.3:
Yes, sign-magnitude is the right terminology, my mistake, but too late to edit. As for two's complement, look at slide 18-19 from the link somebody produced below:
https://posithub.org/conga/2019/docs/13/1430-John-Introducto...
I want a function (isinf, isnumber etc) and I am happy.
Sure, isnan(x) is what one should use. The fact that it is `x != x` is an implementation detail. The problem is that it is also a hack that breaks the usual mathematical axioms for equality and for order relations. For instance, if you want to sort floating-point values, you have to write your own comparison predicate in case there is a NaN, because a NaN is neither smaller, greater or equal to itself.
As for infinities, they somewhat work for real numbers, but it gets more complicated for complex numbers. For instance, Annex G of the C standard stipulates that an infinite complex number multiplied by a nonzero finite complex number should yield an infinite complex number. Sounds reasonable, but consider:
(∞ + i∞)×(0 + i1) = (∞×0-∞×1) + i(∞×1+∞×0) = NaN + iNaN
All in all, what I find frustating with these aspects of IEEE754 is that they complicates things under the hood, but the benefits seem to me limited to some specialized applications.