Is the concept of a "model" in logic grounded?

Question

The concept of a "model" in logic has always seemed a little suspicious to me - as it implies statements that are not deducible from the axioms, yet are true anyway. What could "true" really mean, if we lack a procedure for distinguishing truth from falsehood? It would seem more natural to just say that unprovable statements are indeterminate.

I suspect that a model is better viewed as just the provable results of a different, "larger" logic. Even the human brain can be considered to implement such a "logic." For instance, we say a Godel sentence is true because it can be derived in our brain-logic, though it can't be derived in first-order logic. If neither a claim nor its negation is derivable using the implicit logic of the human brain, I don't see how it could be meaningful to call it "true" or "false."

So when we say M ⊨ B (model M satisfies result B), the idea is that we could interpret this as ⊢ₘ B for some axiomatic logic m, where m is "larger" than the logic we were dealing with before. ⊢ₘ would be different from ⊢ but still about syntactic consequence.

Is there a name for this position? ("model non-realism"?) Do any results of logic make it untenable?

Answer 1

You seem to be asking a specific question about model theory, and a more general question about the relationship between truth and provability, and whether truth outruns provability.

Model theory is one way of expressing the relationship between syntax and semantics. Ultimately, model theory justifies its existence by how useful it is. It has proved to be a useful way to understand the foundations of mathematics (though not the only way) and it has found application in philosophical logic. That said, a few logicians reject the syntactic/semantic distinction, or prefer to couch it in different terms, e.g. using game theory to express the semantics.

In mathematics, model theory has been able to demonstrate results about the properties and limitations of axiom systems. Some significant results are:

• That first order logic is semantically complete and second order logic is not (in standard semantics).
• That first order logic is compact and second order logic is not.
• That the set of semantic truths of arithmetic is not recursively enumerable (assuming arithmetic is consistent).
• That a theory of arithmetic can have non-standard interpretations.
• That if a countable first order theory has any models, it has countable models, and that if it has countable models, it has models of any higher cardinality.

The issue of whether truth in mathematics outruns provability is more an issue in the philosophy of mathematics. Gödel was a realist about mathematics and he interpreted his incompleteness theorems as showing that there are statements in mathematics that are true but unprovable. An alternative approach, taken by Brouwer, is to hold that mathematics is essentially about proving things, and that it does not make sense to speak of mathematical truth beyond what is provable. This approach is called intuitionism and it leads to a substantially different kind of mathematics. Many theorems of classical mathematics that mathematicians are accustomed to relying on are not theorems of intuitionistic mathematics. In particular, since there are pairs of propositions P, ¬P such that neither is provable, intuitionistic logic must dispense with bivalence and with the law of excluded middle and hold that in such cases, neither P nor ¬P is true. Another rule that intuitionistic logic lacks is the classical rule that ¬(∀x)Φx entails (∃x)¬Φx. The logic that remains is a constructive logic that can be interpreted as a logic of warranted assertability.

When we turn from mathematics to speaking of everyday things in philosophy, the fact that truth outruns proof or verification is more obvious. All kinds of things are beyond our ability to demonstrate, such as statements about the past, scientific conjectures that we don't know how to test, or predictions about the future when there might be nobody around to observe them. A fundamental feature of realism is that it involves accepting that whether some proposition is true is independent of whether I, or anybody, believes it. Or even of whether there is any way to verify it at all. Did two millimetres of rain fall on Land's End, England, on March 1st of the year 10 BCE? Nobody knows and almost certainly nobody ever will. There is no record, no evidence, and no scientific basis on which to calculate it. But if one is a realist about the external world, and about its past, then one accepts that such a thing is either true or it is false, independently of our ability to verify it.

To describe the brain as a proof system is rather dubious, and even if it were, it is not clear how it would be relevant to the concept of truth. The point of beliefs, or good beliefs at least, is that they aim at being true. If a belief is simply what a brain proves, and if there is no truth beyond provability, then there is no elbow room to say that a belief is false. An analogy might be with the result of a running a computer program: even if the computation is performed correctly, it will always make sense to ask of the output, is it actually true?

Even if you propose to appeal to some more complex structure to account for truth, such as what is believed by a majority of people in a community, or what is believed by a subset of people who are more successful at reproducing than others, it will still always make sense to say: Yes, these beliefs have that property, but are they really true?

And when we come to logic, there will always be the question of which logic we are to use. There are logical monists who disagree about which is the correct logic, and there are logical pluralists who use several. And even within a family of logics, there are different ways of extending them. If logical truth is not distinct from provability then what does it mean to say that one logic is correct and another not, or that one logic applies to some domain of enquiry and another logic to a different one? Typically it makes more sense to say that a logic is correct if it agrees with some intended semantics, and that our knowledge of logic progresses by constructing formal systems that agree with an intended semantics. The semantics is always of primary concern, and that is where the model theory comes in.

The position of holding that there is no truth beyond what is verifiable or knowable is simply anti-realism. One can be a realist about some domains and not others, e.g. a realist about the external world and about the past, but an anti-realist about mathematics and morality. Intuitionism is a form of anti-realism.

Answer 2

First, I'm going to answer this with a question: How would you know that the axioms of your formal deductive system capture all that needs to be captured so that your concept of (deductive) truth is all that matters to (some informal notion) of truth as a concept?

In other words (assuming the deductive method is all that there is to "truth"), how do you know your axioms are grounded and "useful enough"? (And the same can be said about the inference rules, really.) I.e. what is the (ultimate) point of defining truth in a syntactic way (as deriving from some axioms by some rules)?

(I'll also note here that one of the reasons why relevance logic falls on deaf ears with [most] mathematicians is that they are very discerning about which axioms to admit to begin with. If they were not so discerning and any random mathematician you picked would readily accept that "Trump is president and Trump is not president" is an axiom... they would have to worry about relevance in entailment [not] "blowing up" mathematics. But since mathematicians are very discerning about their axioms [see e.g. how the axiom of constructibility has been debated], they can be a bit more "maximalist" about the rules of the deductive system that founds mathematics.)

Second, assuming ZFC, it's actually quite trivial to define truth (semantically) in an algebraic model (itself a ZFC-defined structure--an algebra in the sense/definition of universal algebra). This is even "grounded" enough that you can define a notion of logical consequence that way; see for instance how the definition a logic in the abstract algebraic logic (AAL) programme includes both syntactically and model-defined logics. (Font's 2016 book is a good read here.) For example, one can define some logics this way that have no known axiomatization. (IIRC, Medvedev's "logic of problems" was the example given.)

Yes, there is a subtle meta-logical point here: we assume FOL (e.g. by Hilbert-style axiom-schemas), in which we build ZFC (with some more axioms) and in which we then (can) "more generally" define what a logic (with some properties) means... and the latter notion can actually encompass not only non-classical (propositional) logics but also allows one to define (propositional) logics merely by their (algebraic) models!

(N.B. I once asked a mathematician--Carl Mummert, if I recall that correctly-- if the (various) axioms of non-well-founded set theory seem "fishy" because they rely on a notion of [pointed] graphs. But how do you define graphs if you don't yet have a notion of set, etc.? His answer was, again if I recall correctly, was that one needs to assume that notion of graph is built in another "mini-language" etc.)

But to get back to your question...

What could "true" really mean, if we lack a procedure for distinguishing truth from falsehood? [...] I suspect that a model is better viewed as just the provable results of a different, "larger" logic. For instance, we say a Godel sentence is true because it can be derived in our brain-logic [...]

Actually that can be made more precise:

Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's completeness theorem (Franzén 2005, p. 135). That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false.

(Also discussed in https://plato.stanford.edu/entries/goedel-incompleteness/#IncNonStaMod)

But surely the fact that we have an "intended interpretation" of arithmetic (when building a system like PA) does say something about us (if not about the world).

Also, although a bit "opinionated", I think the following take (by Raattkainen) (cited by Wikipedia) on misinterpretations of Godel's result is useful to recall here because it pertains to your saying that "we say a Godel sentence is true because it can be derived in our brain-logic":

The structure of Godel's proof is, very roughly, the following : Assume that the formal system F is consistent (otherwise it proves, by elementary logic, every sentence and is trivially complete). By Godel's self-reference lemma, one can then construct a sentence GF that is independent of F (i.e. neither provable nor refutable in F). Thus F is incomplete. So far so good. Yet how then can one conclude that GF is true?

Assuming that the formalized provability predicate used is normal, one can prove, even inside F, that GF is true if and only if F is consistent, although neither side of the equivalence can be proved in F. Therefore, the truth of the sentence GF is already implicitly assumed in the beginning of the proof, in the form of the assumption that F is consistent.

If it nevertheless turns out that F is inconsistent, one has to conclude that GF is, after all, false — and provable in F, because every sentence is. The proof also goes through for a theory that is in fact inconsistent. An amusing real historical example is Quine's original version of his system ML (Quine 1940). At the end of the book, Quine presented a proof of Godel's theorem for this system. But ML was later shown to be inconsistent by Rosser. Hence the Godel sentence GML was actually false, whatever one's intuitions were.

[...]

An unqualified anti-mechanist conclusion was drawn from the incompleteness theorems in a much read popular exposition, Godel's Theorem, by Nagel and Newman (1958). Shortly afterwards, J.R. Lucas (1961) famously proclaimed that Godel's incompleteness theorem "proves that Mechanism is false, that is, that minds cannot be explained as machines". He stated that "given any machine which is consistent and capable of doing simple arithmetic, there is a formula it is incapable of producing as being true ...but which we can see to be true". More recently, very similar claims have been put forward by Roger Penrose (1990,1994).

The basic error of such an argument is actually rather simply pointed out. This objection goes back to Putnam 1960; see also Boolos 1967. The argument assumes that for any formalized system, or a finite machine, there exists the Godel sentence (saying that it is not provable in that system) which is unprovable in that system, but which the human mind can see to be true. Yet Godel's theorem has in reality the conditional form, and the alleged truth of the Godel sentence of a system depends on the assumption of the consistency of the system. That is, all that Godel's theorem allows us humans to prove with mathematical certainty, of an arbitrary given formalized theory F, is: F is consistent => GF.

The anti-mechanists argument thus also requires that the human mind can always see whether or not the formalized theory in question is consistent. However, this is highly implausible. After all, one should keep in mind that even such distinguished logicians as Frege, Curry, Church, Quine, Rosser and Martin-Lof have seriously proposed mathematical theories that have later turned out to be inconsistent.

---

As for these parts of the question:

What could "true" really mean, if we lack a procedure for distinguishing truth from falsehood? [...] If neither a claim nor its negation is derivable using the implicit logic of the human brain, I don't see how it could be meaningful to call it "true" or "false."

Well, I'm not sure what to make of the "implicit logic of the human brain" part, or exactly what you mean by "procedure" in there, but if (as hinted in the comments) your concern is that proofs and models need a constructive approach; intuitionism has its own approach(es) to model theory; one could say perhaps that it has too many...

Intuitionistic systems have inspired a variety of interpretations, including [...] formulas-as-types, Kleene’s recursive realizabilities [...] Of all these interpretations Kripke’s [1965] possible-world semantics, with respect to which intuitionistic predicate logic is complete and consistent, most resembles classical model theory. Recursive realizability interpretations, on the other hand, attempt to effectively implement the B-H-K explanation of intuitionistic truth.

That SEP article also details Kleene’s approach to realizability via partial recursive function (which Wikipedia also covers.)

There's yet another SEP article that more specifically deals with constructive set theories where the implications of model approaches are discussed in more detail. In particular, that page does a good job of contrasting IZF which only restrict the logic and CZF which has a "double restriction" approach to what sets are constructible as well.

Finally, regarding the formulas-as-types interpretation, which has yielded ITT (Intuitionistic Type Theory)... that has also been given various models, both classical e.g. in ZF (or CZF) and realizable. To quote an (explanatory) bit on that, again from (a 3rd) SEP article...

The set-theoretic model can be criticized on the grounds that it models the type of functions as the set of all set-theoretic functions, in spite of the fact that a function in type theory is always computable, whereas a set-theoretic function may not be.

To remedy this problem one can instead construct a realizability model whereby one starts with a set of realizers. One can here follow Kleene’s numerical realizability closely where functions are realized by codes for Turing machines. Or alternatively, one can let realizers be terms in a lambda calculus or combinatory logic possibly extended with appropriate constants. Types are then represented by sets of realizers, or often as partial equivalence relations on the set of realizers. A partial equivalence relation is a convenient way to represent a type with a notion of “equality” on it.

There are many variations on the theme of realizability model. Some such models tacitly assume set theory as the metatheory (Aczel 1980, Beeson 1985), whereas others explictly assume a constructive metatheory (Smith 1984).

So, if your worry is that e.g. the definition of a function in a classical model is non-procedural/non-constructive... then you have to use a constructive meta-theory as well for models/interpretations.