Vrftjkry

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:

1. Let $varphi$ be a sentence in first-order logic. Show that $varphi$ is valid if and only if $negvarphi$ is not satisfiable, and consequently that $varphi$ is satisfiable if and only if $negvarphi$ is not valid.




2. 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:

1. Let $mathscr{M}$ be a model and read "$varphi$ is true in $mathscr{M}$" for $mathscr{M}modelsvarphi$. Then by the definitions above and basic facts of logic (such as DeMorgan's laws for quantifiers), the equivalence $forall mathscr{M} (mathscr{M}modelsvarphi) equiv negexists mathscr{M} (mathscr{M}modelsnegvarphi)$ 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 negforall(mathscr{M}modelsnegvarphi)$.

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.

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:

1. Take in $varphi$




2. Negate $varphi$




3. 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!'

For my own purposes, I'm archiving here my best attempt at integrating, in a compact manner, everything that was mentioned in the answers to my original question. Any comments or critiques of any kind are always welcome. Thanks again to the contributors.

Definitions. A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model.

Completeness theorem with soundness. A sentence in first-order logic is provable if and only if it is valid.

Then the answers to the problems stated above can be given as follows:

1. Let $mathscr{M}_x$ be a model, $xinmathbb{N}$. Let $varphi$ be a sentence in first-order logic. Let $P(x)$ be the predicate "$varphi$ is true in $mathscr{M}_x$." Then $forall x P(x) equiv neg exists x P(x)$ and $exists x P(x) equiv neg forall x neg P(x)$ by the above definitions and De Morgan's laws.




2. Suppose we have $mathcal{A}$. Let $mathcal{B}$ be the algorithm defined by the following procedure. Step 1: take $varphi$ as input. Step 2: negate $varphi$. Step 3: call $mathcal{A}$ with input $negvarphi$, written $mathcal{A}(negvarphi)$. Step 4, case (a): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is satisfiable," then by the above equivalences $varphi$ is not valid and by the completeness theorem it is not provable. Step 4, case (b): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is not satisfiable," then by the above equivalences $varphi$ is valid and by the completeness theorem it is provable. Thus by making use of $mathcal{A}$ we have obtained $mathcal{B}$ such that $mathcal{B}$ decides whether $varphi$ is provable or not. By a symmetric argument we can obtain $mathcal{A}$ if given $mathcal{B}$.