A Set Theory Prover 
Within Theorema

Wolfgang.Windsteiger@RISC.Uni-Linz.ac.at
RISC Institute
Hagenberg, Austria.

The P-C-S Paradigm for Theorema Provers

Proving is seen (mainly) as a sequence of alternating phases of

It is a heuristic method that aims on automated proofs in natural style.

Proving

({{Given:, a collection of formulae A (the assumptions),}, { , a formula G (the goal,  the conclusion).}, {Find:, P, such that:}, { , if G is a consequence of A then P should contain a 
convincing argument (logically correct,  sound,  
                  understandable),
why G necessarily follows from A.}})

Example

Goal: {1} ⊆ ℕ.
Assumptions: Definition of ⊆, ℕ, {…}, and 1.

Proof: Take a ∈ {1}, which forces a = 1, hence a ∈ ℕ.

Computing

({{Given:, a collection of formulae A (the assumptions), }, { , a term T or a formula F.}, {Find:, a term (OverTilde[T]) or a formula (OverTilde[F]), such that:}, { , ({{(a), T = (OverTilde[T]) is a consequence of A and}, { , (OverTilde[T]) is (in some sense) simpler than T.}})}, {or,  }, { , ({{(b), F⇔(OverTilde[F]) is a consequence of A and}, { , (OverTilde[F]) is (in some sense) simpler than F.}})}})

Example

Compute :  {x ∈ ℕ | 
            x ≥ 
              3} ⋂ {x ∈ 𝕀 | 
              x < 6} .

Result :  {3, 4, 
          5}.

Compute :  
      4 ∈ {x ∈ ℕ | 
              x ≥ 
                3} ⋂ {x ∈ 𝕀 | 
                x < 6}  .   .

Result :  
      4 ∈ {3, 4, 
            5}  or True.

Compute :  ((sin(2  x) cos(
                x))/((cos(x))^3)) .

Result: ((2 sin(x))/(cos(x))) or  2 tan(x).

Solving

({{Given:, a collection of formulae A (the assumptions),}, { , a formula G of the form \(∃ \+\(x\&_\)\ \(\(P\_x\&_\)\(.\)\)\)}, {Find:, a proof of G by giving S, such that 
S ⊆ {⟨y⟩|\(P\_\(x\&_ -> y\)\) can be derived from A} and |S|≥1.}})

Example

Goal: (Underscript[∃ , x, y ∈ ℝ])(Underscript[((x^2) + (y^2) = 
                1), (Underscript[⏟, (Subscript[P, x, y])])]).
Assumptions: Axioms of the domain of real numbers.

S = {⟨0, 
            1⟩}  (since (Subscript[P, x, y -> 0, 1]) gives 1 = 1) or

\(TraditionalForm\`S = {⟨0, 
            1⟩, ⟨1, 
            0⟩, ⟨\@2\/2, \@2\/2⟩, ⟨\@2\/2, \(-\(\@2\/2\)\)⟩}\), or

S = {⟨cos(t), 
              sin(t)⟩ | 0 ≤ t < 2  π} 
  (since (Subscript[P, x, y -> cos(t), sin(t)]) gives ((cos(t))^2) + ((sin(t))^2) = 1, which holds for any 0 ≤ t < 2  π).

Provers in Theorema

In general, a Theorema Prover is structured as follows:

The Set Theory PCS Prover

User Prover: SetTheoryPCSProver combines:

Special Provers (set theory specific):

STP: The Set Theory Prove module handles set theoretic expressions in the goal.

STKBR: The Set Theory KnowledgeBase Rewriting module infers new knowledge from set theoretic expressions in the assumptions.

STC: The Set Theory Compute module performs (set theoretic) simplifications in the goal and in the assumptions.

STS: The Set Theory Solve module tries to solve existential goals.
In the context of set theory, such goals appear naturally e.g. in goals of the form \(TraditionalForm\`y ∈ {T\_x\( | \+x\)P\_x}\), which immediately lead to (Underscript[∃ , x]) y = (Subscript[T, x])  ∧  (Subscript[P, x]).

Other special provers involved from general PCS proving (see Buchberger):

Basic natural deduction.

Recognition of terminal proof cases.

Rewriting with respect to formulae in the knowledge base.

System Demonstration

General Outline of the Case Study

We investigate interactions of the following notions:

Computing

The semantics of the Theorema language allows computations on certain expressions.

Definition[\("reflexivity", 
      any[Rel, S], 
reflexive\_S[
          Rel] : \(\(⇔\)\(∀ \+\(x ∈ S\)⟨x, x⟩ ∈ Rel\)\)\)]

Definition[\("symmetry", 
      any[Rel, S], 
symmetric\_S[
          Rel] : \(\(⇔\)\(∀ \+\(x, y ∈ S\)\((⟨x, y⟩ ∈ 
                  Rel \[Implies] ⟨y, 
                    x⟩ ∈ Rel)\)\)\)\)]

Definition["Equivalence class", 
      any[x, A, 
        R], 
(Subscript[class, A, R])[
          x] := {a ∈ 
              A \[VerticalSeparator] ⟨a, 
                x⟩ ∈ R}]

Compute[\(reflexive\_{\(i\)\( | \+\(i = 0, …, 10\)\)}[{⟨i, 
                j⟩\( | \+\(i, j = 0, …, 
                  10\)\)\((Mod[i, 5] = Mod[j, 5])\)}]\),\(using -> ⟨Definition["reflexivity"]⟩\),built–in->⟨Built–in["Sets"][SetOf],Built–in["Quantifiers"],Built–in["Connectives"]⟩]

Compute[\(reflexive\_{\(i\)\( | \+\(i = 0, …, 10\)\)}[{⟨i, 
                j⟩\( | \+\(i, j = 0, …, 
                  10\)\)\((Mod[i, 5] = Mod[j, 5])\)}]\),\(using -> ⟨Definition["reflexivity"]⟩\),built–in->⟨Built–in["Sets"],Built–in["Quantifiers"],Built–in["Connectives"]⟩]

\(Compute[
      symmetric\_{\(i\)\( | \+\(i = 0, …, 10\)\)}[{⟨i, 
              j⟩\( | \+\(i, j = 0, …, 
                10\)\)\((Mod[i, 5] = Mod[j, 5])\)}], 
      using -> ⟨Definition["symmetry"]⟩, 
      built–in -> ⟨Built–in["Sets"], 
          Built–in["Quantifiers"], 
          Built–in["Connectives"], \(Built–in["Tuples"]\)[
            AngleBracket]⟩]\)

\(Compute[
      class\_\({\(i\)\( | \+\(i = 0, …, 10\)\)}, {⟨i, j⟩\( | \+\(i, j = 0, …, 10\)\)\((Mod[i, 5] = Mod[j, 5])\)}\)[4], 
      using -> ⟨Definition["Equivalence class"]⟩, 
      built–in -> ⟨Built–in["Sets"], 
          Built–in["Quantifiers"]⟩]\)

\(Compute[
      class\_\({\(i\)\( | \+\(i = 0, …, 10\)\)}, {⟨i, j⟩\( | \+\(i, j = 0, …, 10\)\)\((Mod[i, 5] = Mod[j, 5])\)}\)[4] = {9, 4}, 
      using -> ⟨Definition["Equivalence class"]⟩, 
      built–in -> ⟨Built–in["Sets"], 
          Built–in["Quantifiers"]⟩]\)

Clear[™Subscript]

Computing ⊆ Proving

Goal: Make use of knowledge provided by the semantics of the language during proving!

Reflexivity

Proposition[\("R reflexive on finite set", 
reflexive\_{\(i\)\( | \+\(i = 0, …, 10\)\)}[{⟨i, 
              j⟩\( | \+\(i, j = 0, …, 
                10\)\)\((Mod[i, 5] = Mod[j, 5])\)}]\)]

Prove[Proposition["R reflexive on finite set"],
using -> 
          Definition["reflexivity"],
built–in -> 
          Built–in["Quantifiers"],
by -> SetTheoryPCSProver,ProverOptions -> {TransformRanges -> False, 
              SimplifyFormula -> False, 
              DisableProver -> {STP, PND}}]

Here is the proof.

Symmetry

Proposition[\("R symmetric on finite set", 
symmetric\_{\(i\)\( | \+\(i = 0, …, 10\)\)}[{⟨i, 
              j⟩\( | \+\(i, j = 0, …, 
                10\)\)\((Mod[i, 5] = Mod[j, 5])\)}]\)]

Prove[Proposition["R symmetric on finite set"],
using -> Definition["symmetry"],
\(built–in -> ⟨Built–in["Quantifiers"], 
            Built–in["Tuples"]⟩\),
by -> SetTheoryPCSProver,ProverOptions -> {TransformRanges -> False, 
              SimplifyFormula -> False, 
              DisableProver -> {STP, STKBR, PND}}]

Here is the proof.

Computing ⊂ Proving

Reflexivity

\(Compute[
      reflexive\_ℕ[{⟨i, 
              j⟩\( | \+\(i, 
                j ∈ ℕ\)\)\((Mod[i, 5] = 
                Mod[j, 5])\)}], 
      using -> ⟨Definition["reflexivity"]⟩, 
      built–in -> ⟨Built–in["Sets"], 
          Built–in["Quantifiers"], 
          Built–in["Connectives"], \(Built–in["Tuples"]\)[
            AngleBracket]⟩]\)

Symmetry

\(Compute[
      symmetric\_ℕ[{⟨i, 
              j⟩\( | \+\(i, 
                j ∈ ℕ\)\)\((Mod[i, 5] = 
                Mod[j, 5])\)}], 
      using -> ⟨Definition["symmetry"]⟩, 
      built–in -> ⟨Built–in["Sets"], 
          Built–in["Quantifiers"], 
          Built–in["Connectives"], \(Built–in["Tuples"]\)[
            AngleBracket]⟩]\)

Representation of Equivalence Class

\(Compute[
      class\_\(ℕ, {⟨i, j⟩\( | \+\(i, j ∈ ℕ\)\)\((Mod[i, 5] = Mod[j, 5])\)}\)[
          4] = {\(4 + 
              5  k\)\( | \+\(k ∈ ℕ\)\)}, 
      using -> ⟨Definition["Equivalence class"]⟩, 
      built–in -> ⟨Built–in["Sets"], 
          Built–in["Quantifiers"]⟩]\)

Solving ⊆ Proving

Goal: Make use of available algebraic solution techniques during proving!

Reflexivity

Proposition[\("R reflexive on ℕ", 
reflexive\_ℕ[{⟨i, 
              j⟩\( | \+\(i, 
                j ∈ ℕ\)\)\((Mod[i, 5] = 
                Mod[j, 5])\)}]\)]

Prove[Proposition["R reflexive on ℕ"],
using -> 
          Definition["reflexivity"],
built–in -> 
          Built–in["Tuples"],
by -> SetTheoryPCSProver,ProverOptions -> {ApplyBuiltIns -> {"kb"}, 
              SimplifyFormula -> False, 
              DisableProver -> {STC, PND}}]

Here is the proof.

Symmetry

Proposition[\("R symmetric on ℕ", 
symmetric\_ℕ[{⟨i, 
              j⟩\( | \+\(i, 
                j ∈ ℕ\)\)\((Mod[i, 5] = 
                Mod[j, 5])\)}]\)]

Prove[Proposition["R symmetric on ℕ"],
using -> 
          Definition["symmetry"],
built–in -> 
          Built–in["Tuples"],
by -> SetTheoryPCSProver,ProverOptions -> {ApplyBuiltIns -> {"kb"}, 
              SimplifyFormula -> False, 
              DisableProver -> {STC, PND}}]

Here is the proof.

Computing ⋃ Solving ⊆ Proving

Representation of Equivalence Class

Proposition[\("class representation", 
class\_\(ℕ, {⟨i, j⟩\( | \+\(i, j ∈ ℕ\)\)\((Mod[i, 5] = Mod[j, 5])\)}\)[
          4] ⊇ {\(4 + 
              5  k\)\( | \+\(k ∈ ℕ\)\)}\)]

We will need two auxiliary Lemmata:

Lemma["Natural Numbers", 
      any[i, j, 
        k ∈ ℕ], 
i + 
          k j ∈ ℕ]

Lemma["Mod Properties", 
      any[i, j, k], 
Mod[i + j k, j] = i]

SetGlobals[SearchDepth -> 50]

Prove[Proposition["class representation"],using -> ⟨Lemma["Natural \
Numbers"], Lemma["Mod Properties"], 
              Definition["Equivalence class"]⟩,
\(built–in -> ⟨Built–in["Numbers"], 
              Built–in["Number Domains"], 
              Built–in["Tuples"]⟩\),
by -> SetTheoryPCSProver,
ProverOptions -> {SimplifyFormula -> False, 
                DisableProver -> {PND}}]//Timing

Here is the proof.

Transitivity of Induced Relation

Proposition["induced by partition is transitive", 
      any[P], with[
        is–partition[P]], 
is–transitive[
        induced–relation[P]]]

Auxiliary:

Proposition[\("intersecting are equal", any[P], 
      with[is–partition[
          P]], 
∀ \+\(X, Y ∈ P\)\((X ⋂ Y ≠ ∅ \[Implies] \((X = Y)\))\)\)]

SetGlobals[SearchDepth -> 80]

Prove[Proposition["induced by partition is transitive"],\(using -> ⟨Definition["transitivity"], 
              Definition["induced relation"], 
              Proposition["intersecting are equal"]⟩\),
built–in -> 
            Built–in["Tuples"],
by -> SetTheoryPCSProver,
\(ProverOptions -> {GRWTarget -> {"goal", "kb"}, ModusPonensKB -> True, 
                InferMembershipIntersection -> True, 
                AllowIntroduceQuantifiers -> True, 
                ApplyBuiltIns -> {"kb"}, 
                DisableProver -> {PND}}\)]//Timing

Here is the proof.

Conclusion

Two main theorems in the area of equivalence relations, induced relations, and partitions

Theorem["induced by factor set of R is R itself", any[R], 
      with[is–equivalence[
          R]], 
induced–relation[
          factor–set[R]] = R]

Theorem["factor set of induced by P is P itself", any[P], 
      with[is–partition[P]], 
factor–set[
          induced–relation[P]] = P]

together with all auxiliary propositions and lemmata starting from the definitions have been proved completely automatized using the Set Theory PCS Prover. After this case study we think that structuring proving into alternating cycles of P-C-S

is a feasible approach for structuring automated theorem provers,

gives naturally structured proofs, AND MOST IMPORTANTLY

opens the door for incorporating powerful known solving and computing techniques from the field of Computer-Algebra (Gröbner bases, Collins' algorithm, Gauss method, Lazy Narrowing, etc.) into automated theorem provers.