1
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

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.