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$
4
  • 10
    $\begingroup$ +1 for all the homework you did before coming here for help, and for the care you took in formatting. $\endgroup$ Commented Nov 19, 2018 at 1:15
  • 3
    $\begingroup$ Kind of you to say so! Thank you @EthanBolker $\endgroup$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 at 16:43

2 Answers 2

Reset to default
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$
7
  • $\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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 at 1:03
  • $\begingroup$ Got it, thanks. $\endgroup$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 at 1:16
7
$\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$
7
  • 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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 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$ Commented Nov 19, 2018 at 17:10

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.