Timeline for Construction of models for true but unprovable formulas
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 11, 2022 at 11:31 | comment | added | user213800 | Fair enough then. Thanks everyone. @Burak feel free to post your comment as answer and I'll accept it. Or anyone else, really. | |
| May 11, 2022 at 10:42 | comment | added | Emil Jeřábek | I think you have a somewhat unreasonable expectations. If you really want something that works for all theories $T$ and formulas $\phi$, the syntactic fact that $T\nvdash\phi$ is the only thing you can work with. Thus, you cannot expect there to be a method that does not essentially build on syntax. | |
| May 11, 2022 at 9:33 | comment | added | მამუკა ჯიბლაძე | A non-specialist speaking (sorry). I suggest to have look at Visser's "The Interpretability of Inconsistency" (a 2014 preprint). He gives a readable exposition of Feferman's results from 1960. Quoting from the introduction: "... a theory interprets itself plus its own inconsistency. In terms of models this tells us that there is a uniform construction (of a special kind) that yields, for every model of the given theory, an internal model of the theory that satisfies the formalized inconsistency statement of the theory." | |
| May 11, 2022 at 9:05 | history | edited | user213800 | CC BY-SA 4.0 |
added 178 characters in body
|
| May 11, 2022 at 9:04 | comment | added | user213800 | Nothing wrong with syntactic models. I just wanted to know about other constructions as well, if any. I don't think I had in mind a particular notion of "naturalness" and that we are obsessing about syntacti things being less worthy; syntax is, after all, natural in its own domain. My question was meant to understand the different means available to construct such models, to get a grasp of the big picture. So I will accept any answer that provides such information. I'll edit the question to hopefully reflect this better. | |
| May 11, 2022 at 7:42 | comment | added | user44143 | @ale64bit, will you clarify in your question what sort of answers you would find natural, and what sort of answers you would accept? | |
| May 11, 2022 at 6:08 | comment | added | Andrej Bauer | What's wrong with: given a theory $T$ and an unprovable $\phi$, consider the model of $T + \neg \phi$ given by the construction in the usual proof of Gödel's completeness? Are we obsessing about syntacti things being less worthy? Or about the fact that the construction uses non-constructive principles? | |
| May 11, 2022 at 4:39 | answer | added | Peter Gerdes | timeline score: 2 | |
| May 10, 2022 at 5:23 | comment | added | user213800 | @Burak I'm not entirely uninterested in those, but it certainly would be interesting to see others beyond the semantics-by-syntax ones that Henkin's construction might produce, which feel rather artificial. | |
| May 9, 2022 at 21:55 | comment | added | jeq | You may be interested in a result of Kripke: for any r.e. $\Sigma_1$-sound extension $\textsf{T}$ of Peano arithmetic, there exists an easily definable subring $R$ of the ring of primitive recursive functions such that for any non-principal ultrafilter $D$ on $\omega$, $R/D$ is a recursively saturated model of $\textsf{T}$. His proof is given on page 16 of my 1980 thesis, arxiv.org/abs/1904.10540. | |
| May 9, 2022 at 21:17 | comment | added | Burak | If you know that your formula is not provable, your theory together with the negation of your formula is consistent and Henkin construction gives you a "kind of explicit" model of this theory as a term model. I am assuming that you are not interested in these models? | |
| May 9, 2022 at 19:36 | comment | added | Punga | This is hard to answer generally. One would need to know the motivation behind such a question to give an appropriate answer. We know such models always exist, but for strong enough theories, by Tennenbaum's theorem, we also know that we cannot really describe them in a precise (computable) way. Forcing could be one answer for set theory, similar constructions exists also for arithmetical theories - but really the model you get in the end is as difficult to understand as the depth of tools you used to obtain it. | |
| S May 9, 2022 at 19:19 | review | First questions | |||
| May 9, 2022 at 19:22 | |||||
| S May 9, 2022 at 19:19 | history | asked | user213800 | CC BY-SA 4.0 |