Logical consequence vs. "proof" in a model

Question

I'm self-studying first-order logic as a foundation of mathematics and struggling to understand what's the point of the symbolic system. In first-order logic, a formula is a "logical consequence" of axioms if it is true in each model that satisfies the axioms. This definition of the terminology "logical consequence" looks very odd to me.

If a model is something in real physical world, truth is definite as a physical reality that can be in princple just observed. However, in my opinion, mathematics does not physically exist. It is a construction using natural "language". In my naive mind, "truth" in a mathematical model is nothing but a consequence of a "proof" based on the definitions of the related mathematical objects and "logic" in a natural language. If there is a proof of a statement in a natural language, the statement is true. If there is a proof on the negation of the statement in the natural language, the statement is false. In this view, the only difference between a symbolic theory (e.g., first-order theory) and a mathematical model is underlying langauges.

Of course, one can argue that mathematics is an abtraction of some part of the real world or motivated by real world, but anyway it should be finally expressed in a natural language. Otherwise we could not make much advance in mathematics.

If a symbolic language has sufficiently expressive power, any "mathematical" statements in a natural language could be appropriately expressed in the symbolic language and vice versa. So we don't need to distinguish the symbolic theory and a model. In this view, when we discuss mathematics, the distinction between syntax and semantic is meaningless, and defining "logical consequence" using truth in a model looks like a tautology.

However, in some reason, if we have to use a symbolic langauge which is not sufficiently expressive (or one may insist that symbolic langauges cannot be as expressive as natural languages inherently), the forementioned definition of "logical consequence" may make sense. In this case, the axioms expressed in the symbolic langauge cannot completely capture the essence of the intended model which is defined in a natural langauge. Only part of the intended model is captured by the symbolic theory and so there could be another model (again defined in the natural language) that satisfies the same axioms.

Does this view make sense? Any recommendation on materials to study would be also helpful.

Answer 1

In logic there is a difference between a proof in the system typically denoted as $\Gamma\vdash\varphi$ and a proof in a model: $\Gamma\vDash\varphi$. What you seem to be referring to is the symbolic system which has no "meaning". We have symbols: $p_1,p_2,...,p_n$ and connectives: $\wedge,\vee,\rightarrow$ but they don't actually mean anything because as you pointed out the symbols are arbitrary and a human-construct. However, if we give them an interpretation we can use the symbolic system to reason about the real world. It is easy to show that $\varphi(x),\forall y(\varphi(y)\rightarrow\psi(y))\vdash\psi(x)$ holds in FOL (symbolically). But now we can give these symbols meaning through an interpretation. For instance: Socrates is a man, all men are mortal, therefore Socrates is mortal can be formalized as $Man(s),\forall x.Man(x)\rightarrow Mortal(x)\therefore Mortal(s)$. Here, this Socrates syllogism is proven in the model and it is true in real life, but under other interpretations the symbolic proof might be false.

This is what is meant when a logical system is Sound and Complete. These soundness and completeness proofs want to prove that any statement $\Gamma\vdash\varphi$ implies $\Gamma\vDash\varphi$ and that any statement $\Gamma\vDash\varphi$ implies $\Gamma\vdash\varphi$. This means that all the valid statements ($\vdash$) are the true statements ($\vDash$) and vice versa.

Your statement that the difference between a symbolic theory and a model is the underlying language is not totally correct, because the difference is the interpretation. It is true that in FOL it really wouldn't matter if you did not distinguish between the model and symbolic system however this is only because it has been proven to be so (FOL Completeness). Other logics do not always have this property and specifically in more advanced modal logics that "get invented", a common task is to prove that the logics are sound and complete. It is very easy to develop a group of symbols, axioms, and special operations, but it is not trivial to prove that your system only proves true things.

Answer 2

Your conception of a model seems somewhat off, and I think that's where your confusion comes from.

A structure for a first-order language consists of a domain of discourse specifying which objects are being talked about, and an interpretation function which gives a meaning to the non-logical symbols of the formal language by mapping the individual symbols, function symbols and predicate symbols to objects, functions and relations over the domain. A structure is thus not something separate from the formal symbolic language: Instead, its role is precisely to make a link between the symbols and the real world.

A model of a theory is a structure which satisfies all the axioms of the theory, i.e., a model is a way of mapping the symbols to the real world that makes the axioms true.

For instance, the alphabet of the langauge of Peano arithmetic consists of the following non-logical symbols: the individual symbol $\text{zero}$, the 1-place function symbol $\text{succ}$ and the 2-place function symbols $\text{plus}$ and $\text{times}$. We can then sentences in this language such as $\forall x. \text{plus}(x, \text{zero}) = x$.
(Normally one would choose mathematical symbols $0, +, \cdot$ instead of natural language words for the non-logical symbols and allow for infix notation, so that the above would be written as $\forall x . x+0 = x$; here I'm deliberately using a more clumsy notation to highlight the difference between formal symbols and their interpretation.)

A structure of this language could be $$\mathcal{N} = \langle \mathbb{N}, [\text{zero} \mapsto 0, \text{succ} \mapsto \{ \langle 0, 1 \rangle, \langle 1, 2 \rangle, \ldots, \langle 17, 18, \rangle, \ldots,\}, \text{plus} \mapsto \{\langle 0, 0, 0 \rangle, \langle 0, 1, 1 \rangle, \ldots, \langle 123, 5, 128 \rangle, \ldots\}, \text{times} \mapsto \{\langle 0, 0, 0 \rangle, \langle 0, 1, 0 \rangle, \ldots, \langle 12, 4, 48 \rangle, \ldots\}] \rangle $$

This model limits the meaning of "everything" to comprise the natural numbers, and interprets the individual symbol $\text{zero}$ as the number $0$, the 1-place function symbol $\text{succ}$ as the successor function $\_ + 1$ over natural numbers, and the 2-place function symbols $\text{plus}$ and $\text{times}$ as addition and multiplication, respectively.

This structure is the standard interpretation of Peano arithmetic, because it gives the intended interpretation of the formal symbols: When we write such things as $\forall x. \text{plus}(x, \text{zero}) = x$, what we intend it to mean is "$0 + 0 = 0$ and $1 + 0 = 1$ and $\ldots$ and $123 + 0 = 123$ and $\ldots$".

$\mathcal{N}$ satisfies all axioms of PA -- after all, the axioms were constructed precisely to reflect true facts about the natural numbers, i.e. this intended interpretation of the symbols. $\mathcal{N}$ is called the standard model of PA.

But, in principle, there is nothing stopping us from defining a structure like $$\text{blargh} = \langle \mathbb{Q}, [\text{zero} \mapsto 52, \text{succ} \mapsto \{ \langle 0, -1 \rangle, \langle 1, 0 \rangle, \ldots, \langle 17, 16, \rangle, \ldots,\}, \text{plus} \mapsto \{\langle 0, 0, 0 \rangle, \langle 0, 1, 0 \rangle, \ldots, \langle 123, 5, 615 \rangle, \ldots\}, \text{times} \mapsto \{\langle 0, 0, -23 \rangle, \langle 0, 1, \frac{1}{4} \rangle, \ldots, \langle 12, 4, 10004\frac{1}{2}, \rangle, \ldots\}] \rangle $$

This would render the same symbolic sentence $\forall x. \text{plus}(x, \text{zero}) = x$ to mean "$0 \cdot 52 = 0$ and $\frac{1}{2} \cdot 52 = \frac{1}{2}$ and $123 \cdot 52 = 123$" and $\ldots$", because we just interpreted "every" as the rationals, "$\text{zero}$" as 52 and "$\text{plus}$" as multiplication. This is of course not the intended meaning of the formal symbols, but it is a perfectly well-defined structure.

This structure does not satisfy the axioms of the theory and therefore is not a model of Peano arithmetic, because of course $123 \cdot 52$ does not equal $123$. If we give the symbols of the formal language a strange meaning, the laws formulated in that language with these symbols may no longer match with the facts about the real world; a structure with a non-standard interpretation is often not a model of the theory and not the kind of thing we're typically interested in.

But there can also exist structures with non-standard interpretations of the language that are indeed models of the theory, and this is the case for PA,, i.e., there exist structures other than $\mathcal{N}$ given above that still obey all the laws about natural numbers. These are called non-standard models of the theory. It's a bit complicated what these look like, but they exist.

Truth of a symbolic sentence is always relative to a structure. Technically speaking, it does not make sense to say a formula is true without specifying where it is supposed to be true. That said, we do often do find ourselves saying such things, and what we mean by saying that a sentence like $\forall x. x + 0 = 0$ is true is that it is true in the standard model. This is common practice, but it is important to bear in mind that this is actually just a convenient abbreviation and behind the scenes, we are always talking about truth in one specific structure.

For mathematical theories, this default structure in which we intend statements to be true will be the respective standard model of the theory, and for symbols in non-mathematical contexts like $\forall x (\text{man}(x) \to \text{mortal})$ we mean that the sentence is true in the real world and under the intended interpretation of the symbols, i.e., where $\text{man}$ is taken to mean "humans" and $\text{mortal}$ refers to all individuals who will eventually die. But again, as far as logic is concerned, there is nothing stopping us from interpreting $\text{man}$ as comprising the politicians in our world and $\text{mortal}$ to mean being a pig. In this structure, $\forall x (\text{man}(x) \to \text{mortal})$ is not true, because for example Joe Biden is not a pig.

A statement is true in one particular structure, usually meaning the standard model.

A statement is valid (or a logical consequence holds, also called universal truth) iff it is true in all models of the theory, i.e. in all structures which satisfy the axioms.

So note that "true" is not the same as "valid". A statement may be true one structure but false in others and therefore not valid.

Both truth and validity are "semantic" notions in the sense that they are about interpretations of the symbols.

A statement is provable iff there is a formal proof in some syntactic proof system like Hilbert-style calculus or natural deduction. When considering provability in a theory, typically such a proof will proceed by repeatedly applying modus ponens on the axioms and some assumptions to yield new statements until eventually the desired conclusion is reached. "Syntactic proof system" here means a set of rules for manipulating symbols like "If you have $A \to B$ written on one line and $A$ on another line, then you may write $B$ on a line below that". It is "syntactic" in the sense that it relies purely on rearranging symbols, without making explicit reference to "semantic" notions such as truth or models and interpretations.

In FOL (more precisely, for a proof system like the Hilbert system described above), the "semantic" notion of being valid (= true under every interpretation of the symbols that satisfies the axioms of the theory) and the syntactic notion of being provable (= derivable by some rule-governed manipulations of symbols on the axioms) happen to be in line with each other. The calculus for FOL is sound, meaning that every statement that is provable is also valid, i.o.w., the proof system doesn't prove nonsense, the statements that can be formally proved are actually true under any possible interpretation that is consistent with the axioms. The calculus for FOL is also complete, meaning that every statement that is valid is also provable, i.e., the proof apparatus is able to capture all sentences that are universally true throughout the models of the theory, there won't be any valid statements that we can't formally prove. This is a convenient result, but by no means trivial; it has to be shown that the proof system actually works this way, and there are many proof systems for logics in which this is not the case.

But a theory may also be incomplete in a different notion of completeness than the one above: Gödel's first incompleteness states that there are statements that are true (in the natural numbers) but not formally provable in PA. So while every valid statement is provable, not every true (in the standard model) statement is. This implies the existence of non-standard models: There is a sentence that must be false in some model (since if it were universally true, it would also be provable) that is not the standard model (because there the statement is true), so non-standard interpretations that are also models of the theory exist.

TL;DR:

• A model is not a notion detached from the symbolic theory; rather, it is a way of interpreting the symbols in the real world in such a way that the axioms are true.
• "true" is not the same as "valid". Truth is relative to a specific structure, and usually means the standard models with the intended interpretation of the symbols, but non-standard models in which different statements hold may exist.
• In FOL, validity and provability happen to coincide; every statement that is valid is also provable and vice versa.
• Truth and provability do not coincide; not every statement that is true (under the intended interpretation of the symbols) is also provable.

Answer 3

Logic has a special place at the foundations of math, but understanding the basics of models is easier if we take a step back and temporarily assume that logic isn't foundational but is just another thing that we study by throwing math at it. Suppose logic is just a bunch of symbols with some rules that we might try to describe with "ordinary mathematics", similarly to how we might want to describe a programming language or a cellular automaton.

That being said, it's important to keep in mind what a model is.

A model is a pair consisting of a set of individuals and a mapping from non-logical symbols to sets. The set theory that you use is almost always ZFC. ZFC itself is a first-order theory with one predicate symbol $\in$, but let's ignore that for now. It's a theory that we have in the background that we can use as a building material.

In the interest of clarity, I am going to be very explicit about issues that arise when encoding structures as sets.

Here's an example. Let's talk about Abelian groups. We decide to use three logical symbols $1$ for the identity element $\cdot$ for the group operation and $^{-1}$ for the inverse.

For intuition, we are looking at $\mathbb{Z}/3\mathbb{Z}$.

Let make our domain, $\{0, 1, 2\}$. We will use the Zermelo ordinals as the natural numbers, i.e. $0$ is $\varnothing$, $1$ is $\{0\}$ and $2$ is $\{1\}$.

So, we have our domain.

Here is the interpretation of $^{-1}$, $\{ (0, 0), (1, 2), (2, 1) \}$. As expected, the inverse sends everything to its additive inverse.

The construction $(\cdots)$ is a tuple. It can be defined in terms of sets as follows, using a Kuratowski pair internally.

$$ (a_1, a_2, \cdots a_n) = \bigg\{ \{\{1\}, \{1, a_1\}\} \bigg\} \cup \bigg\{ \{\{2\}, \{2, a_2\} \} \bigg\} \cup \cdots \cup \bigg\{ \{\{n\}, \{n, a_n\}\} \bigg\} $$

Here is the interpretation of $\cdot$.

$$ \{ (0, 0, 0), (0, 1, 1), (0, 2, 2), (1, 0, 1), (1, 1, 2), (1, 2, 0), (2, 0, 2), (2, 1, 0), (2, 2, 1) \} $$

In this Abelian group, the symbol is $\cdot$, but in the model, the group operation feels very additiony. This mismatch is intentional. The choice of non-logical symbol is arbitrary. The rules that it has to follow and the interpretations are important.

It's also important to note that a given well-formed formula in first order logic using the language of groups can be true or false with respect to our model of $\mathbb{Z}/3 \mathbb{Z}$ without consulting the Abelian group axioms at all.

This gives us a very powerful technique for talking about semantics. We pick a well-understood theory, ZFC, build structures in it that satisfy our rules, and then look at those structures.