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?](https://mathoverflow.net/questions/9309/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 ...$. 



In what sense Fraissean view point shows Model Theory can be done without any formal syntax and deduction rule?
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...


