Two New(ish) Surveys on Gödel's Incompleteness Theorems

Gödel’s incompleteness theorems have many variants: semantic vs. syntactic versions, which specific theory is taken as basic, what model of computability is used, which logical system is assumed to underlie the provability relation, how syntax is arithmetized, what hypotheses the theorem itself uses (soundness, consistency, \(\omega\)-consistency, etc.). These result in trade-offs regarding simplicity of the proof, but also scope of application and consequences that can be drawn.

There are two new(ish) and super-useful surveys of proofs of Gödel’s incompleteness theorem that review these versions and their limitations and scope. The first is by Lev Beklemishev:

Л.Д. Беклемишев (2010). Теоремы Гёделя о неполноте и границы их применимости. I., Успехи Математических Наук 65(5) 61-104. PDF.

English translation:

L. D. Beklemishev (2010). Gödel incompleteness theorems and the limits of their applicability. I., Russian Mathematical Surveys 65(5) 857-898. PDF

The second is by Bernd Buldt:

B. Buldt (2014). The scope of Gödel’s first incompleteness theorem, Logica Universalis. forthcoming. PDF preprint

Lev’s is mathematically more exhaustive and more technical; Bernd’s is less technical and also goes into philosophically relevant aspects such as Gödel’s theorems for system with non-classical underlying logics.

Possible Postdoc on Genesis of Mathematical Knowledge

Via the APMP list:
Expressions of interest are invited for a postdoc grant (financed by Junta de Andalucia) associated with the following research project: 
“THE GENESIS OF MATHEMATICAL KNOWLEDGE: COGNITION, HISTORY, PRACTICES” (P12-HUM-1216). IP: Jose Ferreiros
Contact: josef@us.es
The grant consists in a 2-year research contract to be held at the University of Sevilla. Salary is in the range of 84000 euros for 24 months. Holders must have obtained their PhD before start of the grant,  [update:] by 2014 and at most 10 years ago (exceptions apply in case of motherhood). They will be doing research along the lines of this interdisciplinary project — devoted to philosophy of mathematics, links between cognition and mathematical practice, and the interactions logic/mathematics and physics/mathematics.  Knowledge of Spanish is desirable, although it is not a formal requirement.
The call for these grants, issued by Junta de Andalucia, will be open from early December, allowing for only 15 days. Applications will be made to the Junta de Andalucia, but we invite candidates to get in touch with the project IP in advance, so that we can coordinate and assist you.  If you are interested in applying, please contact the IP by email as soon as possible, explaining briefly your situation and interests. Keep in mind that the selection will be made on the basis of fit between the candidate’s research project and the topic of the project.

Kalmár's Compleness Proof

Dana Scott’s proof reminded commenter “fbou” of Kalmár’s 1935 completeness proof. (Original paper in German on the Hungarian Kalmár site.) Mendelsohn’s Introduction to Mathematical Logic also uses this to prove completeness of propositional logic. Here it is (slightly corrected):

We need the following lemma:

Let \(v\) be a truth-value assignment to the propositional variables in \(\phi\), and let \(p^v\) be \(p\) if \(v(p) = T\) and \(\lnot p\) if \(v(p) = F\). If \(v\) makes \(\phi\) true, then \[p_1^v, \dots, p_n^v \vdash \phi.\]

This is proved by induction on complexity of \(\phi\).

If \(\phi\) is a tautology, then any \(v\) satisfies \(\phi\). If \(v\) is a truth value assignment to \(p_1, \dots, p_n\), let \(\Gamma(v,k) = {p_1^v, \dots, p_k^v}\). Let’s show that for all \(v\) and \(k = n, \dots, 0\), \(\Gamma(v, k) \vdash \phi\). If \(k = n\), then \(\Gamma(v, n) \vdash \phi\) by the lemma and the assumption that \(\phi\) is a tautology, i.e., true for all \(v\). Suppose the claim holds for \(k+1\). This means in particular \(\Gamma(v, k) \cup {p_{k+1}} \vdash \phi\) and \(\Gamma(v, k) \cup {\lnot p_{k+1}} \vdash \phi\) for any given \(v\). By the deduction theorem, we get \(\Gamma(v, k) \vdash p_{k+1} \to \phi\) and \(\Gamma(v, k) \vdash \lnot p_{k+1} \to \phi\). By \(\vdash p_{k+1} \lor \lnot p_{k+1}\) and proof by cases, we get \(\Gamma(v, k) \vdash \phi\).  The theorem then follows since \(\Gamma(v, 0) = \emptyset\).

Notes:

  • The inductive proof of the lemma requires as inductive hypothesis both the claim and the corresponding claim for the case where \(v\) makes \(\phi\) false (i.e., that then \(p_1^v, \dots, p_n^v \vdash \lnot \phi\)). Kalmár did not include the constants \(T\) and \(F\) in the language, but if you would, then Scott’s (iii) would be a special case of the lemma.
  • Scott’s proof does not require the deduction theorem, but does require proof of substitutability of equivalents.

Dana Scott's Favorite Completeness Proof

Last week I gave my decision problem talk at Berkeley. I briefly mentioned the 1917/18 Hilbert/Bernays completeness proof for propositional logic. It (as well as Post’s 1921 completeness proof) made essential use of provable equivalence of a formula with its conjunctive normal form. Dana Scott asked who first gave (something like) the following simple completeness proof for propositional logic:

We want to show that a propositional formula is provable from a standard axiomatic set-up iff it is a tautology. A simple corollary will show that if it is not provable, then adding it as an axiom will make all formulae provable.

  1. If a formula is provable, then it is a tautology.

Because the axioms are tautologies and the rules of inference (substitution and detachment) preserve being a tautology. The argument is by induction on the length of the proof.

  1. If a formula is not provable, then it is not a tautology.

We need three lemmata about provable formulae. The symbols \(T\) and \(F\) are for true and false. We write negation here as \(\lnot p\).

  1. $\vdash p \rightarrow [\phi(p) \leftrightarrow \phi(T)]$.
  2. $\vdash \lnot p \rightarrow [\phi(p) \leftrightarrow \phi(F) ]$.
  3. If \(\phi\) has no propositional variables, then either \(\vdash \phi \leftrightarrow T\) or \(\vdash \phi \leftrightarrow F\).

All these are proved by induction on the structure of \(\phi\) and require checking principles of substitutivity of equivalences. And I am claiming here this is less work than formulating and proving how to transform formulae into conjunctive normal form.

From (i) and (ii) it follows that: \[\vdash \phi(p) \leftrightarrow [ [ p \rightarrow \phi(T) ] \land [\lnot p \rightarrow \phi(F)] ],\] because we can show generally: \[\vdash \psi \leftrightarrow [ [ p \rightarrow \psi ] \land [ \lnot p \rightarrow \psi ] ].\] Thus, we can conclude: if \(\vdash \phi(T)\) and \(\vdash \phi(F)\), then \(\vdash \phi(p)\). Hence if \(\phi(p)\) is not provable, then one of \(\phi(T)\), \(\phi(F)\) is not provable.

So, if a formula \(\phi\) has no propositional variables and is not provable, then by (iii), \(\phi \leftrightarrow F\). So it is not a tautology. Arguing now by induction on the number of propositional variables in the formula, if \(\phi(p)\) is not provable, then one of \(\phi(T)\), \(\phi(F)\) is not a tautology. And so \(\phi(p)\) is not a tautology. QED

I don’t know the answer. Do you?

The only thing it reminded me of was this old paper which shows that all tautologies in \(n\) variables can be proved in \(f(n)\) steps using the schema of equivalence. It uses a similar idea: evaluate formulas without variables to truth values, and then inductively generate the tautologies by induction on the number of variables and excluded middle.  You could turn that proof into a completeness proof by establishing for a given calculus that the required equivalences and formulas are provable. 

Dana’s proof is a lot simpler, though. Thanks to him for allowing me to post his question here.

Lectures on the Epsilon Calculus

Back in 2009, I taught a short course on the epsilon calculus at the Vienna University of Technology.  I wrote up some of the material, intending to turn them into something longer.  I haven’t had time to do that, but someone might find what I did helpful. So I put it up on arXiv:

http://arxiv.org/abs/1411.3629