Proof of completeness and soundness of a proof system

Question

As stated here, https://en.wikipedia.org/wiki/List_of_rules_of_inference, "a set of rules can be used to infer any valid conclusion if it is complete, while never inferring an invalid conclusion, if it is sound"

I would like to know how is it possible to assess if a given proof system (set of inference rules) is both consistent and complete. Is there a decidable algorithm (an algorithm which halts) for determining this?

Answer 1

Proof Systems

A proof system is a Formal system with logical axioms (possibly none) and rules of inference (at least one).

Some examples :

• Hilbert-style proof system : usually more than one (logical) axioms and few rules : modus ponens and generalization. See Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 109, for a system with few axioms and only modus ponens as inference rule;

• Natural deduction : no (logical) axiom and many rules, typically a couple for every connective. See Jan von Plato, Elements of Logical Reasoning (2013), page 31.

Other proof systems are : sequent calculus, resolution, tableaux method (or truth tree).

Completeness and Soundness

Regarding completeness and soundness, they are relative to a semantics suitable for the language of the proof system : truth tables for propositional calculus, mathematical structures for first-order logic (see e.g. Enderton, page 80).

See Enderton, page 131 :

In this section we establish two major theorems: the soundness of our deductive calculus :

if $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$

and its completeness :

if $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$.

Although our deductive calculus was chosen in a somewhat arbitrary way, the significant fact is that some such deductive calculus is sound and complete.

Soundness means : the proof system can derive as conclusion ($\varphi$) only formulae that are logical consequence of the formulae contained into the set of premises ($\Gamma$).

Completeness means : the proof system can derive as conclusion ($\varphi$) all the formulae that are logical consequence of the formulae contained into the set of premises ($\Gamma$).

Soundness implies consistency; consider the case of propositional logic : no formula and its negation are both tautologies. But the soundness of the calculus means that a formula which is not a tautology is not derivable; thus, no pair of contradictory formulae is derivable.

Decidability

Regarding decidability, this property is relative to the set of formulae derivable within the calculus; the answer is positive for propositional calculus : the truth table is a (very inefficient) algorithm to verify validity (i.e.checking for "tautologuesness").

For first-order logic, the answer is negative (Enderton, page 142-145):

ENUMERABILITY THEOREM For a reasonable language, the set of valid formulae can be effectively enumerated. [...]

It should be remarked that our proofs of enumerability cannot, in general, be strengthened to proofs of decidability. For almost all languages the set of validities is not decidable. (See Church’s Theorem.)

Answer 2

No theory containing at least the peano axioms can prove its own consistency (proven by Gödel). But there can be a stronger theory proving the consistency of the weaker theory. The catch is, to prove the consistency of the stronger theory, you need an even stronger one.

ZFC is believed to be consistence and can be used to prove the consistency of PA.

To be both consistent and complete, a theory must be weaker than PA, for example the Presburger arithmetic has been proven to be both complete and consistent.