In what sense Fraissean view point shows Model Theory can be done without any formal syntax and deduction rule?

Question

In this post I want to look at an issue I was in doubt when looking at the comment of F. G. Dorais in the post In model theory, does compactness easily imply completeness? F. G. Dorais remark was:

Blockquote ...The first, which comes through rather clearly, is that Model Theory could ultimately be done without any formal syntax and deduction rules...

I think F. G. Dorais was talking about Fraisse's development of model theory via back and forth. It is, however, not clear to me that this is more free from syntax and deduction rule than the traditional one in a meaningful way.

I think Fraissen view does show that Model Theory could be done without a specific choice of syntax. But it seems unreasonable to think that the traditional model theorists would believe that a specific choice of syntax does matter.

The main question I want to ask:

Is there any difference between Fraissean point of view to traditional point of view BEYOND switching from formal syntax and deduction rule to its informal counter part?

It is not immediately clear to me that the Fraissean did anything more than doing so.

If this is the case then there is nothing genuine new about Fraissean point of view than the traditional one. For example, there seems to be no fundamental difference between writing $ N \vDash S0+S0=SS0 $ and speaking out loud "in $N$, one plus one is equal to two". In both cases, we use language which are ultimately meaningless. There is no more meaning in the utterance of "one" than writing $S0$. (If a parrot shout “one plus one is equal to two”, his statement would have no meaning).

In both cases meaning is given by the interpretations. The only difference is the interpretation in the case of "one" is more familiar than in the case of $S0$. This difference has nothing to deal with the subject matter of mathematics. Likewise, there is no meaningful difference between " there exist .. in M" and $M \vDash \exists ...$.

Answer 1

After your answer, I think I understand better where you see a problem. I don't think you fully appreciate the way of interpreting formulas from Fraïssé's point of view. For simplicity, I will follow your lead and stick with the case of a language with just one relation symbol. It's not hard to generalize, but that would introduce some unnecessary tedium.

First, think about how you would actually define a formula in the Fraïssean style. What you have are the $n$-types (${\sim_\omega}$-equivalence classes of $n$-tuples). There is a (Hausdorff, in fact, zero-dimensional) topology on the space $S_n$ of $n$-types which is induced by the ${\sim_p}$-equivalences. A good way to think about this topology is to think of the set $S_n$ of $n$-types as the inverse limit of the ${\sim_p}$-quotients, so the basic clopen sets of the topology on $S_n$ correspond to ${\sim_p}$-equivalence classes for some $p < \omega$.

Formulas can then be viewed as clopen sets in $S_n$. The meaning of ${\land}$, ${\lor}$, ${\lnot}$, is clear since clopen sets form a Boolean algebra. Before thinking about quantifiers, let's see what it means to satisfy a formula $\phi$, i.e. a clopen set in $S_n$. Let's take a structure $(M,R)$ and pick an $n$-tuple $\bar{a}$ from $M$. Then $(M,R,\bar{a})$ has a specific type, which may or may not belong to the clopen set $\phi$ of $S_n$. To (ab)use classical symbolism, we can write $(M,R) \vDash \phi(\bar{a})$ when the type of $(M,R,\bar{a})$ does belong to $\phi$. This gives the usual interpretation of ${\land}$, ${\lor}$, ${\lnot}$.

Returning to quantifiers, the existential quantifier is, in a certain sense, the projection $\exists x_{n+1}:S_{n+1} \to S_n$ which simply forgets the last coordinate (suggested by the dummy variable symbol $x_{n+1}$). More precisely, if $\psi$ is a clopen set in $S_{n+1}$, then the set $\exists x_{n+1}\psi$ of $n$-types that extend to an $(n+1)$-type in $\psi$ is a well-defined subset of $S_n$. The fact that this is a clopen set is however not immediately obvious, nor is the fact that this is correct. (It's easier to think about this when $\psi$ is a basic clopen set, i.e. a ${\sim_p}$-equivalence class for some $p < \omega$. Working through the definitions, you see that $\exists x_{n+1}\psi$ is easy to understand in terms of ${\sim_{p+1}}$-equivalence. It's also easier to see that this is indeed correct.)

Now that we understand how to view formulas from Fraïssé's point of view. How does compactness enter? The Compactness Theorem, in Fraïssé's view, simply says that the spaces $S_n$ are all compact. (Or, in a more restricted sense, that $S_0$ is compact.) In our case, the fact that the spaces $S_n$ are compact is obvious, since they are inverse limits of finite spaces. However, this fact uses the cheat that we're only considering a language with only one relation symbol. For the general case, the ultrafilter construction reduces the problem to the case where the language is finite. (This works well in a relational language with constants, to handle functions you need some magic tricks.)

The point here is that you prove that the spaces $S_n$ are compact directly, you don't need to know that clopen sets are actually formulas. The Classical Compactness Theorem then follows from the simple observation that formulas are closed sets. The other big theorems follow in the same way. For example, the Omitting Types Theorem follows from the fact that the Baire Category Theorem holds for compact spaces, again without explicit mention formulas.

What about the Completeness Theorem? Here, you definitely need formulas (or at least sentences), but we know how to interpret those so it's not a big deal. The Compactness Theorem tells us that any inconsistent set of sentences has a finite inconsistent subset. As a collection of deduction rules, we can take all rules

$\phi_1,\dots,\phi_k \vdash \psi$

where $\{\phi_1,\dots,\phi_k,\lnot\psi\}$ is an inconsistent set of sentences. This is a horrible system, but it's finitary, sound and complete for semantical consequence. (You can do something similar if you want deduction rules for formulas, but there's really no point to any of this.) This is a completely useless completeness theorem since there it does not give a useful description of this set of deduction rules. You would have a very hard time proving the Gödel Incompleteness Theorems from this...

Answer 2

This is a partial answer to the above question. It is too long for a comment. I write it hear hoping to hear idea from those senior than me, and in case it is useful.

Here is some back ground, you might skip it if you are familiar with Poizat's definition:

There are two definitions of p- equivalent given in Poizat's A course in Model Theory, one via local isomorphism and the other via formal language. I think to compare the two view, it is crucial to compare this twos definitions.

Let ${\bf M}=(M, R)$, ${\bf N}=(N, S)$ structures with $ R, S$ $m$-ary relations.

Formal language definition:

Two $n$-tupe $\vec{a},\vec{b}$ are $p$-equivalent if and only if they satisfy the same formula in the language with quantifier rank at most $p$.

Local isomorphism definition: (Fraissean point of view)

A local isomorphism $s$ from $\bf M$ to $\bf N$ is defined to be an isomorphism between the a restriction of $\bf M$ to a finite set $\vec{a}$ to the restriction of $\bf N$ to a finite set $\vec{b}$. 0-isomorphism are local isomorphisms. A local isomorphism $s$ is a $p+1$-isomorphism iff

1) Forth condition: for any element $c$ in $M$ there is $d$ in $N$, and $t$ a $p$-isomorphism which map $c$ to$d$ and extends $s$.

2) Back condition: for any element $d$ in $N$ there is $c$ in $M$, and $t$ a $p$-isomorphism which map $c$ to $d$ and extends $s$.

Two $n$-tupe $\vec{a},\vec{b}$ are $p$-equivalent if there is a $p$ automorphism that maps one into another

First, we try to answer the question about syntax. We can unravel the local isomorphism definition to make it more like the language one, we get the following:

Two $n$-tupe $\vec{a},\vec{b}$ are $p$-equivalent iff all the following are satisfied

$ \forall c_p \in M, \exists d_p \in N,$ $ \forall c_{p-1} \in M, \exists d_{p-1} \in N,$...( all statements about $\vec{a}, c_p, c_{p-1}, c_{p-2}, ...c_1 ) \leftrightarrow$ ( all statements about $\vec{b}, d_p, d_{p-1}, d_{p-2}, ...d_1 $ )

$ \forall d_p \in N, \exists c_p \in M,$ $ \forall c_{p-1} \in M, \exists d_{p-1} \in N,$...( all statements about $\vec{a}, c_p, c_{p-1}, c_{p-2}, ...c_1 ) \leftrightarrow$ ( all statements about $\vec{b}, d_p, d_{p-1}, d_{p-2}, ...d_1 $ )

... ( all alternation between $c_i \in M$ and $d_i \in N$).

I think was wrong in the question. There was some genuine difference between the Fraissean view and the traditional view. In both cases we do use (formal or informal) quantifiers. But in traditional view the quantifier was on each domain and in the Fraissean view the quantifier is running back and forth between two domains. However, this difference does NOT shows Fraissean view point is anymore free from language than the traditional view. (The quantifier is even more complicated, in fact. But it is not the point).

I think the difference is like this: The traditional view point characterize local morphism in term of invariance. (In this case, it preserve the statements with at most p quantifier). The Fraissean view point describe the morphisms directly through induction. Both are useful. The traditional view point is used in the proof of compactness (I don't know if this can be done in an easy way using the Fraissean view). The Fraissean view is important in many applications: To show that many theories are complete.

How about deduction rules?

I think we can define the deduction rule on the model side in an adhoc way (or may be not so adhoc) but it seems rather irrelevant here. So my previous concern is not correct.

I think that it is right that model theory can be developed independent of deduction rules. Perhaps that is because two equivalent statement are exactly the same to all model. I still don't understand exactly the relationship between Fraissean approach and this.