I'm working through this module, "Undecidability of First-Order Logic" and would love to talk about the two exercises given immediately after the statement of Godel's completeness theorem.
First, note Definition 2.1 from the text: A sentence $\varphi$ is valid if it is true in all models. In contrast, $\varphi$ is satisfiable if it is true in some model. Then the exercises are given as follows:
-
Let $\varphi$ be a sentence in first-order logic. Show that $\varphi$ is valid if and only if $\neg\varphi$ is not satisfiable, and consequently that $\varphi$ is satisfiable if and only if $\neg\varphi$ is not valid.
-
Suppose that we have an algorithm $\mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not. Show that we can use this to get an algorithm $\mathcal{B}$ to tell whether a sentence of first-order logic is provable or not.
Conversely, suppose that we have an algorithm $\mathcal{B}$ to tell whether a sentence of first-order logic is provable or not. Show that we can use this to get an algorithm $\mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not.
The first exercise seems pretty straightforward. My answer:
- Let $\mathscr{M}$ be a model and read "$\varphi$ is true in $\mathscr{M}$" for $\mathscr{M}\models\varphi$. Then by the definitions above and basic facts of logic (such as DeMorgan's laws for quantifiers), the equivalence $\forall \mathscr{M} (\mathscr{M}\models\varphi) \equiv \neg\exists \mathscr{M} (\mathscr{M}\models\neg\varphi)$ holds as desired. The same goes for the restatement introduced by "consequently" in the exercise, i.e. $\exists \mathscr{M}(\mathscr{M}\models \varphi) \equiv \neg\forall(\mathscr{M}\models\neg\varphi)$.
Make sense? Anybody spot any errors, or feel like suggesting improvements of any kind?
Okay. Now the second exercise is where things get more interesting, at least for me, because I don't fully grasp this idea of correspondence between "valid" and "provable," which is the core of Gödel's completeness theorem.
Looking at what Wikipedia has to say about the theorem, I feel like I basically understand the result, but am still unsure how I would apply it in terms of the second exercise.
Take the first part of the problem: all I've got is an algorithm $\mathcal{A}$ that decides satisfiability of $\varphi$. The completeness theorem establishes an equivalence between syntactic provability and semantic validity. I can't figure out how to cross the chasm from satisfiability to validity, or otherwise find the logical connection I would need to use the theorem to solve my problem.
While searching for similar questions before posting, I found this one, which offers some stimulating food for thought but deals with different givens, namely: an algorithm that takes a $\varphi$ and returns $\varphi'$ such that $\varphi$ is satisfiable iff $\varphi'$ is valid. I can see that this is getting close to what I need, but again I can't see how to adapt it to my purposes.
Can anyone offer a hint, a suggestion, or pointer of any kind? I would much appreciate it.
Best Answer
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $\neg$, $\forall$, and $\exists$ are logical operators, but $\models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $\varphi$ is valid or not, you can decide whether $\neg \varphi$ is satisfiable or not: if $\neg \varphi$ is satisfiable, then $\varphi$ is not valid, but if $\neg \varphi$ is not satisfiable, then $\varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $\varphi$ is valid, then it is provable, and if $\varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $\mathcal{A}$ that can figure put whether $\varphi$ is satisfiable or not for any $\varphi$, then design algorithm $\mathcal{B}$ that is trying to figure out whether $\varphi$ is provable or not as follows:
Take in $\varphi$
Negate $\varphi$
Call algorithm $\mathcal{A}$ with $\neg \varphi$
4a. If algorithm $\mathcal{A}$ says that $\neg \varphi$ is satisfiable, then print '$\varphi$ is not provable!'
4b. If algorithm $\mathcal{A}$ says that $\neg \varphi$ is not satisfiable, then print '$\varphi$ is provable!'