Hilbert-Bernays theorem

Question

As far as I understand, the following result is called the Hilbert-Bernays theorem (is that correct?):

If a (first-order) formal theory $T$ is consistent, then it has a model.

Can anybody give me a reference, preferrably with a proof of this fact?

EDIT. Gentlemen (and ladies), before you close this question:

is it possible that this special proposition has its own name, different from "the completeness theorem"?

C.Smorynski in "Handbook of Mathematical Logic" (edited by Jon Barwise) calls a similar statement "the Hilbert-Bernays theorem" (Theorem 6.1.1 in volume 4), that is why I used this name.

Can anybody explain me the difference between the result that Smorynski mentions (the "true Hilbert-Bernays theorem") and what I initially asked about? And if possible give me a reference where the Hilbert-Bernays theorem is proved.

Answer 1

This is called the "completeness theorem". P. T. Johnstone's "Notes on logic and set theory" proves this in Chapter 3. I liked this book for having full details while still being quite short.

Answer 2

1. It is not in general true [as the question assumed in its original form] that if a formal theory $T$ is consistent, then it has a model. (For example, take second-order Peano Arithmetic extended with a constant $c$ governed by the axioms $c \neq 0$, $c \neq S0$, $c \neq S00$, etc. This is consistent but has no model -- as nicely explained in this answer by Henning Makholm)
2. It is a theorem that if a first-order theory is consistent, then it has a model. This is a version of the completeness theorem for first-order logic that, famously, is due ultimately to Kurt Gödel.
3. Any standard math logic text will prove this: but there's a good version in Leary/Kristiansen, A Friendly Introduction to Mathematical Logic, which is freely available through the friendly generosity of the authors.

Answer 3

We can see S.C.Kleene, Introduction to Metamathematics (1952), §72. Gödel's completeness theorem (page 389-on) :

Theorem 34C. If a predicate letter formula $F$ is irrefutable (i.e. if $¬F$ is unprovable) in the predicate calculus, then $F$ is satisfiable in the domain of the natural numbers. (Gödel’s completeness theorem for the predicate calculus, 1930.)

And see page 395 :

Theorem 36. The addition to the postulate list for the predicate calculus of an unprovable predicate letter formula $G$ for use as an axiom schema would cause the number-theoretic system as based on the predicate calculus and Postulate Group B (§19 [first-order Peano's axioms]) to become $ω$-inconsistent. (In fact, a certain formula would become refutable which expresses a true proposition of the form $(y)D(y)$ where $D(y)$ is an effectively decidable predicate.) (Hilbert-Bernays completeness theorem, 1939.)

The "usual" modern formulation : "every consistent f-o theory has a model", is later; the source is probably A.Tarski and his US school.

See Leon Henkin, The Completeness of the First-Order Functional Calculus, JSL (1949), [doi:10.2307/2267044}(https://doi.org/10.2307/2267044), jstor :

THEOREM. If $\Lambda$ is a set of formulas in which no member has any occurrence of a free individual variable, and if $\Lambda$ is consistent, then $\Lambda$ is simultaneously satisfiable in a domain of individuals having the same cardinal number as the set of primitive symbols of [the system].

See Henkin's paper (1st page) : "Although several proofs have been published showing the completeness of the propositional calculus (cf. Quine), for the first-order functional calculus only the original completeness proof of Gödel (1930) and a variant due to Hilbert and Bernays [Grundlagen der Mathematik, vol II, 1939] have appeared."

For sure, we can find it into Abraham Robinson, Introduction to Model Theory and the Metamathematics of Algebra (1963, 1st ed.1951 as On the Metamathematics of Algebra), page 12 :

THEOREM (EXTENDED COMPLETENESS THEOREM OF THE LOWER PREDICATE CALCULUS). Every consistent set of sentences $K$ in a language $L$ [the lower predicate calculus] possesses a model.