15
$\begingroup$

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 $\neg\varphi$ is not satisfiable, and consequently that $\varphi$ is satisfiable if and only if $\neg\varphi$ 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}\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.

$\endgroup$
  • 10
    $\begingroup$ +1 for all the homework you did before coming here for help, and for the care you took in formatting. $\endgroup$ – Ethan Bolker Nov 19 '18 at 1:15
  • 3
    $\begingroup$ Kind of you to say so! Thank you @EthanBolker $\endgroup$ – Rebecca Bonham Nov 19 '18 at 2:28
  • 2
    $\begingroup$ @RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day. $\endgroup$ – Don Thousand Nov 19 '18 at 6:41
  • $\begingroup$ @RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best. $\endgroup$ – Rebecca Bonham Nov 19 '18 at 16:43
7
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?) $\endgroup$ – Rebecca Bonham Nov 19 '18 at 1:00
  • 1
    $\begingroup$ @RebeccaBonham $\models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $\varphi$ is a logic statement, and $\mathscr{M}\models\varphi$ is a statement about that logic statement. $\endgroup$ – Bram28 Nov 19 '18 at 1:03
  • $\begingroup$ Got it, thanks. $\endgroup$ – Rebecca Bonham Nov 19 '18 at 1:04
  • 2
    $\begingroup$ Strictly speaking I think "Gödel's completeness result" is only "if $\varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it. $\endgroup$ – Henning Makholm Nov 19 '18 at 1:08
  • 1
    $\begingroup$ @HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem $\endgroup$ – Bram28 Nov 19 '18 at 1:16
6
$\begingroup$

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, $x\in\mathbb{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 $\neg\varphi$, written $\mathcal{A}(\neg\varphi)$. Step 4, case (a): If $\mathcal{A}(\neg\varphi)$ returns "$\neg\varphi$ 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}(\neg\varphi)$ returns "$\neg\varphi$ 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}$.

$\endgroup$
  • 2
    $\begingroup$ For 1. The $\mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $\varphi$ is valid if and only (by definition of valid) if $\varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $\varphi$ is false if and only if (by semantics) there is no model in which $\neg \varphi$ is true if and only if (by definition satisfiability) $\neg \varphi$ is not satisfiable. $\endgroup$ – Bram28 Nov 19 '18 at 14:56
  • 1
    $\begingroup$ For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $\varphi$ is provable, then $\mathcal{B}$ will say it is provable, and if $\varphi$ is not provable, then $\mathcal{B}$ will say it is not provable. So, if you find that $\neg \varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if' $\endgroup$ – Bram28 Nov 19 '18 at 15:02
  • 1
    $\begingroup$ Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure. $\endgroup$ – Bram28 Nov 19 '18 at 15:06
  • 1
    $\begingroup$ 1. I was thinking of "the $\mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $\models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation. $\endgroup$ – Rebecca Bonham Nov 19 '18 at 16:51
  • 2
    $\begingroup$ Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other. $\endgroup$ – Bram28 Nov 19 '18 at 17:10

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.