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".

Second, simply using symbols instead of words does not immediately make things "a lot more rigorous".

To address the heart of your question: The meta-theoretical work, like most mathematics, is usually done informally. (It certainly can be done formally too, though.) To actually start to formalize the meta-theory, we would need to define everything formally. This means a formal definition of, e.g., terms and formulas, and by "formal" I mean an expression in the explicitly chosen theory, e.g. ZFC. This is usually a lot of work and not something the authors are interested in doing. Being "formal" where it is convenient in a pile of otherwise informal mathematics is, at best, not very smooth from a presentation perspective, and, at worst, a touch disingenuous.

It doesn't really make sense to talk about "implicitly using" a formal language. "Implicitly using" formalism is just not using formalism. Instead, the usual goal (nominally at least) is that formalizing the informal math should be relatively straightforward if tedious. To this end, mathematical vernacular is fairly highly structured. In practice, my impression is that since few mathematicians have experience formalizing math in something like a proof assistant such as Mizar or Coq, they don't actually have a good feel for where the difficult parts are in formalization. They simultaneously think formalism is a lot more overbearing than it is1 (or can be), while at the same time think that how to formalize something is a lot more straightforward than it is. This isn't really a problem though, as (again) few mathematicians ever actually do this, so the bluff is never called.

1 This is not to say that it doesn't add a lot more work and complexity, but my impression is that many mathematicians' views on this are more driven from tales about Principia or Bourbaki than actually using systems designed to be usable.

  • 1
    $\begingroup$ So the informal natural language is being used because it's more clear to the reader, its use is common in mathematics (common mathematics is informal), and because it avoides ambiguity between meta-language and object language, knowing that if necessary the definition could be formalized in the meta-theory with the first order language of sets, right? $\endgroup$ – Luis Orion Mar 13 at 13:45
  • 1
    $\begingroup$ I think that's reasonable except that it makes it sound more intentional that it is. Working informally is just the "default" thing to do. Choosing to use a formal meta-language means you have to actually describe it, which, in practice, means a significant part of the text will be explaining the formalism unless the point of the text is to do whatever in that formal system. For example, if I wanted to write a text on doing model theory in Coq, I may assume the readers are already familiar with Coq and not spend one or more chapters explaining Coq. $\endgroup$ – Derek Elkins Mar 13 at 19:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.