 First-order consistency

A first-order theory is consistent when it has no formal proof of a contradiction. This syntactic property concerns the specified calculus; its equivalence with having a first-order model uses the completeness theorem.