3
$\begingroup$

Gödel's Completeness Theorem shows that first-order logic is (semantically) complete, namely, provability and validity coincide.

Gödel's Incompleteness Theorem shows that there are theories where certain true (in the intended interpretation) formulas are undecidable, and thus such theory is (syntactically) incomplete. So there must exist models of such a theory, where the aforementioned formula is false.

Are there systematic ways to construct such a model, given the theory and formula?

EDIT: Sorry for the confusion. Perhaps a better way to frame the question is: what are the/some known systematic ways to construct such a model, given the theory and formula?

Improve this question
$\endgroup$
10
  • $\begingroup$ 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. $\endgroup$
    – Punga
    Commented May 9, 2022 at 19:36
  • 5
    $\begingroup$ 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? $\endgroup$
    – Burak
    Commented May 9, 2022 at 21:17
  • 1
    $\begingroup$ 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. $\endgroup$
    – jeq
    Commented May 9, 2022 at 21:55
  • $\begingroup$ @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. $\endgroup$
    – user213800
    Commented May 10, 2022 at 5:23
  • $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Commented May 11, 2022 at 6:08

1 Answer 1

Reset to default
2
$\begingroup$

Yes, check out the Paris-Harrington theorem's use of indicators as one way to do this for a specific kind of Ramsey theorish combinatorial claim. It's kinda a tough slog but it's a really explicit construction of a model of PA which makes a true (in N) combinatorial claim false.

Generally speaking, however, there is no general constructive method to produce such models. However, I believe the indicator method from the Paris-Harrington theorem can be extended to work for cases where the issue is the provable totality of functions with a certain rate of growth.

Improve this answer
$\endgroup$

You must log in to answer this question.