Post-completeness

A logical theory is Post-complete (or Hilbert-Post complete) just if there is no proper, consistent extension of it.

In propositional systems

Suppose, for example, that the theory \mathcal{T} is comprised of some kind of propositional formula \phi, with judgement \Gamma \vdash_\mathcal{T} \phi, where \Gamma is a list or set of assumptions. (This judgement could come from a Hilbert system, natural deduction, and so on.)

Suppose we have a formula \alpha that does not follow from the theory, i.e. \not\vdash_\mathcal{T} \alpha. Are we allowed to construct a theory \mathcal{T} + \alpha, by adding \alpha to the axioms of \mathcal{T}? We are, but we do not know if it will be consistent.

If \mathcal{T} is Hilbert-Post complete, then we will have that adding any \alpha that does not already follow from \mathcal{T} to the axioms of the theory leads to a contradiction. That is, \vdash_{\mathcal{T} + \alpha} \bot.

In particular, classical propositional logic is Hilbert-Post complete.

In first-order and higher-order logics

First-order logic is not Hilbert-Post complete.

Presumably the same is true of higher-order logics.

In \lambda-calculus

The study of \lambda-calculus is usually concerned with equational theories between terms of the calculus. These have judgements of the form

	\Gamma \vdash M = N : A

where \Gamma is a context consisting of free variables, M, N are terms, and A is a type. In the case of the untyped \lambda-calculus, all free variables and terms have the same type, so the judgement is simply written as

	\vdash M = N

Hence, questions about Hilbert-Post completeness take the following form: how many more terms can we axiomatically equate before everything is equal?

Untyped \lambda-calculus

Hilbert-Post completeness has mostly been studied in terms of the untyped \lambda-calculus.

In particular, the theory \mathcal{H}^\star, which equates any two untyped terms just if they are both solvable or unsolveable when plugged into any context, is Hilbert-Post complete: see the classic book by Barendregt §16.2, 1984.