Timeline for A meta-mathematical question related to Hilbert tenth problem
Current License: CC BY-SA 4.0
47 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 9, 2022 at 11:02 | history | edited | Glorfindel | CC BY-SA 4.0 |
broken link fixed
|
| Sep 29, 2011 at 13:16 | vote | accept | Joël | ||
| Sep 29, 2011 at 13:13 | comment | added | Joël | ...as the complement in $\{"c=c'"\}$ of the image of the set of integers $>2$ that are not sumo two primes by the constant map that sends everything to "$c=c'$". This is a perfectly valid construction in ZFC, and we thus have a well-defined set $Th(M)$ in ZFC, even if ZFC perhaps cannot provably determine wether this set has cardinality $0$ or $1$. So I believe this is what you meant and I am satisfied with that answer. Thanks again. PPS: @unknowngoogle: by all means do open a new question... | |
| Sep 29, 2011 at 13:06 | comment | added | Joël | and $M$ satisfies $c=c'$ accordingly. My problem was that when I interpreted $M$ as a set in ZFC as I was told to do, Goldbach conjecture could be indecidable and has no truth value, so I found meaningless to say "$M$ satisfies $c=c'$" if "Golbach's conjecture is true in ZFC". Now, you solved my problem by telling me to interpret everithing insided ZFC. For example, $Th(N)$ for any model $N$ would be a ZFC-set of sentences in the language (defined ultimately in terms of $\emptyset$), either empty or equal to $\{"c-c'"\}$, and in this case $Th(M)$ could be defined... | |
| Sep 29, 2011 at 12:59 | comment | added | Joël | PS: this thread has already been too long, but if you're interested in what was my problem you can read this. Consider a language with just two constant $c$ and $c'$ and a theory on this language with no non-logical axioms. Let us consider a model $M$ of that theory defined as the set of subsets of $\mathbb{N}$ with $c$ interpreted as the empty set, $c'$ the set of even integers $>2$ that are not some of two primes. Does $M$ satisfies $c=c'$? With the platonistic interpretation of model's theory (sets as naturel sets outside any axioms system), Goldbach conjecture is either true or false... | |
| Sep 29, 2011 at 12:52 | comment | added | Joël | @Timothy: your comment yesterday showed me I was on the wrong track in my attempt to understand the notion of "Model inside ZFC", and a good night over this gave me a full understanding of what you meant. I was actually misled by the phrase "Model inside ZFC" into believing that just the model was a ZFC-set, while actually you interpret everything (the language, the theory, the model) as sets in the ZFC axiomatic. Now everything is clear, so thanks again. | |
| Sep 28, 2011 at 23:00 | comment | added | Joël | @Emil, Don't worry and thanks for all your explanations. | |
| Sep 28, 2011 at 18:23 | comment | added | Emil Jeřábek | @Joël: I’m sorry for the tone of some of my comments above. | |
| Sep 28, 2011 at 16:06 | comment | added | Qfwfq | @Timothy: thank you for the link. Maybe you're converting me into a hardcore formalist/intuitionist (for foundational matters)... even if you're not one! ;) But reading your link I'm now wondering how is it possible for a set-theoretic principle (say, foundation) to be incompatible with intuitionistic logic! But this comment thread is getting too long: perhaps I'll open a new question about this in the future.. | |
| Sep 28, 2011 at 15:49 | comment | added | Qfwfq | Joel: Ah, I see now that TimothyChow had already clarified the "codifying" thing in a comment. | |
| Sep 28, 2011 at 15:42 | comment | added | Qfwfq | @Joël: I don't know if my comments above have been useful. Anyway, what logicians do is even more "confusing": they formalize [within a certain theory (such as ZFC) which they chose to treat as "the" metatheory] other formal theories of sets (such as ZF or NBG, or even a "copy" of the formal theory ZFC itself), each of which stands at the same "level" (in a hypothetical "who is more meta" hierarchy) as PA or, for what it matters, as any other mathematical object such as $\mathbb{R}^n$. | |
| Sep 28, 2011 at 15:30 | comment | added | Qfwfq | [continued] Wait... how is the latter thing $\mathbb{Th}(\mathbb{N})$ defined? Well, you must have a notion of when a model of PA (such as $\mathbb{N}$) satisfies a sentence $\phi$: then $\mathbb{N}\model\phi$ is the formal sentence of ZFC (of course written in full fledged unreadable symolism) stating the above, $\mathrm{Th}(\mathbb{N})$ is the set of sentences satisfied by $\mathbb{N}$ Wait... but there are no sets! Right: what we can only manipulate is the formal sentence $\phi\in\mathrm{Th}(\mathbb{N})$ which says this. | |
| Sep 28, 2011 at 15:30 | comment | added | Qfwfq | @Joël: for a formalist, there are no sets. There are sentences that talk about sets. And, among those, there are sentences that talk about sets that codify e.g. the following: Riemannian manifolds, the formal theory of groups, the language of linear orders, any number $n$, sentences about natural numbers (and sets thereof), PA (which stands, here, at the same 'level' as the formal theory of groups), $\mathbb{N}$, any model of PA (which stands, here, at the same level as $\mathbb{N}$), $\mathbb{Th}(\mathbb{N})$. | |
| Sep 28, 2011 at 14:56 | comment | added | Timothy Chow | Joël: Yes, model theory, like any other piece of mathematics, is written in a human-friendly style, rather than in a style which makes it evident that everything can be built on set theory as a foundation. I suspect that you, like most mathematicians, have glibly accepted that "everything can be based on set theory" without thinking too hard about what that means. If you do think about it, you'll see that this means that everything you talk about in mathematics—a differential equation, a symbol, a number, a homomorphism, whatever—must be encoded as a set. | |
| Sep 28, 2011 at 14:48 | comment | added | Timothy Chow | @unknowngoogle: To put it another way, the "little dance" I suggested was for a formalist who wants to make sense of classical mathematics as practiced by classical mathematicians. If you are not only a formalist but also a constructivist who thinks that classical mathematicians are doing something illegitimate when they reason non-constructively, then you must additionally suspend your disapproval of their use of the law of the excluded middle when you're transcribing their journal articles into (say) the Mizar proof assistant. | |
| Sep 28, 2011 at 14:47 | comment | added | Joël | @Tim: yes, definitely. This is not at all how I was understanding the phrase "interpret in ZF" so far. Honestly, the web-references about model-theory we discussed above gave me no hint that such an encoding-process was in play. I will be trying to understand details of this construction now. Thanks. | |
| Sep 28, 2011 at 14:42 | comment | added | Timothy Chow | @unknowngoogle: Classical mathematics assumes that, e.g., either $P=NP$ or $P\ne NP$, regardless of whether we, or the axioms we are willing to assume, can prove either one. If we accept this point of view, then ZFC accurately captures classical mathematical discourse. Now, if for philosophical reasons you don't accept that arithmetic statements can be true independently of whether they can be proved, then you'll reject some of classical math and you shouldn't use ZFC as your meta-theory. E.g., you might want to use IZF instead. See plato.stanford.edu/entries/set-theory-constructive | |
| Sep 28, 2011 at 14:29 | comment | added | Timothy Chow | ...of writing (x,y) as {{x},{x,y}}. Everything—symbols, strings, functions, syntactic rules—must be encoded as sets. Then something like $x\in\mathrm{Th}(\mathbb N)$ is a purely set-theoretic statement that can be expressed formally in the language of ZFC. Does that help? – Timothy Chow 0 secs ago | |
| Sep 28, 2011 at 14:23 | comment | added | Timothy Chow | Joël, you are right that one must distinguish between $\exists$ as a symbol in a first-order formula of arithmetic, and $\exists$ as a quantifier in the formal language of ZFC. To develop the model theory of arithmetic set-theoretically, we must encode first-order formulas of arithmetic as sets. For example, we could list the symbols $\exists$, $\neg$, etc., in some fixed order, and agree to encode them with the sets $\lbrace \rbrace, \lbrace\lbrace\rbrace\rbrace$, etc. Formulas would then be sequences of symbols, and sequences can be coded using the Kuratowski ordered-pair trick... | |
| Sep 28, 2011 at 13:57 | comment | added | Joël | formal sentence in ZFC. Except in the very lucky case where you can formally prove it or disprove it, I don't see while this very long sentence of ZFC should have a well-defined truth value any more than say the continuum hypothesis. | |
| Sep 28, 2011 at 13:55 | comment | added | Joël | @Emil. Our two messages crossed each other. "You are defining the truth of arithmetical sentences in a particular model of arithmetic inside ZFC. What is so difficult to understand about this?". I don't know. I just don't understand. Note that I would perfectly understand the same sentence without the last two words "inside ZFC". About your assertion about reals: I understand it as a long assertion first defining a set call $\mathbb{R}$ (I guess by the long route defining $N$, then $Q$, then $R$) and stating that some explicit subset of this set is open as you did. That's just a long... | |
| Sep 28, 2011 at 13:38 | comment | added | Joël | Emil, my comment five comments above is an example as you requested. Now please stop fighting: I am not criticizing your references or Tim's and I am a real mathematician asking in good faith. If you tell me that in these references "for some a in A" is just a colloquial way to write the formal "\exists a \in A" of ZFC, I agree with you (if only because you're at liberty to make any definition). So let's move on. Now the interpretation of sentences of PA in the model are formal sentences in ZFC even if we take the liberty to write them in plain english as we usually do in math... | |
| Sep 28, 2011 at 13:36 | comment | added | Emil Jeřábek | Re (3): You don’t define the truth of any ZFC sentences. You are defining the truth of arithmetical sentences in a particular model of arithmetic inside ZFC. What is so difficult to understand about this? A set $X$ of reals is open if $\forall x\in X\exists u,v(u<x<v\land(u,v)\subseteq X)$. This is a prefectly usual definition in ZFC. If not, what is your definition of open sets of reals in ZFC, then? If yes, why are you not worried how to define the truth of formulas like $\forall x\in X\exists u,v(u<x<v\land(u,v)\subseteq X)$? | |
| Sep 28, 2011 at 13:26 | comment | added | Emil Jeřábek | I repeat my request: show me a text which does definitions in the way you demand. Since the bulk of modern mathematics is supposed to take place in ZFC, it shouldn’t be hard to find. | |
| Sep 28, 2011 at 13:25 | comment | added | Joël | I have been hesitating in my interpretation of what you were saying... At some times my understanding that you meant by truth of the sentence in (ZFC) its provability. But Tim and other have insisted than not. Or it is a definition of truth "by induction" by which I have no idea what you mean in a formal system? | |
| Sep 28, 2011 at 13:25 | comment | added | Emil Jeřábek | @Joël: No, I don’t agree at all. Everywhere in mathematics, it is quite usual to spell most statements in words, including quantifiers and logical connectives. It would be completely crazy to write everything as a symbolic formula. In any case, it makes no difference, since the two are just different ways of writing the same thing, and you have yourself just admitted that you understand what it means, so the conclusion is that you are only trying to make a point. | |
| Sep 28, 2011 at 13:20 | comment | added | Joël | In (2), the first $\exists$ is a symbol of PA, while the second is a symbol of ZFC. So, I am right that my understanding (2) is what Tim or you are saying when you talk of a model is ZFC? No assuming (2) is right, we shall interpret for example the PA sentence $\exists a: a=0$ by $\exists a : a \in \mathbb{N} \wedge a=\emptyset$. (or something like that, I am not familiar with the exact syntax of ZFC. Now I come to my main problem (which may disappear if I have misunderstood (1) or (2)): (3) How do you define the truth value of a ZFC sentence like the one above? ... | |
| Sep 28, 2011 at 13:09 | comment | added | Joël | Now, assuming you agree with (1), my problem with what Tim (and other, including you?) is saying is that he keeps insisting that he understand models as formal things in ZFC, not as platonistic sets. So perhaps I don't understand what he means by that, but it seems to me that the interpretation if the model $\mathbb{N}$ of a PA sentence should be a well-formed ZFC sentence. There is no well-formed ZFC beginning by "for some $a$ in $A$". So my understanding (2) is that a PA sentence beginning by $\exists a, ...$ should be interpreted in the model $\mathbb{N}$ as $\exists a \in \mathbb{N},..$. | |
| Sep 28, 2011 at 13:03 | comment | added | Joël | @Emil: No, these reference are not formal. For example, in the link given by Tim (end of first paragraph of its Edit above), in the fifth line of the definition of the satisfaction relation, "$\exists x, \phi(x)$" is interpreted as "for some a in A, ...". Now "for some a in A, ..." is not (the beginning of) a statement of ZFC, is it? (or I am getting crazy?). What is a statement of ZFC is $\exists a \in A, ...$. So please, let us call what I have just said (1) and if you want to answer, tell me if you agree if (1) so that we can have et least this small bit of understanding in common... | |
| Sep 28, 2011 at 11:46 | comment | added | Emil Jeřábek | And here is a proof of the completeness theorem in Isabelle: afp.sourceforge.net/entries/Completeness.shtml . The definition of satisfaction (readable, but quite terse) is in section 3 "Formula", subsection 3.9 "Validity". What’s the background theory is unclear to me (Isabelle is a generic theorem prover). | |
| Sep 28, 2011 at 11:22 | comment | added | Emil Jeřábek | I should have thought about proof assistants before. Someone has done the work already, of course. A formalization of the definition of the satisfaction relation in Mizar is here: mmlquery.mizar.org/cgi-bin/mmlquery/meaning?article=zf_model ("funcnot 4" and subsequent definitions). It is for models of set theory rather than arithmetic, it assumes $\in$ is always interpreted by set membership, and the background theory is Tarski–Grothendieck rather than ZFC, but these are inessential details. It is also perfectly unreadable. | |
| Sep 28, 2011 at 10:37 | comment | added | Emil Jeřábek | Or is it simply that you do not understand how to do inductive definitions in ZF? In that case you should consult some textbook on set theory first. | |
| Sep 28, 2011 at 10:31 | comment | added | Emil Jeřábek | @Joël: What you say does not make any sense to me. Both references are as formal as it gets, short of writing down an inscrutable formula in some Coq-like proof assistent. Would you care to give an example of a definition and/or argument that you do consider to be formalizable in ZF? | |
| Sep 28, 2011 at 1:41 | comment | added | Joël | So I really don't understand what you mean when you say, for example "$\exists x:\phi(x)$ is satisfied by $\mathbb{N}$ if there exists $x \in \mathbb{N}$ such that $\phi(x)$ is satisfied by $\mathbb{N}$." I am not trying to play the smart ass, I am really requesting help here. The references you and Emil gave me treat the sets as intuitive, non-formal, object, so as a Platonist I have no real problem interpreting what that means, but you keep insisting that it is a formal, syntactic, notion of model, and I don't get it. Thanks for helps (I'm ready to read another ref., if it mentions ZF)... | |
| Sep 28, 2011 at 1:31 | comment | added | Joël | ...I understand the above in a realist (platonist) way. I know what is a set, what is an element of a set, what it means to test something for all $x$. When I was a graduate student, I took some basic introduction to model theory and this is how I was taught models. But when I get back here, I am told (by Emil, you Timothy, and others) that the model you consider are not "platonist set" but set of ZF. And then I get (sincerely) confused. For I don't know what is an element of a ZF-set (though I know what means $x \in X$, nor what means "for all" in ZF (though I know $\forall$)... | |
| Sep 28, 2011 at 1:25 | comment | added | Joël | unknowngoogle, I have the same doubts/confusions as you have. But Timothy, I have an even more basic problem: I still don't understand your definition of "ℕ satisfies ϕ. You, and before you Emil, gave me two web-references. I read them, and didn't think I had any problems with them: they use sets in an informal way, not mentioning ZF or any other formalized set theory, and define a model of a theory as a set $M$ with etc., and the satisfability in the model of a formula of the form $\forall x, \ \phi(x)$ as "for all elements $x$ of $M$, (the interpretation of $\phi(x)$ holds". | |
| Sep 28, 2011 at 0:51 | comment | added | Qfwfq | (...) It holds formally in ZFC (for trivial reasons: it's in the "logic package" you use to manipulate axioms of ZFC), but it's not "real", as in the "real world" truth is an incomplete concept (by Goedel applied to ZFC). [Of course what said about PA and ZFC also holds for any theory T and metatheory S ]. | |
| Sep 28, 2011 at 0:51 | comment | added | Qfwfq | (...) A ZFC formula like $(\phi\in \mathrm{Th}(\mathbb N))\vee (\phi\notin \mathrm{Th}(\mathbb N))$, on the contrary, doesn't say "a certain sentence is true in the real world" so says nothing about arithmetic 'truths' (Perhaps you can codify it in an exotic way into PA, but it's not the point). So, if we consider an undecidable (in ZFC) sentence of the form $\phi\in\mathrm{Th}(\mathbb{N})$, then we must observe that the principle of excluded middle does not hold for "real world truth" about arithmetics. (...) | |
| Sep 28, 2011 at 0:50 | comment | added | Qfwfq | I'm getting confused about undecidability now... I agree that, from the point of view of ZFC, $\phi\in\mathrm{Th}(\mathbb{N})$ is just like any other well formed formula $\psi$. The point is that from the point of view of arithmetics "$\phi\in\mathrm{Th}(\mathbb{N})$" reads "$\phi$ is true in the real world". (...) | |
| Sep 28, 2011 at 0:18 | comment | added | Qfwfq | (Right: I should have written $\mathrm{Th}(\mathbb{N})$, as in your answer) | |
| Sep 27, 2011 at 18:09 | comment | added | Timothy Chow | By the way, it's wrong to write $\mathrm{Th}(PA)$ (boldface or not!) because by definition, only structures (and not axioms) can satisfy sentences. | |
| Sep 27, 2011 at 17:58 | comment | added | Timothy Chow | ϕ∈Th(N) could be undecidable in ZFC; however, ZFC will prove (ϕ∈Th(N))∨(ϕ∉Th(N)). In other words, "either ϕ is true or false" is a theorem of ZFC even if neither ϕ∈Th(N) nor ϕ∉Th(N) is provable in ZFC. Again, there's nothing special about "true sentences of arithmetic" here. ZFC always proves $\psi\vee\neg\psi$ for any $\psi$ regardless of whether $\psi$ or $\neg\psi$ is provable, because ZFC is based on classical logic. I will reiterate that my suggestion here is NOT that "ϕ is true" should be interpreted as "ϕ is provable in ZFC" but as "ϕ∈Th(N)" (for ϕ a first-order sentence of arithmetic). | |
| Sep 27, 2011 at 17:27 | comment | added | Qfwfq | (uh, $\mathrm{Th}(PA)$ should not be typeset in boldface..) | |
| Sep 27, 2011 at 17:25 | comment | added | Qfwfq | ... of ZFC the alternative "Either $\phi$ is true or $\phi$ is false" doesn't always hold: $\phi\in\mathrm{Th}(\mathbb{PA})$ could be undecidable in ZFC (in the sense that ZFC doesn't formally prove "$\phi\in\mathrm{Th}(\mathbb{PA})$" nor its negation). Am I saying nonsense? | |
| Sep 27, 2011 at 17:24 | comment | added | Qfwfq | Very clear answer. But I think there's one more ambiguity on which one should shed some light. A formalist (such as myself, I think) interprets "The arithmetic sentence $\phi$ is true" as "ZFC (formally) proves that $\mathbb{N} \models\phi$" or "$\phi\in\mathrm{Th}(\mathbb{PA})$" (where both $\mathbb{N} \models\phi$ and $\phi\in\mathrm{Th}(\mathbb{PA})$ are really first-order sentences of ZFC). But with this formalistic definition of truth (lacking a "real world" against which to check truth), which is always relative to a certain metatheory such as ZFC, by Goedel incompleteness... | |
| Sep 27, 2011 at 16:35 | history | edited | Timothy Chow | CC BY-SA 3.0 |
Added explanation of satisfiability relation; added 120 characters in body
|
| Sep 26, 2011 at 21:35 | history | answered | Timothy Chow | CC BY-SA 3.0 |