Algorithm for deciding satisfiability of a universal statement

215 Views Asked by At

Question: Given $\Sigma = \lbrace c , R_1^2, ... , R_k^2 \rbrace $ when c is a constant. Prove / disprove that exists an finite time algorithm for deciding satisfiability of a universal statement A.

My proof: True: Due to Herbrand's theorem, a universal statement is satisfiable $\iff$ all of it's ground instances are satisfiable. Since there are no function symbols then this just means checking $c$ in every ground instance of the statement A and this is finite as the statement is of finite length.

I want to make sure that this argument is indeed true.

1

There are 1 best solutions below

0
On

Your argument is right, but you don't need to appeal to a strong result like Herbrand's theorem. Universal sentences are preserved under substructures, i.e., if $\phi$ has the form $\forall\overline{x}\psi$ where $\psi$ is quantifier-free and if $\phi$ is valid in a structure $M$, then $\phi$ is valid in any substructure of $N$. For your signature containing only a constant symbol $c$ and some relation symbols, any substructure $M$ has a substructure $N$ whose universe comprises the singleton set $\{c\}$ and $\phi$ must be valid in $N$ if it is to be valid in $M$. This does imply (if you like to put it that way), that $\phi$ is satisfiable iff its ground instances are satisfiable.