[tybug]

A common misconception in the first paragraph:

> However, Godel shattered these aspirations in 1931 by proving the existence of true but unprovable mathematical formulas.

Godel sentences are unprovable, but they are not "true". They are independent, i.e. true in some models and false in others. The godel sentence happens to be true in the standard model - some people take liberties with this and extend to calling it true, but that's not accurate, or at the very least misleading.

[ttctciyf]

Isn't the claimed "truth" based on an appeal to a more intuitive notion of truth than a formal model-relative one?

The Godel sentence for some Formal Axiomatic System asserts, by way of numerical encoding, its own unprovability in that FAS, and since it in fact cannot be proven in the FAS it is "true" in the sense that it asserts (via its numerical encoding) something which is in fact the case, i.e. just the ordinary sense of "true".

[denotational]

“True in the standard model” is generally what most working mathematicians who are not logicians mean by “true”.

[tybug]

No disagreement here. But I hold that this is an especially confusing way of describing independent statements, especially in this paper, which certainly was written by a logician.

I take particular issue with the phrasing because it confused me for years in highschool and throughout undergraduate. How could something be true and not provable? It took me until a model theory course to realize that it cannot, and most pop descriptions of the incompleteness theorem are - dare I say it - wrong. Though I'm sure you would argue it's not wrong, merely an informal description.

I would, however, expect a bachelor's thesis not to stray into such confusing territory.

[isaacfrond]

It's exactly that point that I've never understood. Please elaborate. What is the 'standard model'?

[H8crilA]

The model of natural numbers with addition and multiplication that we intuitively understand as the correct one. As Godel showed you can't actually describe this model in first order logic (Skolem-Lowenheim further shows how hopeless we are in describing the model). "Every child knows what natural numbers actually are".

[lisper]

More concretely: you can add an axiom to standard PA that says, "There exists a number that is the Godel number of a proof of G." The resulting system is consistent, and includes a new kind of number that is not a natural number (because you can prove that N is not a proof of G for any N that is a natural number). It's analogous to adding an axiom that says, "There exists a number whose successor is 0", which introduces a new kind of number that we call "negative numbers." Math is extended in familiar interesting directions like this all the time by adding axioms like "There exists a number whose square is 2" (which gives you irrational numbers) or "there exists a number such that the successor of its square is 0" (which gives you imaginary numbers).

[Y_Y]

You didn't say otherwise, but it's interesting to note that the irrationals is quite "big" in the sense that you can do a lot without them. Not only can you make a nice consistent extension of usual structures on N, Z, Q etc by just adding sqrt(2), you can even add all square roots, or all n-th roots, or the solutions to all polynomials without getting plenty of good irrationals. Sets between Q and R are often neglected, but there's a wealth of good maths in there.

[loicd]

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.

[denotational]

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.

[loicd]

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

[denotational]

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

[loicd]

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

[MrManatee]

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

[denotational]

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.

[Y_Y]

Can you give an example of a nontrivial statement that's true in every model?

[loicd]

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

[Y_Y]

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.

[loicd]

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

[denotational]

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

[Y_Y]

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?

[zokier]

> true in some models and false in others

Isn't that the case for pretty much everything that you can twist them in any direction by the choice of axioms?

https://xkcd.com/704/

[mananaysiempre]

>> true in some models and false in others

> Isn't that the case for pretty much everything that you can twist them in any direction by the choice of axioms?

By models in this context are usually meant models of this one particular set of axioms you’re talking about at the moment (considered in some sort of ambient metatheory that isn’t always spelled out explicitly but you can go in that direction too if you want). For example, you can construct a model of PA in ZF that is morally { {}, {{}}, {{{}}}, ... } for the elements (that was not a syntactically valid formula in ZF, but you can prove a critter that is intuitively described by it exists nevertheless) and x \mapsto {x} for the successor, even though PA says nothing about sets, functions, or anything of that sort. Basically, for “model” read “implementation” (an “interpretation” of a thing within another thing is a synonymous term that actual logicians occasionally use).

(And yes, there are models of PA inside ZF that are substantially different from that one[1].)

[1] https://golem.ph.utexas.edu/category/2019/06/nonstandard_mod...