validity reduction between FOL fragments

54 Views Asked by At

Let $\Sigma_1=\langle R^2,P^1,=\rangle$ a dictionary with $R$ a binary relation, $P$ an unary relation and equality.

Let $\Sigma_2=\langle c,f^1,=\rangle$ a dictionary with $c$ a constant, $f$ an unary function and equality.

Prove or Disprove: There exists an algorithm that given a formula $\varphi$ over the alphabet $\Sigma_2$ outputs a formula $\psi$ over the alphabet $\Sigma_1$ such that $\varphi$ is valid if and only if $\psi$ is valid.

I know that in monadic logic validity is decidable since satisfiability is decidable but $\Sigma_2$ is not monadic as it contains a binary relation.

I tried to prove that satisfiability in $\Sigma_1$ is decidable but it dosen't seem that way.

Any help?

1

There are 1 best solutions below

2
On BEST ANSWER

There is such an algorithm. The main idea is that we can simulate the constant symbol $c$ with the unary relation $P$, by asserting that there is a unique element satisfying $P$, and we can simulate the function symbol $f$ with the binary relation $R$, by asserting that $R$ is the graph of a function.

So we turn the $\Sigma_2$-formula $\varphi$ into a $\Sigma_1$-formula of the following form:

$$((\exists^! x\, P(x)) \land (\forall x\, \exists^! y\, R(x,y)) \rightarrow \hat{\varphi},$$ where $\exists^!x$ means "there exists a unique $x$" and $\hat{\varphi}$ is a formula obtained by "replacing all instances of $c$ and $f$ in $\varphi$ with $P$ and $R$."

I put the last part in quotes there for a reason: we have to think a bit about how to construct $\hat{\varphi}$. The problem is that $\Sigma_2$-formulas can have nested terms, which we have to unravel. For example, suppose $\varphi$ is the formula $$f(c) = f(f(x)).$$

This is equivalent to the unnested formula $$\exists z_1\, (c = z_1 \land \exists z_2\, (f(z_1) = z_2 \land (\exists z_3\, f(x) = z_3 \land \exists z_4\, (f(z_3) = z_4 \land z_2 = z_4)))).$$

The point is that $c$ only appears in subformulas of the form $c = z$ for $z$ a variable, equivalent to $P(z)$. And $f$ only appears in subformulas of the form $f(z) = w$ for $z$ and $w$ variables, equivalent to $R(z,w)$.

Then we can take $\hat{\varphi}$ to be $$\exists z_1\, (P(z_1) \land \exists z_2\, (R(z_1,z_2) \land (\exists z_3\, R(x,z_3) \land \exists z_4\, (R(z_3,z_4) \land z_2 = z_4))))$$

I'll leave it to you to fill in the details in the general case.


P.S. This idea of simulating constant and function symbols by relation symbols allows us to safely assume, in many contexts in model theory, that we're working with a purely relational language. This assumption isn't always safe, though: whether we have function symbols in the language matters if we're thinking about substructures (in a relational language, any subset is a substructure) or quantifier elimination (the translation from a general language to a relational language involves adding quantifiers).

P.P.S. $\Sigma_1$ and $\Sigma_2$ have standard meanings in logic, so it's probably better to use other notation for your languages/dictionaries! Also, the collection of all formulas in the language $\Sigma_1$ is just full first-order logic in the language $\Sigma_1$. It's not called a "fragment" - except in the trivial sense that it's the maximal fragment (the full logic).