# Definitions in metamathematics

In model theory, the satisfiability relation $$\vDash$$ between a model $$M= (D,f)$$ and a set of formulas tells us when a formula $$\varphi$$ is true or not in the model ("interpretation") $$M$$.

This relation is usually defined recursively in the following way. I won't be 100% precise giving the definition, but it's something like this:

• $$M \vDash \neg \varphi$$ if and only if $$M \not \vDash \varphi;$$

• $$M \vDash \varphi \wedge \psi$$ if and only if $$M \vDash \varphi$$ and $$M \vDash \psi$$;

• $$M \vDash \forall x(\varphi)$$ if and only if for all $$x$$ in $$D$$ the formula $$\varphi$$ holds;

• $$M \vDash \exists x(\varphi)$$ if and only if there exists an $$x$$ in $$D$$ such that the formula $$\varphi$$ holds;

...and so on. At this point, there's something that really bothers me.

Model theory is developed in set theory (models are sets), which uses the language of first order logic with the connectives $$\wedge, \vee, \neg, \Rightarrow$$ and the quantifiers $$\exists , \forall$$. Well, we know that set theory is so powerful that it allows us to talk about first order logic, and this is why we can describe the semantics of first order logic within set theory (the model theoretic semantics). That said, why is the natural language used in the recursive definition of $$\vDash?$$ Shouldn't we use the usual connectives connectives $$\wedge, \vee, \neg, \Rightarrow$$ and the quantifiers $$\exists , \forall$$ in the definition?

I know that the symbols would be graphically the same (since we are describing first order logic with first order logic) and it would look circular, but if necessary, we could change a bit the connectives since they are symbols of a language and define $$\vDash$$ for this symbols in a way that they still model our intuitive idea of the logical connectives (and anyway $$\vDash$$ is a relation between sets, and there's nothing circular about that, but that's not the point). I mean something like this:

• $$M \vDash \neg_L \varphi \Leftrightarrow M \not \vDash \varphi;$$

• $$M \vDash \varphi \wedge_L \psi \Leftrightarrow \Big (M \vDash \varphi \wedge M \vDash \psi \Big )$$;

• $$M \vDash \forall_L x(\varphi) \Leftrightarrow \forall x \in D:\varphi;$$

• $$M \vDash \exists_L x(\varphi) \Leftrightarrow \exists x \in D: \varphi$$

...and so on. That's a lot more rigorous, and in this way it's easier to see the "interpretation" of the considered language $$L$$.

Why isn't the definition stated in this way, using the formal connectives? Is there something that I'm missing or are we informally using our natural language just because it's easier to understand for the reader and it's implicitly used the formal language as I did?

First, it's definitely desirable to have some notational distinction between object and meta level connectives. Your subscript $$L$$ is a reasonable way to accomplish this. Personally, though, at least in introductory texts, I would strongly encourage notation that makes it very hard for these things to be confused, as confusing them is seemingly quite common. (In this case, I'd personally, interpret the connectives more directly as set-theoretic operations, e.g. $$\land$$ as $$\cap$$.) Related to this, I suspect using more similar notation would exasperate philosophical concerns about "circularity".