Axiomatic semantics: Typed lambda calculus

p 304, Discussion
It is well known that ordinary mathematical discourse is not entirely
formal, as this would be unbearable tedious[...].

The need for a delicate balance between rigor and informality is well
accepted in ordinary mathematics, and in most cases this works to the
satisfaction of everyone concerned.

Two important properties are:

- Soundness: a theory is sound if for no well-formed formula f the
  rules allow deriving both f and non f.
- Completeness: a theory is complete if for any well-formed formula f
  the rules allow the derivation of f or non f.

Soundness is also called "non-contradiction" or "consistency".

One would [...] expect all "good" theories to be complete, but this is
not the case: among the most important results of mathematical logic
are the incompleteness of such theories as predicate calculus or
arithmetic.