Hacker News new | ask | show | jobs
by loicd 1070 days ago
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.
2 comments

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.

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

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

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

Can you give an example of a nontrivial statement that's true in every model?
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.

I didn't claim you'd claimed it ;)

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?