maximally consistent


A set Δ of well-formed formulas (wff) is maximally consistent if Δ is consistent and any consistent supersetMathworldPlanetmath of it is itself: ΔΓ with Γ consistent implies Γ=Δ.

Below are some basic properties of a maximally consistent set Δ:

  1. 1.

    Δ is deductively closed (Δ is a theory): ΔA iff AΔ.

  2. 2.

    Δ is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath: ΔA or Δ¬A for any wff A.

  3. 3.

    for any wff A, either AΔ or ¬AΔ.

  4. 4.

    If AΔ, then Δ{A} is not consistent.

  5. 5.

    Δ is a logic: Δ contains all theoremsMathworldPlanetmath and is closed under modus ponensMathworldPlanetmath.

  6. 6.

    Δ.

  7. 7.

    ABΔ iff AΔ implies BΔ.

  8. 8.

    ABΔ iff AΔ and BΔ.

  9. 9.

    ABΔ iff AΔ or BΔ.

Proof.
  1. 1.

    If AΔ, then clearly ΔA. Conversely, suppose ΔA. Let be a deductionMathworldPlanetmathPlanetmath of A from Δ, and Γ:=Δ{A}. Suppose ΓB. Let 1 be a deduction of B from Γ, then ,1 is a deduction of B from Δ, so ΔB. Since Δ⊬, Γ⊬, so Γ is consistent. Since Δ is maximal, Γ=Δ, or AΔ.

  2. 2.

    Suppose Δ⊬A, then AΔ by 1. Then Δ{A} is not consistent (since Δ is maximal), which means Δ,A, or ΔA, or Δ¬A.

  3. 3.

    If AΔ, then Δ⊬A by 1, so Δ¬A by 2, and therefore ¬AΔ by 1 again.

  4. 4.

    If AΔ, then ¬AΔ by 3., so that ¬A,A, is a deduction of from Δ{A}, showing that Δ{A} is not consistent.

  5. 5.

    If A is a theorem, then ΔA, so that AΔ by 1. If AΔ and ABΔ, then A,AB,B is a deduction of B from Δ, so BΔ by 1.

  6. 6.

    This is true for any consistent set.

  7. 7.

    Suppose ABΔ. If AΔ, then BΔ since Δ is closed under modus ponens. Conversely, suppose AΔ implies BΔ. This means that Δ,AB. Then ΔAB by the deduction theoremMathworldPlanetmath, and therefore ABΔ by 1.

  8. 8.

    Suppose ABΔ, then by modus ponens on theorems ABA and ABB, we get A,BΔ, since Δ is a logic by 5. Conversely, suppose A,BΔ, then by modus ponens twice on theorem A(BAB), we get ABΔ by 5.

  9. 9.

    Suppose ABΔ. Then ¬(¬A¬B)Δ by the definition of , so ¬A¬BΔ by 3., which means ¬AΔ or ¬BΔ by the contrapositive of 8, or AΔ or BΔ by 3. Conversely, suppose AΔ or BΔ. Then by modus ponens on theorems AAB or BAB respectively, we get ABΔ by 5.

The converses of 2 and 3 above are true too, and they provide alternative definitions of maximal consistency.

  1. 1.

    any complete consistent theory is maximally consistent.

  2. 2.

    any consistent set satisfying the condition in 3 above is maximally consistent.

Proof.

Suppose Δ is complete consistent. Let Γ be a consistent superset of Δ. Γ is also complete. If AΓ-Δ, then ΓA, so Γ⊬¬A since Γ is consistent. But then Δ⊬¬A since Γ is a superset of Δ, which means ΔA since Δ is complete. But then AΔ since Δ is deductively closed, which is a contradictionMathworldPlanetmathPlanetmath. Hence Δ is maximal.

Next, suppose Δ is consistent satisfying the condition: either AΔ or ¬AΔ for any wff A. Suppose Γ is a consistent superset of Δ. If AΓ-Δ, then ¬AΔ by assumption, which means ¬AΓ since Γ is a superset of Δ. But then both A and ¬A are deducible from Γ, contradicting the assumption that Γ is consistent. Therefore, Γ is not a proper superset of Δ, or Γ=Δ. ∎

Remarks.

  • In the converse of 2, we require that Δ be a theory, for there are complete consistent sets that are not deductively closed. One such an example is the set V of all propositional variables: it can be shown that for every wff A, exactly one of VA or V¬A holds.

  • So far, none of the above actually tell us that a maximally consistent set exists. However, by Zorn’s lemma, it is not hard to see that such a set does exist. For more detail, see here (http://planetmath.org/LindenbaumsLemma).

  • There is also a semantic characterizationMathworldPlanetmath of a maximally consistent set: a set is maximally consistent iff there is a unique valuationPlanetmathPlanetmath v such that v(A)=1 for every wff A in the set (see here (http://planetmath.org/CompactnessTheoremForClassicalPropositionalLogic)).

Title maximally consistent
Canonical name MaximallyConsistent
Date of creation 2013-03-22 19:35:13
Last modified on 2013-03-22 19:35:13
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 10
Author CWoo (3771)
Entry type Definition
Classification msc 03B05
Classification msc 03B10
Classification msc 03B99
Classification msc 03B45
Related topic FirstOrderTheories
Defines complete
\@unrecurse