\documentclass[% version=last,% a5paper, 10pt,% headings=small,% bibliography=totoc,% index=totoc,%o twoside,% leqno,% cleardoublepage=empty,% %open=any,% %parskip=half,% %draft=false,% draft=true,% %DIV=classic,% DIV=11,% headinclude=true,% pagesize]%{scrreprt} {scrartcl} %\usepackage[notref,notcite]{showkeys} \renewcommand{\theequation}{\fnsymbol{equation}} \usepackage[headsepline]{scrpage2} \pagestyle{scrheadings} \clearscrheadings \ohead{\pagemark} \ihead{G\"odel's Completeness Theorem} \usepackage{hfoldsty} \usepackage[neverdecrease]{paralist} \usepackage{url} \usepackage{relsize} % Here \smaller scales by 1/1.2; \relscale{X} scales by X \renewenvironment{quote}{\begin{list}{} {\relscale{.90}\setlength{\leftmargin}{0.05\textwidth} \setlength{\rightmargin}{\leftmargin}} \item[]} {\end{list}} \usepackage{amsmath,amsthm,amssymb,bm,upgreek,mathrsfs} %\usepackage[all]{xy} \usepackage{stmaryrd} % for \mapsfrom \newcommand{\Forall}[1]{\forall#1\;} \newcommand{\Exists}[1]{\exists#1\;} \let\oldvec\vec \renewcommand{\vec}[1]{\bm{#1}} \newcommand{\N}{\mathbb N} \usepackage[mathcal]{euscript} \newcommand{\tf}[1]{\mathcal{#1}} % ``Tarski's font'' \newcommand{\F}{\mathbf F} \newcommand{\EF}{\mathbf{EF}} \newcommand{\AF}{\mathbf{AF}} \newcommand{\AC}[1][]{\mathbf{AC}_{#1}} \newcommand{\AT}{\mathbf{AT}} \newcommand{\ACL}{\mathbf{ACL}} \DeclareMathOperator{\spectrum}{Spec} \newcommand{\spec}[1]{\spectrum(#1)} \newcommand{\conc}{\mathbin{\hat{\ }}} \newcommand{\sig}{\mathscr S} \newcommand{\str}[1]{\mathfrak{#1}} \newcommand{\size}[1]{\lvert#1\rvert} \DeclareMathOperator{\setMod}{Mod} \newcommand{\sMod}[1]{\setMod(#1)} \newcommand{\Mod}[2][]{\mathbf{Mod}_{#1}(#2)} \newcommand{\Moda}[1]{\mathbf{Mod}^*(#1)} \newcommand{\Str}{\mathbf{Str}} \DeclareMathOperator{\sentences}{Sen} \newcommand{\Sen}{\sentences} \newcommand{\modsim}{/\mathord{\sim}} \newcommand{\pow}[1]{\mathscr P(#1)} \newcommand{\inv}{{}^{-1}} \newcommand{\Cat}[1]{\bm{\mathsf{#1}}} \newcommand{\Top}{\Cat{Top}} \newcommand{\Frm}{\Cat{Frm}} \newcommand{\Loc}{\Cat{Loc}} \newcommand{\Grp}{\Cat{Grp}} \newcommand{\Set}{\Cat{Set}} \DeclareMathOperator{\domain}{dom} \newcommand{\dom}[1]{\domain(#1)} \DeclareMathOperator{\points}{pt} \newcommand{\pt}[1]{\points(#1)} \DeclareMathOperator{\homoms}{Hom} \newcommand{\Hom}[1]{\homoms(#1)} \newcommand{\bel}[1]{\left[#1\right]} \newcommand{\Sn}[1][\sig]{\sentences_{\sig}} \newcommand{\Sna}[1][\sig]{\sentences^*_{\sig}} \DeclareMathOperator{\formulas}{Fm} \newcommand{\Fm}[1][\sig]{\formulas_{#1}} \DeclareMathOperator{\freevariables}{fv} \newcommand{\fv}[1]{\freevariables(#1)} \DeclareMathOperator{\variables}{v} \newcommand{\vr}[1]{\variables(#1)} \DeclareMathOperator{\theory}{Th} \newcommand{\Th}[1]{\theory(#1)} \newcommand{\Tha}[1]{\theory^*(#1)} \renewcommand{\emptyset}{\varnothing} \renewcommand{\setminus}{\smallsetminus} \renewcommand{\leq}{\leqslant} \renewcommand{\nleq}{\nleqslant} \renewcommand{\geq}{\geqslant} \renewcommand{\phi}{\varphi} %\newcommand{\Or}{\;\lor\;} \newcommand{\Or}{\;\mathrel{\text{\textsc{or}}}\;} \renewcommand{\models}{\vDash} \newcommand{\nmodels}{\nvDash} \newcommand{\included}{\subseteq} \newcommand{\includes}{\supseteq} \newcommand{\pincluded}{\subset} \newcommand{\liff}{\leftrightarrow} \newcommand{\lto}{\Rightarrow} \newtheorem{theorem}{Theorem} \newtheorem{definition}[theorem]{Definition} \newtheorem{corollary}[theorem]{Corollary} \newtheorem{lemma}{Lemma} \theoremstyle{definition} \newtheorem{example}[theorem]{Example} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \begin{document} \title{G\"odel's Completeness Theorem} \author{David Pierce} \date{June 18, 2015} \publishers{Mimar Sinan Fine Arts University\\ Istanbul\\ \url{http://mat.msgsu.edu.tr/~dpierce/}} \maketitle Here are notes on Kurt G\"odel's 1930 paper, ``The completeness of the axioms of the functional calculus of logic,'' in the translation of Stefan Bauer-Mengelberg, as edited by Jean van Heijenoort in the anthology, \emph{From Frege to G\"odel} \cite{Goedel-compl}. I make these notes in preparation for a course of three lectures on the Compactness Theorem to be presented in the school (June 20--24, 2015) of the 5th World Congress and School on Universal Logic in Istanbul (the congress being June 25--30). G\"odel's paper apparently represents the earliest explicit statement of a version of the theorem that is now called the Compactness Theorem. In G\"odel's version, the signature is countable (``denumerable''). G\"odel defines a proof system and proves its completeness in the sense that every sentence that cannot be disproved (``refuted'') has a model. By means of the Compactness Theorem, he derives the result that, in a countable signature, an arbitrary set of sentences has a model, provided the set is consistent (the conjunction of no finite subset can be disproved). As G\"odel explains in his first paragraph, the ``functional calculus'' of his title is the \textbf{restricted functional calculus,} which he defines in a footnote: \begin{quote} In terminology and symbolism this paper follows \emph{Hilbert and Ackermann 1928.}%%%%% \footnote{Van Heijenoort spells out the reference in his own bibliography: David Hilbert and Wilhelm Ackermann, \emph{Grundz\"uge der theoretischen Logik} (Berlin: Springer, 1928).} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% According to that work, the restricted functional calculus contains the logical expressions that are constructed from propositional variables, $X$, $Y$, $Z$, \dots, and functional variables (that is, variables for properties and relations) of type I, $F(x)$, $G(x,y)$, $H(x,y,z)$, \dots, by means of the operations $\lor$ (or), $\overline{\phantom X}$ (not), $(x)$ (for all), $(Ex)$ (there exists), with the variable in the prefixes $(x)$ or $(Ex)$ ranging over individuals \emph{only, not} over functions. A formula of this kind is said to be valid (tautological) if a true proposition results from every substitution of specific propositions and functions for $X$, $Y$, $Z$, \dots, and $F(x)$, $G(x,y)$, \dots, respectively (for example $(x)[F(x)\lor\overline{F(x)}]$). \end{quote} Perhaps the expression \emph{type I} is the ancestor of our \emph{first order,} and a \emph{function of type I} takes individuals as its arguments. Such functions are our \emph{relations.} A proposition can then be understood as a nullary relation. I shall translate G\"odel's symbolism as follows: \begin{equation*}\renewcommand{\arraystretch}{1.3} \begin{array}{cc} \text{G\"odel}&\text I\\\hline\hline (x)&\forall x\\\hline (Ex)&\exists x\\\hline \overline{\phantom x}&\lnot\\\hline \&&\land\\\hline \bm{\sim}&\liff\\\hline \rightarrow&\lto\\\hline\hline \end{array} \end{equation*} (I vacillate between using $\Rightarrow$ for implication, because the notion is different from a function's being from one set to another, and using $\rightarrow$ because it is easier to write by hand.) The \emph{restricted} functional calculus is what Church \cite{MR18:631a} calls the \emph{pure} functional calculus. We just call it first-order logic. But we have made a difference in emphasis. We have a different first-order logic for each \emph{signature.} G\"odel just supposes there are infinitely many $n$-ary functional variables (relation symbols) for each $n$. Perhaps for G\"odel, a \emph{property} is a singulary relation; a \emph{relation,} a relation of more than one argument. An $n$-ary relation on a set $A$ determines the function from $A^n$ to $2$ that takes the value $1$ at a point $\vec a$ of $A^n$ if and only if the relation actually holds at that point. I shall quote G\"odel's ten numbered theorems \emph{verbatim,} with my own commentary interspersed. \textsc{Theorem I.} \emph{Every valid formula of the restricted functional calculus is provable.} The proof of this will not be completed until after Theorem VI. G\"odel explains validity in another footnote. In our terminology, $\phi(\vec x)$ is \textbf{valid} if $\Forall{\vec x}\phi(\vec x)$ is true in every structure; by ``well-known theorems'' (of L\"owenheim and Skolem, presumably), it is enough to be true in every countable structure. The formula $\phi(\vec x)$ is \textbf{satisfiable} if $\Exists{\vec x}\phi(\vec x)$ is true in some structure. Thus $\phi$ is valid if and only if $\lnot\phi$ is not satisfiable. G\"odel's ``system of axioms'' is as follows. Again I translate into current symbolism; my convention on parentheses is Shoenfield's \cite[pp.\ 17--8]{MR1809685}: $\lor$ is more binding than $\lto$, and of two occurrences of one of these, the occurrence on the right is the more binding. The ``undefined primitive notions'' are $\lor$, $\lnot$, and $\forall x$, and, ``By means of these, $\land$, $\lto$, $\liff$, and $\exists x$ can be defined in a well-known way.'' The axioms are: \begin{enumerate}[1)] \item $P\lor P\lto P$, \item $P\lto P\lor Q$, \item $P\lor Q\lto Q\lor P$, \item $(P\lto Q)\lto R\lor P\lto R\lor Q$, \item $\Forall xF(x)\lto F(y)$, \item $\Forall x(P\lor F(x))\lto P\lor\Forall xF(x)$. \end{enumerate} The rules of inference are: \begin{description} \item[Detachment:] from $\phi$ and $\phi\lto\psi$, infer $\psi$. \item[Substitution:] ``The rule of substitution for propositional and functional variables.'' Above, $P$, $Q$, and $R$ are propositional variables, and $F(x)$ is a functional variable. Church discusses this. There are six axioms above; by substitution we derive infinitely many validities. Alternatively, we could replace the axioms with \emph{axiom schemes,} and forget about the rule of substitution. \item[Generalization:] From $\phi(x)$, infer $\Forall x\phi(x)$. \item[Change of variables:] ``Individual variables (free or bound) may be replaced by any others, so long as this does not cause overlapping of the scopes of variables denoted by the same sign.'' \end{description} G\"odel points out in a note that Russell and Whitehead do not formulate ``all of these'' explicitly. G\"odel has noted in the first paragraph that we already have completeness for propositional calculus. Thus, I say, we might as well replace the first four axioms above with one axiom scheme, giving us every tautology of the propositional calculus. G\"odel himself will re-assert propositional completeness as one of the lemmas below. We could be more explicit about change of variables: \begin{itemize} \item $\Forall x\phi(x)\lto\Forall y\phi(y)$ is an axiom ($y$ being substitutable for $x$ in $\phi$). \item From $\phi(x)$, infer $\phi(y)$, provided $x$ is not a free variable of any hypotheses of a proof. \end{itemize} G\"odel states some lemmas without proof: \begin{enumerate} \item For every tuple $\vec x$ of variables,%%%%% \footnote{As G\"odel explains, he uses lower-case German letters like $\mathfrak x$, $\mathfrak y$, $\mathfrak u$, $\mathfrak v$, ``and so on,'' for these tuples.} \begin{gather*} \Forall{\vec x}\phi(\vec x)\lto\Exists{\vec x}\phi(\vec x),\\ \Forall{\vec x}\phi(\vec x)\land\Exists{\vec x}\psi(\vec x) \lto\Exists{\vec x}(\phi(\vec x)\land\psi(\vec x)),\\ \Forall{\vec x}\lnot\phi(\vec x)\liff\lnot\Exists{\vec x}\phi(\vec x). \end{gather*} Note that G\"odel has not formally explained the meaning of $\exists x$; perhaps the ``well-known'' definition alluded to above is that $\Exists x\phi$ means $\lnot\Forall x\lnot\phi$. \item For every $n$ in $\upomega$, for every permutation $\sigma$ of $n$, for every $n$-tuple $\vec x$ of variables, \begin{equation*} \Exists{\vec x}\phi(\vec x)\lto\Exists{(\vec x\circ\sigma)}\phi(\vec x). \end{equation*} In my notation, $\vec x$ is a function from $n$ to the set of variables. \item Assuming $\vec x$ is injective as such a function, even if $\vec y$ is not, \begin{equation*} \Forall{\vec x}\phi(\vec x)\lto\Forall{\vec y}\phi(\vec y). \end{equation*} \item {}[Blending of quantifiers in a conjunction or disjunction: see the proof of Theorem III. G\"odel apparently neglects to say that the variables must be distinct.] \item For every $\phi$ there is $\phi'$ in \emph{normal form} such that $\phi\liff\phi'$. G\"odel does not define normal form, but only refers again to Hilbert and Ackermann. Evidently it is as defined by Skolem in his 1920 paper \cite{Skolem-LS}: in our terms, a formula is in \textbf{normal form} if it is an \textbf{open} (quantifier-free) formula, preceded by some (or no) existential quantifiers, preceded by some (or no) universal quantifiers. \item If $\phi\liff\phi'$, then $\psi\liff\psi'$, where $\phi$ is a subformula of $\psi$, and $\psi'$ results from $\psi$ by replacing $\phi$ with $\phi'$. \item Completeness of the first four axioms for propositional calculus. Note that G\"odel does not mention any rules of inference at this point. \end{enumerate} Theorem I is equivalent to: \textsc{Theorem II.} \emph{Every formula of the restricted functional calculus is either refutable or satisfiable} (and moreover satisfiable in the [\emph{sic}] denumerable domain of individuals). \textbf{Refutable} means having provable negation. The ``class'' (set) $\mathfrak K$ consists of \emph{sentences} in normal form of the more precise form \begin{equation*} \Forall x\dots\;\Exists y\phi. \end{equation*} That is, the sentence must have at least one universal and one existential quantifier. \textsc{Theorem III.} \emph{If every $\mathfrak K$-expression is either refutable or satisfiable, so is every expression.} A note says the restriction to ``the denumerable domain of individuals'' will be implicit. \begin{proof} By definition, $\phi(\vec x)$ is satisfiable if and only if $\Exists{\vec x}\phi(\vec x)$ is satisfiable. If $\phi(\vec x)$ is refutable, this means $\lnot\phi(\vec x)$ is provable, so $\Forall{\vec x}\lnot\phi(\vec x)$ is provable by Generalization, so $\Exists{\vec x}\phi(\vec x)$ is refutable. If $\Exists{\vec x}\phi(\vec x)$ is refutable, this means $\lnot\Exists{\vec x}\phi(\vec x)$ is provable, so that $\Forall{\vec x}\lnot\phi(\vec x)$ is provable, and therefore $\lnot\phi(\vec x)$ is provable by Axiom 5, that is, $\phi(\vec x)$ is refutable. It is now enough to prove the claim for \emph{sentences.} By Lemma 5, it is enough to prove the claim for \emph{normal sentences.} Let $\mathsf Q\;\phi$ be such. If $x$ and $y$ are distinct variables not occuring in $\mathsf Q$, and $R$ is some singulary relation symbol, then the sentence \begin{equation*} \Forall x\lnot Rx\lor\Exists yRy \end{equation*} is a tautology and is therefore provable by Lemma 7. But by Lemma 4, the sentence \begin{equation*} \Forall x\lnot Rx\lor\Exists yRy\liff \Forall x\Exists y(\lnot Rx\lor Ry) \end{equation*} is provable, by Lemma 4, and therefore so are the following: \begin{gather*} \Forall x\Exists y(\lnot Rx\lor Ry),\\ \mathsf Q\;\phi \liff\mathsf Q\;\phi\land\Forall x\Exists y(\lnot Rx\lor Ry),\\ \mathsf Q\;\phi\land\Forall x\Exists y(\lnot Rx\lor Ry) \liff\Forall x\mathsf Q\;\Exists y(\phi\land(\lnot Rx\lor Ry)),\\ \mathsf Q\;\phi \liff\Forall x\mathsf Q\;\Exists y(\phi\land(\lnot Rx\lor Ry)). \end{gather*} The sentence $\Forall x\mathsf Q\;\Exists y(\phi\land(\lnot Rx\lor Ry))$ being in $\mathfrak K$, we are done. \end{proof} The \textbf{degree} of a sentence in $\mathfrak K$ is the number of blocks of universal quantifiers. \textsc{Theorem IV.} \emph{If every expression of degree $k$ is either satisfiable or refutable, so is every expression of degree $k+1$.} \begin{proof} Suppose $\sigma$ is the sentence $\Forall{\vec x}\Exists{\vec y}\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi$. Suppose $R$ (taking arguments of the length of $\vec x\vec y$) does not occur in $\phi$. Then \begin{equation*} (R\vec x\vec y\lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi) \liff\Forall{\vec u}\Exists{\vec v}\mathsf Q\;(R\vec x\vec y\lto\phi). \end{equation*} We make the following abbreviations: \begin{align*} \tau_1&\text{ is } \Forall{\vec x'}\Exists{\vec y'}R\vec x'\vec y'\land \Forall{\vec x}\Forall{\vec y} (R\vec x\vec y\lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi),\\ \tau_2&\text{ is } \Forall{\vec x'}\Exists{\vec y'}R\vec x'\vec y'\land \Forall{\vec x}\Forall{\vec y} \Forall{\vec u}\Exists{\vec v}\mathsf Q\;(R\vec x\vec y\lto\phi),\\ \tau_3&\text{ is } \Forall{\vec x'}\Forall{\vec x}\Forall{\vec y}\Forall{\vec u} \Exists{\vec y'}\Exists{\vec v}\mathsf Q\; (R\vec x'\vec y'\land(R\vec x\vec y\lto\phi)). \end{align*} ``Obviously'' $\tau_1\lto\sigma$. By Lemma 6, $\tau_1\liff\tau_2$; by Lemma 4, $\tau_2\liff\tau_3$. We may assume as an inductive hypothesis that $\tau_3$ is either satisfiable or refutable. If $\tau_3$ is satisfiable, then so is $\sigma$. If $\tau_3$ is refutable, then so is $\tau_1$. In particular, taking $R\vec x\vec y$ to be $\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi$, we have \begin{equation*} \lnot (\Forall{\vec x}\Exists{\vec y} \Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi\land \Forall{\vec x}\Forall{\vec y} (\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi \lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi)). \end{equation*} But $\Forall{\vec x}\Forall{\vec y} (\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi \lto\Forall{\vec u}\Exists{\vec v}\mathsf Q\;\phi)$, and therefore $\lnot\sigma$. \end{proof} ``It now remains only to prove'' \textsc{Theorem V.} \emph{Every formula [\emph{sic}] of degree 1 is either satisfiable or refutable.} Let $\Forall{\vec x}\Exists{\vec y}\phi(\vec x,\vec y)$ be such a formula, that is, sentence, where $\vec x$ is an $r$-tuple, and $\vec y$ is an $s$-tuple, of distinct variables. All variables come from the sequence $(x_k\colon k\in\upomega)$. Let \begin{gather*} \phi_1\text{ be }\phi(\vec x^1,\vec y^1),\\ \phi_2\text{ be }\phi(\vec x^2,\vec y^2)\land\phi_1,\\ \makebox[4cm]{\dotfill}\\ \phi_n\text{ be }\phi(\vec x^n,\vec y^n)\land\phi_{n-1}. \end{gather*} Here $k\mapsto\vec x^k$ is the bijection from $\N$ to the set of $r$-tuples of variables such that, writing $\vec x^k$ as $(x_{k(i)}\colon i