2

I've been reading patrick suppes’ an introduction to logic, and the rules of inference mentioned in it, like universal specification, conditional proof, etc. haven't been proven to be sound or complete in that book. So how are you supposed to prove these rules?

3
  • Try asking this on Math.SE - it's a question on model theory and not philosophy. – Mozibur Ullah Jun 3 '20 at 18:51
  • You can prove that a rule is sound, but an individual rule won't be complete, only a system of rules can be. – lemontree Jun 3 '20 at 21:17
  • 1
    To @MoziburUllah’s point, consider a text like Philosophy and Model Theory (Button/Walsh, Oxford 2018) if you’re interested in the philosophical implications of model-theoretic ideas – Joseph Weissman Jun 4 '20 at 14:25
6

First of all, you won't show that a single rule of inference is sound and complete, but rather that the system of rules as a whole is.

Proving soundness

Γ ⊢ A   ⇒   Γ ⊨ A

-- which essentially states that your system doesn't produce nonsense --

is relatively easy: One proves the soundness of each axiom and rule by demonstrating that the axiom is a tautology or, respectively, that the rule is a semantically valid inference; then uses the induction principle to establish that if each of the individual rules are fine, the soundness will be preserved when plugging them together to a larger derivation.

Proving completeness

Γ ⊨ A   ⇒   Γ ⊢ A

-- which states that every logical inference will be captured by the system --

is trickier. The usual proof proceeds as follows:

Proving by contradiction:
Assume Γ ⊨ A, but not Γ ⊢ A.
Then Γ ∪ {¬A} is not satisfiable (= has no model), but consistent (= no contradiction can be derived from it).
However, it can be shown that any consistent set of formulas is also satisfiable. (*)
Contradiction, so Γ ⊨ A   ⇒   Γ ⊢ A.

The proof of (*) is the complicated part.

For propositional logic, one goes by extending a consistent set of formulas to a maximally consistent one, i.e. one where no more formulas can be added without making the set inconsistent; the proof that this consistent extension is possible makes use of the fact that the set of formulas of propositional logic is enumerable. Maximally consistent sets have certain properties, eventually making it possible to show that consistent sets of formulas are satisfiable, i.e., (*).

For predicate logic, where quantifiers need to be taken care of, one starts by constructing from the assumed-to-be-consistent set of premises its so-called theory, which is a set of formulas that is closed under deduction, i.e. everything that can be derived from the set and everything that can be derived from those derived things and so on, is included in the theory.
Theories are then transformed into so-called Henkin theories, in which, essentially, for every existential claim ∃xA(x) there ought to be a name c referencing a concrete object (= a witness) that satisfies that property, A(c).
Lindenbaum's lemma then states that consistent theories can be turned into complete consistent theories, which are theories that decide every formula, i.e. for every formula of the language, a complete theory can either prove the formula or its negation. (Note that this is parallel to the notion of maximal consistency from above.)
For these complete consistent Henkin theories the model existence lemma holds, which states that a consistent set of formulas has a model.
After limiting the language back to the one before henkinization, (*) follows as a corollary.


A detailled proof of soundness and completeness can be found:

  • for sequent calculus: e.g. in H.-D. Ebbinghaus/J. Flum/W. Thomas, Mathematical Logic
  • for natural deduction: e.g. in D. van Dalen, Logic and structure
  • for Hilbert-style calculus: e.g. in H. Enderton, A mathematical introduction to logic

The proofs of soundness for the indvidual rules of course will look different for different rule systems, but the proof idea as a whole is the same across all these presentations.

Not the answer you're looking for? Browse other questions tagged or ask your own question.