1
$\begingroup$

For some context: I'm currently taking a course of Formal Methods and Logics and there's a passage where we show that the monadic second order ($\text{MSO}$) theory of (possibly labelled) linear orders is decidable. We introduced the question by saying what we intend for linear order, which can be seen as an interpretation of the language:

$$\{\le^{(2)},X_1^{(1)},...,X_n^{(1)}\}$$

But then we continued by saying that "we will show that for each formula $\phi \in \text{MSO}(\{\le\})$ with free monadic variables $X_1,...,X_n$ there exists a finite automaton that recognizes its language", etc.

Notice how the symbols $X_1,...,X_n$ are now interpreted not anymore as unary relational symbols of the language (i.e. the labels), but rather as free variables of the formula. I tagged this question with "predicate logic", too, because we could make the same parallel between first-order variables $x$ and constant symbols of the language.

My question is: under what circumstances can we "drop" the symbols from the language and treat them equivalently as free variables? As in:

$$(D^I,\le^I,X_1^I,...,X_n^I)\vDash\phi\quad\to\quad(D^I,\le^I),\,X_i\overset{\sigma}{\mapsto} X_i^I\vDash\phi(X_1,...,X_n)$$

where $I$ is the interpretation and $\sigma$ is its state. My guess is that we did it for convenience, since the proof of the above is by induction over the structural complexity of the formula, which is independent of the number of free variables, whereas we wish to maintain the same language. I hope the question is clear, since I myself am a bit confused. Thanks in advance.

$\endgroup$
  • $\begingroup$ When we "drop" symbols from the language and treat them as variables, I wouldn't say we treat them equivalently. Once the $X_i$ are variables, we can quantify them, and that includes the possibility of quantifying some of them universally and others existentially. The closest we can come to that in first-order logic is that statements like "$\phi$ is valid" implicitly quantify all $X_i$'s universally, and "$\phi$ is satisfiable" quantifies them all existentially. $\endgroup$ – Andreas Blass Feb 13 at 1:47
  • $\begingroup$ @AndreasBlass Ok, I think I get what you're saying, but intuitively would the formalism lose expressivity if we completely replaced the use of free variables with the possibility to augment the language with corresponding symbols or viceversa? $\endgroup$ – giofrida Feb 13 at 2:05
  • $\begingroup$ Not if you never do anything with the free predicate variables. But if you actually use them as variables, meaning you can quantify them, then yes, the formalism with predicate symbols as part of the first-order language is less expressive than the second-order formalism. The latter allows statements of the form $(\forall X_1)(\exists X_2)\dots$, and the former doesn't. $\endgroup$ – Andreas Blass Feb 13 at 2:16
  • $\begingroup$ @AndreasBlass No, this is clear, I'm aware that second-order logic is more expressive than first-order. I was assuming that the logic remained the same (in my case, MSO). Should I try to polish the main question? I don't know how to phrase it better than I already did... $\endgroup$ – giofrida Feb 13 at 2:26

Your Answer

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

Browse other questions tagged or ask your own question.