A logical theory is Post-complete (or Hilbert-Post complete) just if there is no proper, consistent extension of it.
Suppose, for example, that the theory is comprised of some kind of propositional formula , with judgement , where 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 that does not follow from the theory, i.e. . Are we allowed to construct a theory , by adding to the axioms of ? We are, but we do not know if it will be consistent.
If is Hilbert-Post complete, then we will have that adding any that does not already follow from to the axioms of the theory leads to a contradiction. That is, .
In particular, classical propositional logic is Hilbert-Post complete.
First-order logic is not Hilbert-Post complete.
Presumably the same is true of higher-order logics.
The study of -calculus is usually concerned with equational theories between terms of the calculus. These have judgements of the form
where is a context consisting of free variables, are terms, and is a type. In the case of the untyped -calculus, all free variables and terms have the same type, so the judgement is simply written as
Hence, questions about Hilbert-Post completeness take the following form: how many more terms can we axiomatically equate before everything is equal?
Hilbert-Post completeness has mostly been studied in terms of the untyped -calculus.
In particular, the theory , 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].