Question on Godel completeness theorem

Question

Let $T$ be a formal theory. Suppose that $Con(T)$. Does it Godel completeness theorem confirms that the corresponding model $M_{T}$ of the $T$ really exists?

Answer 1

(For simplicity, I assume all languages and theories are countable.)

I'm not sure what "really exists" means; Godel's theorem says that a model of $T$ exists whenever $T$ is consistent.

If by "really exists" you mean "exists in some constructive sense," then the answer is: sort of. There are consistent, computable theories with no computable model (e.g., PA + a nonstandard integer - see Tennenbaum's Theorem; or $ZF$ (and, I suspect, every natural set theory) - see Is there a computable model of ZFC?), but every consistent theory $T$ does have a model which is low with respect to $T$; in particular, such a model is computable from $T'$, the Turing jump of $T$, which is nicely definable. If you accept operations as complicated as Separation and Replacement, then you should certainly accept the existence of models of consistent theories (unless your underlying logic is not classical, in which case I have nothing useful to say, although Andrej Bauer probably does).

Let me elaborate a bit on why having computationally simple models is relevant. It's not just that such models are "less complicated" than standard set-theoretic constructions, as I state above; it's that we don't even need to talk about set theory, at all, to get them! The models in question are uniformly computable in the jump of $T$; that is, there is a single $e\in\omega$ such that for all theories $T$, either $\Phi_e^{T'}$ codes a model of $T$, or $\Phi_e^{T'}$ codes a proof of $\exists x(x\not=x)$ from $T$. So if we believe that jumps of arbitrary sets of natural numbers "really exist" - that is, if we believe that statements of the form $\exists n\phi(n)$ are meaningful whenever $\phi$ is meaningful - then we have to believe that consistent theories have models. It is definitely possible to be skeptical of the meaningfulness of arbitrary arithmetic statements, but at that level of skepticism it seems like classical logic is the "wrong" tool, so all the questions/theorems look different anyways. I'm pushing this point because I suspect your question is coming from a skepticism towards set theory - which I consider entirely healthy! - and I want to argue that no set theory is needed to believe in models.

Please let me know if this addresses your question. I would suggest, though, that you explain a bit what you mean.

Answer 2

I do not know from what angle you're coming, but "really exist" might mean "exists constructively". In this case you should look at Stefano Berardi, Silvio Valentini: Krivine's intuitionistic proof of classical completeness (for countable languages) Ann. Pure Appl. Logic 129(1-3): 93-106 (2004). Even though existence of the usual Tarski models for consistent theories cannot be proved construtively, one can still prove a slightly weaker version of completeness.