502 – Completeness | A kind of library

502 – Completeness

1. Preliminaries

Just as with propositional logic, one can define a proof system for first order logic. We first need two definitions.

Definition 1 If ${\phi}$ is a formula, a generalization of ${\phi}$ is any formula of the form

$\displaystyle \forall x_1\forall x_2\dots\forall x_n\,\phi.$

(We are not requiring in the definition above that the ${x_i}$ are different or that they are present in ${\phi.}$ )

Definition 2 Let ${t}$ be a term, let ${x}$ be a variable, and let ${\phi}$ be a formula. We say that ${t}$ is substitutable for ${x}$ in ${\phi}$ iff no free occurrence of ${x}$ in ${\phi}$ is within the scope of a quantifier ${\exists z}$ or ${\forall z}$ with ${z}$ a variable occurring in ${t.}$

The point of this definition is the following: Given a formula ${\phi,}$ a variable ${x,}$ and a term ${t}$ , let ${\phi[x/t]}$ denote the formula resulting of replacing each free occurrence of ${x}$ in ${\phi}$ by ${t.}$ For example, if ${\phi}$ is ${\exists y\,(x\ne y),}$ and ${t=f(z,w)}$ for some binary function symbol ${f}$ and variables ${z,w,}$ then ${\phi[x/t]=\exists y\,(f(z,w)\ne y).}$ Similarly, ${\phi[y/t]=\phi}$ because no occurrence of ${y}$ in ${\phi}$ is free, and ${\phi[x/y]=\exists y\,(y\ne y).}$

We would like ${\phi[x/t]}$ to mean that ${t}$ has whatever property ${\phi}$ was claiming of ${x.}$ However, some care is needed, as the last example shows: While ${\phi}$ asserts that there is some element other than ${x}$ , which is true in any model with at least two elements, no matter how ${x}$ is interpreted, we have that ${\phi[x/y]}$ asserts that there is an element different from itself, which is always false.

The notion of “ ${t}$ being substitutable for ${x}$ ” captures the idea that, no matter what ${\phi}$ is, ${\phi[x/t]}$ will actually express, as intended, the property of ${t}$ that ${\phi}$ expressed of ${x}$ .

2. A Hilbert-type proof system

Just as with propositional calculus, we can develop a notion of formal proof as a finite string of formulas with some properties.

First, we state the axioms of predicate logic. To be concrete, we formalize syntax, so the only primitive connectives are ${\lnot,\rightarrow}$ and the only quantifier is ${\forall,}$ and all others are treated as abbreviations.

A logical axiom is any generalization of any formula of the following form:

(Propositional axioms)
1. ${\phi\rightarrow(\psi\rightarrow\phi).}$
2. ${((\phi\rightarrow(\psi\rightarrow\chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\chi)).}$
3. ${(\lnot\phi\rightarrow\lnot\psi)\rightarrow((\lnot\phi\rightarrow\psi)\rightarrow\phi).}$
(Quantifier axioms)
1. ${\forall x\,(\phi\rightarrow\psi)\rightarrow(\forall x\,\phi\rightarrow\forall x\,\psi).}$
2. ${\phi\rightarrow\forall x\,\phi,}$ provided that ${x}$ is not free in ${\phi.}$
3. ${\forall x\,\phi\rightarrow\phi[x/t],}$ provided that ${t}$ is a term substitutable for ${x}$ in ${\phi.}$
(Equality axioms)
1. ${x=x.}$
2. ${x=y\rightarrow y=x.}$
3. ${(x=y\land y=z)\rightarrow(x=z).}$
4. ${(x_1=y_1\land \dots\land x_n=y_n)\rightarrow}$ ${(f(x_1,\dots,x_n)=f(y_1,\dots,y_n)).}$
5. ${(x_1=y_1\land\dots\land x_ny_n)\rightarrow}$ ${(R(x_1,\dots,x_n)\leftrightarrow R(y_1,\dots,y_n)).}$

As before, the only rule of inference is MP, Modus Ponens.

Proofs are defined as before: Given a set of formulas ${S}$ and a formula ${\phi,}$ we write ${S\vdash\phi,}$ ${S}$ proves ${\phi,}$ iff there is a proof of ${\phi}$ from ${S,}$ i.e., a sequence

$\displaystyle \phi_1,\dots,\phi_n$

where each ${\phi}$ is either a logical axiom, or an element of ${S,}$ or comes from previous ${\phi_j,\phi_k}$ by an application of MP. Again, if ${S=\emptyset}$ we simply write ${\vdash\phi.}$

It is easy to verify that ${{\mathcal M}\models \phi}$ whenever ${\phi}$ is a logical axiom and ${{\mathcal M}}$ is a structure, and that if ${{\mathcal M}\models S}$ and ${S\vdash\phi,}$ then ${{\mathcal M}\models\phi.}$ This is the soundness theorem.

3. Completeness

More delicate is the verification of the completeness theorem. I will only sketch the idea of one of its proofs, due to Leon Henkin.

As with propositional calculus, it is enough to check that if ${S}$ is consistent, i.e., it does not prove a contradiction, then ${S}$ is satisfiable, i.e., it has a model. Just as in that proof, it is enough to prove this result for a set ${S}$ that is maximal, i.e., such that for any formula ${\phi}$ in the language of ${S,}$ either ${S\vdash \phi}$ or ${S\vdash\lnot\phi,}$ and one can also request that ${S}$ is actually closed under deduction, i.e., if ${S\vdash\phi,}$ then ${\phi\in S.}$

Henkin’s first idea is to expand the language by adding new constants, and to expand the theory ${S}$ so it is Skolemized. The name comes from Thoralf Skolem, and refers to the notion of a Skolem Hull; this is a kind of substructure in which only definable elements are considered. What Henkin means here is the following: For each formula ${\phi(x)}$ in the language, with only one free variable ${x,}$ add a new constant symbol ${c_\phi,}$ and add to ${S}$ the `axiom’

$\displaystyle \exists x\,\phi\rightarrow\phi[x/c_\phi].$

What this accomplishes is that now we have a canonical `witness’ to existential statements, namely, if ${M\models S}$ and ${M\models\exists x\,\phi,}$ then in fact ${M\models\phi(c_\phi^M).}$

One needs to verify that given any consistent ${S}$ in a language ${{\mathcal L},}$ one can expand ${{\mathcal L}}$ to a larger language ${{\mathcal L}'}$ and ${S}$ to ${S'}$ in language ${{\mathcal L}'}$ so that ${S'}$ is still consistent, it is maximal, and is Skolemized.

This is accomplished by iterating the obvious process: First expand ${S}$ so it is maximal consistent in language ${{\mathcal L},}$ expand the language adding constants ${c_\phi}$ for all formulas ${\phi}$ in ${{\mathcal L},}$ thus obtaining ${{\mathcal L}_1,}$ and expand ${\hat S}$ as required to form ${S_1.}$ This does not yet work, since there are new formulas, e.g. ${\exists x\,(x\ne c_{y=y})}$ that do not yet admit Skolemization. So one repeats, first passing to a maximal consistent ${\hat S_1}$ in language ${{\mathcal L}_1,}$ then obtaining a larger language ${{\mathcal L}_2}$ and a larger theory ${S_2}$ in ${{\mathcal L}_2,}$ etc. The language ${{\mathcal L}'=\bigcup_n{\mathcal L}_n}$ and the theory ${S'=\bigcup_n S_n}$ are finally as required.

One of course needs to check that the passage from ${S_n}$ to ${S_{n+1}}$ does not add contradictions.

Once we have a theory maximal consistent and with Skolemization, let’s call it ${S}$ again, Henkin’s idea is to note that the theory essentially describes a model of itself.

Namely, one defines an equivalence relation on the constant symbols of the language by setting

$\displaystyle c\sim c' \Longleftrightarrow S\vdash c=c'.$

(That this is indeed an equivalence relation follows easily from the equality axioms.)

Now we define a model ${M}$ by setting as its universe the set of equivalence classes ${[c].}$ We define the interpretations of constant, relation, and function symbols as dictated by ${S.}$ For example, if ${f}$ is a symbol for a binary function, we define ${f^M:M\times M\rightarrow M}$ by setting

$\displaystyle f^M([a],[b])=[c_{x=f(a,b)}].$

(One needs to check that this is well defined).

One sets ${a^M=[a]}$ for ${a}$ a constant symbol. Finally, one defines ${R^M}$ , for ${R}$ an ${n}$ -ary relation symbol, by

$\displaystyle R^M([a_1],\dots,[a_n])\Longleftrightarrow S\vdash R(a_1,\dots,a_n).$

Once the model ${M}$ is defined, then one checks that ${M\models S,}$ as desired. This makes essential use of the fact that ${S}$ is Skolemized.

One nice property of this technique is that it implies that if ${S}$ is a theory in a countable language, and ${S}$ is consistent, then ${S}$ has a countable model. We will return to the issue of the sizes of models later in the course, once we have discussed infinite cardinalities.

An immediate consequence of the completeness theorem is compactness: If ${S}$ is unsatisfiable, then it must be inconsistent, and therefore a finite subtheory ${S_0}$ is inconsistent, hence unsatisfiable.

This indicates that some use of the axiom of choice is required in any proof of completeness, since we have seen that compactness implies the existence of nonprincipal ultrafilters, and it is known that this requires some amount of choice. (In the proof sketched above, we used choice each time we expanded a consistent theory to a maximal consistent one. If the original theory is countable, this only requires König’s lemma, but more choice is necessary if ${S}$ is uncountable.)

Typeset using LaTeX2WP. Here is a printable version of this post.

This entry was posted on Friday, September 25th, 2009 at 3:21 pm and is filed under 502: Logic and set theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

2 Responses to 502 – Completeness

502 – Notes on compactness « A kind of library says:

August 29, 2012 at 12:03 pm

[…] indicated on the set of notes on the completeness theorem, compactness is an immediate consequence of completeness. Here I want to explain a purely […]

Reply
502 – First order (or predicate) logic « A kind of library says:

August 29, 2012 at 12:44 pm

[…] with .footnote{This notion of does not coincide with the notion described in the set of notes on completeness, but it turns out to be equivalent to it since I am requiring that does not appear anywhere in […]

Reply

	ปั่นสล็อต on 414/514 The theorems of Rieman…
	Richard Kimberly Hec… on Woodin’s proof of the se…
	Is there a Borel-mea… on 414/514 Examples of Baire clas…
	Simple bijectiveness… on 580 -Some choiceless results…
	Schur’s theore… on 580 -III. Partition calcu…
	Uncountable linearly… on 403/503 – Homework …
	What is a non-constr… on On strong measure zero se…
	function from Nmathb… on Hindsight
	Cauchy Schwarz Inequ… on 275 -Positive polynomials
	What is a Cantor-sty… on 580 -Some choiceless results…
	Question about Gener… on 580 -Some choiceless results…
	Set has Measure Zero… on On strong measure zero se…
	Non-measurable subse… on 580 -Cardinal arithmetic …
	hmeng1 on 414/514 The theorems of Rieman…
	580 -Cardinal arithm… on 580 -Cardinal arithmetic …

M	T	W	T	F	S	S
	1	2	3	4	5	6
7	8	9	10	11	12	13
14	15	16	17	18	19	20
21	22	23	24	25	26	27
28	29	30

A kind of library