TH∃OREM∀:
A System for Formal Mathematics

Bruno Buchberger
RISC, Austria

Acknowledgement to Theorema Group: 
T. Jebelean, W. Windsteiger, T. Kutsia, M. Rosenkranz, F. Piroi;  and Ph.D. students.

The Goal of Theorema

Support Mathematical Theory Exploration

Mathematical Theory Exploration

Starting from a body of knowledge on some concepts      (e.g. +, * on numbers and functions)

invent (axioms, definitions for) new concepts (operations: predicates, functions)   (e.g. limit)

invent and prove properties of notions

invent problems about notions

invent methods (algorithms) for problems and prove their correctness

compute (apply algorithms to data)

organize, store, and retrieve knowledge

Current computer algebra systems support some of these aspects.

Current reasoning systems support some other of these aspects.

Goal: Support all these aspects.
Calculemus, MKM etc. are research networks that aim at creating integrated systems. 
Group members: MIZAR, OMEGA, EDIN, ISABELLE, NUPRL, ...
Theorema is one of the (founding) groups of these networks.

A Never Ending Endeavor on Two Floors

Theorema : A Coherent Frame for Mathematical Theory Exploration

One logic frame: a version of predicate logic.

One software technologic frame: implementation language ("meta language") is Mathematica:

A. Theorema reasoners are programmed in Mathematica (in the future: in Theorema itself)

B. Mathematica as a front-end (flexible syntax, hierarchical notebooks, graphics etc.)

Example: Syntax and Manipulating Mathematical Texts

Initialize Theorema

Needs["Theorema`"];

Predicate Logic Formulae, Labels, and Keywords

Definition[\("limit:", any[f, a], 
	
      limit[f, a]⟺\ \(\(∀ \+ϵ\)\+\(ϵ > 0\)\(∃ \+N\(\(∀ \+n\)\+\(n ≥ N\)\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ\)\)\)\)]

Note that logic "application" is denoted by brackets in Theorema!

Definition["limit:"]

Definition["limit:"]  // InputForm

The identifier spaces of Theorema and Mathematica are kept disjoint!

Users can program their own syntax!

Proposition[\("limit of sum", 
      any[f, a, g, 
        b], 
	\((limit[f, a] ∧ 
            limit[g, b])\)\ \ \ \ \  \[Implies] \ \ \ \ \ limit[f + g, 
          a + b]\)]

Definition[\("+:", 
      any[f, g, x], 
	\((f + g)\)[x] = f[x] + g[x]\)]

Lemma[\("|+|", 
      any[x, y, a, 
        b, δ, ϵ], 
	\((\[LeftBracketingBar]\((x + 
                    y)\) - \((a + 
                    b)\)\[RightBracketingBar] < \((δ + ϵ)\))\)\ \ \ \ ⟸\ \ \ \((\[LeftBracketingBar]x - a\[RightBracketingBar] < δ ∧ \[LeftBracketingBar]y - 
                  b\[RightBracketingBar] < ϵ)\)\)]

Lemma[\("max", any[m, M1, M2], 
	
      m ≥ 
          max[M1, M2]\ \ \ \ \  \[Implies] \ \ \ \ \ \((m ≥ 
              M1 ∧ m ≥ M2)\)\)]

Combining Formulae to "Theories"

Theory["limit",
	({{Definition["limit:"]}, {Definition["+:"]}, {Lemma["|+|"]}, {Lemma["max"]}})]

Theory["limit"]

Theory["Test",
({{Theory["limit"]}, {Lemma["max"] }})]

Logicographic Symbols (Invent Arbitrary New Symbols and Two-dimensional Nesting)

Logicographic Symbols: In Theorema, users can invent, design, declare, and use their own mathematical symobls:

Example: Computing (Within Predicate Logic)

Programs are Predicate Logic Formulae

Definition["addition",any[m, n],
	({{m + 0 = m, " +0:"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + .:"}})]

Definition["addition"] // InputForm

\(Compute[\(\(\(0\^+\)\^+\)\^+\) + \(\(0\^+\)\^+\), 
      using -> Definition["addition"]]\)

\(Compute[\(\(\(0\^+\)\^+\)\^+\) + \(\(0\^+\)\^+\), 
      using -> ⟨⟩]\)

Definition["multiplication",any[m, n],
	({{m*0 = 0, " *0:"}, {\(m*\(n\^+\) = \((m*n)\) + m\), " * .:"}})]

\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(0\^+\)\^+\), 
      using -> Definition["addition"]]\)

No hidden knowledge is used!

\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\), 
      using -> ⟨Definition["addition"], 
          Definition["multiplication"]⟩]\)

\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\), 
      using -> ⟨Definition["multiplication"]⟩]\)

Using the Theory Construct

Theory["arithmetic",
({{Definition["addition"]}, {Definition["multiplication"]}})]

\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\), 
      using -> Theory["arithmetic"]]\)

Defining Hidden Knowledge

Use[Theory["arithmetic"]]

\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\)]\)

Use[⟨⟩]

\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\)]\)

Avoiding to Write "Compute" All the Time

"Theorema Computing Sessions" possible like in Mathematica, Maple, etc.  Not discussed here.

Using Built-in Knowledge Explicitly

Compute[3*4, using -> Theory["arithmetic"]]

Compute[3*4, using -> Theory["arithmetic"]] // 
      InputForm

Built–in["Mathematica decimal arithmetic",
({{™Times -> Times}, {™Plus -> Plus}})]

Compute[3*4, 
      using -> ⟨Built–in["Mathematica decimal \
arithmetic"]⟩]

Compute[3 + 4*5!, 
      using -> ⟨Built–in["Mathematica decimal \
arithmetic"]⟩]

?? Built–in

\(Compute[3 + 4*\(5!\), 
      using -> ⟨Built–in["Numbers"]⟩]\)

Thus, if one wants, the full power of the Mathematica algorithm library can be used from within Theorema programs.

Sequence Variables

(For the metamathematics of sequence variables see [Kutsia, Buchberger, MKM 2004])

Sequence variables allow flexible arity operations.

Definition["reverse",\(any[x, x\&_]\),
	({{r[⟨⟩] = ⟨⟩, "reverse empty"}, {\(r[⟨x, x\&_⟩] = 
                r[⟨x\&_⟩]⌢x\), "reverse general"}})]

\(Compute[r[⟨⟩], 
      using -> ⟨Definition["reverse"]⟩]\)

\(Compute[r[⟨3, 2, 4, 2, 1⟩], 
      using -> ⟨Definition["reverse"]⟩]\)

Definition["compose",\(any[x, x\&_]\),
	({{\(x⌣⟨x\&_⟩ = ⟨x, x\&_⟩\), "prepend"}, {\(⟨x\&_⟩⌢
                  x = ⟨x\&_, x⟩\), "append"}, {\(⟨x\&_⟩⌢⟨y\&_⟩ = ⟨x\&_, 
                  y\&_⟩\), "concatenate"}})]

Compute[r[⟨3, 2, 4, 2, 1⟩], 
      using -> ⟨Definition["compose"], 
          Definition["reverse"]⟩]

Sequence Variables Allow Complicated Pattern Matching

Definition["first lines of a propositional prover",\(any[g, g1, g2, a\&_, b, b1, b2, b\&_, c\&_, d\&_, k]\),
	({{\(prove[
                  g, ⟨a\&_, g, b\&_⟩] = 
                T\), "goal is among assumptions"}, {\(prove[
                  g, ⟨a\&_, b, c\&_, N[b], 
                    d\&_⟩] = T\), "contradicting assumptions"}, {prove[A[g1, g2], k] = and[prove[g1, k], prove[g2, k]], "prove conjunction"}, {\(prove[
                  g, ⟨a\&_, A[b1, b2], 
                    c\&_⟩] = 
                prove[g, ⟨a\&_, b1, b2, 
                    c\&_⟩]\), "use conjunction"}})]

Use[⟨Definition["first lines of a propositional \
prover"]⟩]

Compute[
      prove[X < Y, ⟨F[U, V], G[U], X < Y, 
          F[V, U]⟩]]

Compute[
      prove[X < Y, ⟨F[U, V], G[U], X > Y, 
          F[V, U]⟩]]

Compute[
      prove[X < Y, ⟨F[U, V], G[U], X > Y, N[G[U]], 
          F[V, U]⟩]]

Compute[
      prove[X < Y, ⟨F[U, V], G[U], X > Y, N[G[A]], 
          F[V, U]⟩]]

Compute[
      prove[A[X < Y, X > Y], ⟨F[U, V], G[U], X > Y, 
          N[G[A]], F[V, U]⟩]]

Bounded Quantifiers

Use[⟨⟩]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], 
        Built–in["Sets"]⟩]

Compute[(Underscript[∀ , i = -10, …, 10])i ≤ 
          0]

Compute[(Underscript[∃ , i = -10, …, 10])i ≤ 
          0]

\(Compute[{\ \((2  i)\)\( | \+\(i ∈ {1, 2, 3}\)\)}]\)

\(Compute[{i\( | \+\(i = 1, …, 20\)\)is–prime[
            i]}]\)

Compute[{2, 3, 1, 2, 3} = {1, 2, 3, 3, 3}]

Compute[{2, 3, 1, 2, 3}]

Compute[{1, 2, 3, 3, 3}]

Compute[{1, 2, 1, 3} = {2, 1, 4, 3}]

Definition["some quantifier programs",any[n, X, Y, A, B],
({{IP[
                  n] ⇔ ((Underscript[∀ , d = 1, …, n])(d ∣ 
                          n)⟹((d = 
                              1) ∨ (d = 
                              n)))

              }, {\(X⊕Y := ⟨\ \((X\_i + 
                        Y\_i)\)\( | \+\(i = 
                          1, …, \[LeftBracketingBar]X\[RightBracketingBar]\)\)⟩\)}, {X ⪯ Y := 
                where[n = \[LeftBracketingBar]X\[RightBracketingBar], (Underscript[∀ , i = 1, …, n])((Subscript[X, i]) ≤ 
                        (Subscript[Y, i]))]

              }, {\(A⊖B := {\ 
                  x\( | \+\(x ∈ A\)\)\((x ∉ B)\)}\)}, {A ⊆ 
                  B := (Underscript[∀ , x ∈ A])x ∈ B}, {𝔓[A]:={({{{{}}, ⇐, A = {}}, {\(where[a = æ[A], 
                          P = 𝔓[A⊖{a}], \ 
	
                          P ⋃ {\(({a} ⋃ 
                                    B)\)\( | \+\(B ∈ P\)\)}]\), ⇐, otherwise}})}}})]

Principle: Predicate logic definitions and (proved) propositions can also be read as programs!

Use[⟨⟩]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Definition["some quantifier programs"]⟩]

Compute[IP[1]]

Compute[IP[28]]

Compute[⟨1, 1, 1, 1, 
          1⟩⊕⟨3, 3, 3, 3, 
          3⟩]

Compute[⟨1, 1, 1, 1, 
          1⟩ ⪯ ⟨3, 3, 3, 
          3, 3⟩]

Compute[⟨1, 1, 8, 1, 
          1⟩ ⪯ ⟨3, 3, 3, 
          3, 3⟩]

Compute[{1, 2, 3}⊖{2, 3, 4, 5}]

Compute[{3, 2, 33} ⊆ {2, 3, 4, 5}]

Compute[𝔓[{}]]

Compute[𝔓[{3}]]

Compute[𝔓[{1, 3}]]

Compute[𝔓[{1, 3, 4, 8}]]

Functors

Some Internal Preparations

The following two Mathematica functions will be needed in the definition of arithmetic modulo the prime p:

Clear[PFInverse, PFQuotient]
PFInverse[x_, 
        p_] := ExtendedGCD[x, p][[2, 1]]
PFQuotient[x_, y_, p_] := Mod[x PFInverse[y, p], p]

PFQuotient[1, 3, 5]

In the current version of Theorema, the following Mathematica function definition must be entered

\[LeftBracketingBar]⟨x___?
            IsSequenceFree⟩\[RightBracketingBar] := 
      Length[{x}]

for completing a definition in the Theorema package.

Now we make a couple of Mathematica functions available in Theorema, including the two new ones from above,

Built–in["Mathematica general functions",
({{is–even -> EvenQ}, {is–odd -> OddQ}, {mod -> Mod}, {gcd -> GCD}, {lcm -> LCM}, {sign -> Sign}, {maximum -> Max}, {quotient -> Quotient}, {pf–inverse -> PFInverse}, {pf–quotient -> PFQuotient}})]

The following function 'pairs' computes a list consisting of all pairs of elements in a given list:

Definition["Theorema general functions",\(any[a, x, x\&_]\),
({{pairs[⟨⟩] = ⟨⟩}, {\(pairs[⟨x, 
                    x\&_⟩] = ⟨\(⟨x, ⟨x\&_⟩\_i⟩\)\( \[VerticalSeparator] \+\(i = 
                            1, …, \[LeftBracketingBar]⟨x\&_⟩\[RightBracketingBar]\)\)⟩ ≍ 
                  pairs[⟨x\&_⟩]\)}})]

For example,

Use[⟨Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Connectives"], 
        Built–in["Quantifiers"], 
        Definition["Theorema general functions"]⟩]

Compute[ pairs[⟨⟩]]

Compute[ pairs[⟨1⟩]]

Compute[ 
      pairs[⟨1, 2, 3, 4, 5⟩]]

Compute[ 
      pairs[⟨1, 2, 1, 1, 2⟩]]

What are Functors?

Functors are functions that map domains into domains.

A domain is a carrier together with operations on the carrier.

How can we code all the "enormous" information in a domain into one object?

In "ordinary" algebra: A domain D is a tuple  ( carrier, operation1, operation2, ...).

In Theorema (adopting the notion of "interpretation" from model theory):

D maps operators into operations.

D[+] is a (binary) operation.

D[+][x,y]    is the operation D[+]  applied to x and y.  (We have Currying in Theorema.)

Syntax:  D[+][x,y], in Theorema, can be written in the form    x \(TraditionalForm\`+\+D\) y.

(Theorema functors are like SML functors but slightly more general: Carrier of D may be defined by arbitrary characteristic function (Underscript[χ, D]).)

A functor can now easily take entire domains D, ... as an arguments: For example functor F that describes the Cartesian product of two domains D and E:

F[D, E][+][    ⟨a, 
          b⟩,   ⟨x, 
          y⟩   ]:=   ⟨     D[+][a, x],      E[+][b, 
          y]  ⟩

or

F[D, 
        E]  :=     (Underscript[æ, N])       (Underscript[∀ , a, b, x, y])     N[+][    ⟨a, 
                b⟩,   ⟨x, 
                y⟩   ]:=   ⟨     D[+][a, x],      E[+][b, 
            y]  ⟩

or, with some syntax,

\(F[D, 
        E]\  := \ \ \ \ \(\(æ\+N\ \ \ \ \ \ \ \(∀ \+\(a, b, x, y\)\ \ \ \ \ ⟨a, 
                b⟩\ \ \( + \+N\)\ \ ⟨x, 
                y⟩\)\)\(:=\)\(\ \ \ \)\(⟨\ \ \ \ \ a\( + \+D\)x, \ \ \ \ \ b\( + \+E\)y\ \ ⟩\)\(\ \)\)\)

or, with some more syntax,

F[D, E] :=    Functor[ N,       any[a, b, x, y],    
 ({{\(⟨a, 
                      b⟩\ \ \( + \+N\)\ \ ⟨x, 
                      y⟩ := \ \ \ ⟨\ \ \ \ \ a\( + \+D\)x, \ \ \ \ \ b\( + \+E\)y\ \ ⟩\)}, {\(⟨a, 
                      b⟩\ \ \(*\+N\)\ \ ⟨x, 
                      y⟩ := \ \ \ ⟨\ \ \ \ \ a\(*\+D\)x, \ \ \ \ \ b\(*\+E\)y\ \ ⟩\)}, {....}}) ]

or, even,

F[D, E] :=    Functor[ N,       any[a, b, x, y, O],    
 ({{⟨a, 
                      b⟩  (Underscript[O, N])  ⟨x, 
                      y⟩ :=    ⟨     a (Underscript[O, D]) x,      b (Underscript[O, E]) y  ⟩}, {....}}) ]

This is the form implemented in Theorema.

Why Are Functors Useful?

Computational Aspect: Economy of programming. No code repetition for building up "towers of domains".

Logical Aspect: Economy of proving. No proof repetition when building  up "towers of domains".

If D is a monoid                 then   Cartesian[D,D] is a monoid.

If D is a Groebner ring      then   Poly[D]   is a Groebner ring.

If D is a partition                then   Equ[D]    is an  equivalence.

....

is–monoid[D]⇔(Underscript[((Underscript[∀ , x, y, z])), (Underscript[ϵ, D])[
              x], (Underscript[ϵ, D])[y], (Underscript[ϵ, D])[z]])(({{x (Underscript[∘, D])(y (Underscript[∘, D])z) = (x (Underscript[∘, D])y) (Underscript[∘, D])y}, {x (Underscript[∘, D])(Underscript[1, D]) = x}}))

is–monoid defines a "category"

The three fundamental notions for structuring mathematics:  domains, categories, functors.

"Conservation Theorems":  

          If  domain D is in category A 
          
                     then F[D], the result of applying functor F to D, is in category B.

Theorema provides some tools for organizing such proofs.

Example: Rational Numbers

Definition

Definition["rational numbers field" ,any[],
rational–numbers–field[]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                              x] ⇔ 
                            is–rational[x]}, {(Underscript[0, N]) = 0}, {(Underscript[1, N]) = 1}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {(Underscript[inverse, N])[x] = 1/x}, {\(x\(/\+N\)y = x/y\)}})}})
	]]

Construct Domain

Definition["ℚ0", ℚ0 = 
        rational–numbers–field[]]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["ℚ0"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Apply for Computation

Compute[(Underscript[ϵ, ℚ])0[2.0005]]

Compute[(Underscript[ϵ, ℚ])0[2/5]]

Compute[(Underscript[0, ℚ])0]

Compute[(Underscript[1, ℚ])0]

\(Compute[5/2\( + \+ℚ0\)3]\)

\(Compute[\(-\+ℚ0\(-2\)\)/3]\)

\(Compute[3\( - \+ℚ0\)\(-2\)/3]\)

\(Compute[5\(*\+ℚ0\)3/4]\)

Compute[(Underscript[inverse, ℚ])0[3/4]]

\(Compute[\(7/
          5\)\(/\+ℚ0\)\((\(-2\)/3)\)]\)

\(Compute[\(7/5\)\(/\+ℚ\)\((\(-2\)/3)\)]\)

Example: Prime Fields

Definition

Definition["prime field" ,any[p],
prime–field[p]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                                  x]⇔∧{({{is–integer[x]}, {0 ≤ x}, {x < p}})} }, {(Underscript[0, N]) = 0}, {(Underscript[1, N]) = 1}, {\(x\( + \+N\)y = mod[x + y, p]\)}, {\(\(-\+N x\) = mod[\(-x\), p]\)}, {\(x\( - \+N\)y = mod[x - y, p]\)}, {\(x\(*\+N\)y = mod[x*y, p]\)}, {(Underscript[inverse, N])[x] = pf–inverse[x, p]}, {\(x\(/\+N\)y = pf–quotient[x, y, p]\)}})}})
	]]

Remark on the operations in the functor: (Underscript[inverse, N]) and \(\(/\+N\)\) refer to the function pf–inverse and pf–quotient, respectively, which we linked to the Mathematica function PFInverse and PFQuotient by the 'Built-in' construct. PFInverse and PFQuotient were defined above in Mathematica.

Construct Domain

Definition["𝔽5", 𝔽5 = 
        prime–field[5]]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["prime field"]}, {Definition["𝔽5"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Apply for Computation

Compute[(Underscript[ϵ, 𝔽])5[0]]

Compute[(Underscript[ϵ, 𝔽])5[4]]

Compute[(Underscript[ϵ, 𝔽])5[
        5]]

Compute[(Underscript[ϵ, 𝔽])5[-1]]

Compute[(Underscript[0, 𝔽])5]

Compute[(Underscript[1, 𝔽])5]

\(Compute[4\( + \+𝔽5\)1]\)

\(Compute[\(-\+𝔽5\((2)\)\)]\)

\(Compute[1\( - \+𝔽5\)\((2)\)]\)

\(Compute[4\(*\+𝔽5\)3]\)

Compute[(Underscript[inverse, 𝔽])5[3]]

\(Compute[4\(/\+𝔽5\)3]\)

Example: Power Products as Tupels

Definition

Definition["tuples division semigroup lexical",any[k, D],
tuples–division–semigroup–lexical[k]   =
Functor[N,\(any[m, m\&_, n, n\&_, x, y, i]\),
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[
                                x]⇔∧{({{is–tuple[x]}, {\[LeftBracketingBar]x\[RightBracketingBar] = k}, {(Underscript[∀ , i = 
                                        1, …, k])∧{({{is–integer[(Subscript[x, i])]}, {(Subscript[x, i]) ≥ 0}})} }})} }, {(Underscript[1, N]) = ⟨0 (Underscript[\[VerticalSeparator] , i = 1, …, k])⟩}, {\(x\(*\+N\)y = ⟨\(x\_i + 
                                  y\_i\)\( \[VerticalSeparator] \+\(i = 
                                      1, …, 
                                    k\)\)⟩\)}, {\(x\(/\+N\)y = ⟨\(x\_i - 
                                  y\_i\)\( \[VerticalSeparator] \+\(i = 
                                      1, …, 
                                    k\)\)⟩\)}, {(x  (Underscript[∣ , N])y)⟺(Underscript[∀ , i = 1, …, k])(Subscript[x, i]) ≤ (Subscript[y, i])}, {(Underscript[lcm, N])[x, y]     = ⟨maximum[(Subscript[x, i]), 
                                  (Subscript[y, i])] (Underscript[\[VerticalSeparator] , i = 
                                      1, …, 
                                    k])⟩}, {\(⟨⟩\( > \+N\)⟨⟩ ⇔ False\)}, {\(⟨m, 
                                m\&_⟩\( > \+N\)⟨n, n\&_⟩\)⇔{({{True, ⇐, m > n}, {\(⟨m\&_⟩\( > \+N\)⟨n\&_⟩\), ⇐, (m = n)}, {False, ⇐, otherwise}})} }, {(Underscript[deg, N])[x]  (* 
                              the degree of x *)  = (∑_(i = 1, …, k))(Subscript[x, i])}})}})
	]]

Note: ' (Underscript[∣ , N])' must be typed '\ [VerticalBar]'.

Construct Domain

Definition[\("𝕋3", 
	𝕋3 = 
        tuples–division–semigroup–lexical[3]\)]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["tuples division semigroup lexical"]}, {Definition["𝕋3"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Apply for Computation

Compute[(Underscript[ϵ, 𝕋])3[⟨1, 0, 
          2⟩]]

Compute[(Underscript[ϵ, 𝕋])3[⟨1, 
          0, -2⟩]]

Compute[(Underscript[ϵ, 𝕋])3[⟨1, 0, 
          2, 4⟩]]

Compute[(Underscript[1, 𝕋])3]

\(Compute[⟨1, 2, 
          4⟩\(*\+𝕋3\)⟨2, 0, 2⟩]\)

Compute[⟨0, 0, 
          0⟩ (Underscript[∣ , 𝕋])3⟨0, 0, 0⟩]

Compute[⟨0, 4, 
          1⟩ (Underscript[∣ , 𝕋])3⟨0, 5, 3⟩]

Compute[⟨0, 4, 
          4⟩ (Underscript[∣ , 𝕋])3⟨0, 5, 3⟩]

Compute[⟨0, 5, 
          1⟩ (Underscript[∣ , 𝕋])3⟨0, 5, 0⟩]

\(Compute[⟨55, 2, 
          4⟩\(/\+𝕋3\)⟨2, 0, 2⟩]\)

Compute[
      (Underscript[lcm, 𝕋])3[⟨55, 2, 
          4⟩, ⟨2, 0, 
          2⟩]]

Compute[
      (Underscript[lcm, 𝕋])3[⟨55, 2, 
          4⟩, ⟨2, 20, 
          9⟩]]

\(Compute[⟨55, 2, 
          4⟩\( > \+𝕋3\)⟨2, 0, 2⟩]\)

\(Compute[⟨55, 2, 
          4⟩\( > \+𝕋3\)⟨55, 2, 4⟩]\)

\(Compute[⟨55, 2, 
          4⟩\( > \+𝕋3\)⟨55, 3, 4⟩]\)

\(Compute[⟨55, 3, 
          4⟩\( > \+𝕋3\)⟨55, 3, 3⟩]\)

\(Compute[⟨55, 3, 
          4⟩\( > \+𝕋3\)⟨55, 3, 2342⟩]\)

Compute[
      (Underscript[deg, 𝕋])3[⟨55, 3, 
          4⟩]]

Example: Polynomials Over a Coefficient Domain and a Power Product Domain

Definition

Definition["reduction polynomials" ,any[C, T],
reduction–polynomials[C, T]   =

Functor[N,\(any[c, d, i, m, m\&_, n, n\&_, p, q, s, t]\),
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[p]⇔(∧{({{is–tuple[p]}, {(Underscript[∀ , j = 
                                        1, …, \[LeftBracketingBar]p\[RightBracketingBar]])(∧{({{is–tuple[(Subscript[p, j])]}, {\[LeftBracketingBar](Subscript[p, j])\[RightBracketingBar] = 2}, {(Underscript[ϵ, C])[(Subscript[(((Subscript[p, j]))), 1])]}, {(Underscript[ϵ, T])[(Subscript[(((Subscript[p, j]))), 2])]}, {(Subscript[(((Subscript[p, j]))), 1]) ≠ (Underscript[0, C])}})})}, {\(∀ \+\(j = 1, …, \[LeftBracketingBar]p\[RightBracketingBar] - 1\)\((p\_j)\)\_2\( > \+T\)\((p\_\(j + 1\))\)\_2\)}})})
}, {(Underscript[1, N]) = ⟨⟨(Underscript[1, C]), 
                                (Underscript[1, T])⟩⟩}, {(Underscript[0, N]) = ⟨⟩}, {\(⟨⟩\( + \+N\)q = q\)}, {\(p\( + \+N\)⟨⟩ = p\)}, {\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\( + \+N\)⟨⟨d, t⟩, 
                                n\&_⟩\)={({{\(⟨c, 
                                        s⟩⌣\((⟨m\&_⟩\( + \+N\)⟨⟨d, t⟩, n\&_⟩)\)\), ⇐, \(s\( > \+T\)t\)}, {\(⟨d, 
                                        t⟩⌣\((⟨⟨c, s⟩, 
                                        m\&_⟩\( + \+N\)⟨n\&_⟩)\)\), ⇐, \(t\( > \+T\)s\)}, {\(⟨c\( + \+C\)d, 
                                        s⟩⌣\((⟨m\&_⟩\( + \+N\)⟨n\&_⟩)\)\), ⇐, \(c ≠ \(-\+C 
                                        d\)\)}, {\(⟨m\&_⟩\( + \+N\)⟨n\&_⟩\), ⇐, otherwise}})} }, {\(\(-\+N⟨⟩\) = ⟨⟩\)}, {\(\(-\+N⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\) = ⟨\(-\+C c\), 
                                s⟩⌣\((\(-\+N⟨m\&_⟩\))\)\)}, {\(p\( - \+N\)q = p\( + \+N\)\((\(-\+N q\))\)\)}, {\(\(
\)\(⟨⟩\(*\+N\)q = ⟨⟩\)\)}, {\(p\(*\+N\)⟨⟩ = ⟨⟩\)}, {\(\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\(*\+N\)⟨⟨d, t⟩, 
                                n\&_⟩ = \((⟨⟨c\(*\+C\)d, 
                                      
                                      s\(*\+T\)t⟩⟩\( + \+N\)⟨⟨c, 
                                        s⟩⟩\(*\+\(\(N\)\(\ \)\)\)⟨n\&_⟩)\)\( + \+N\)⟨m\&_⟩\(*\+\(\(N\)\(\ \)\)\)⟨⟨d, t⟩, 
                                  n\&_⟩\)\(
\)
                          \)}, {\(\((⟨⟩\( > \+N\)p)\) ⇔ False\)}, {\(\((⟨⟨c, 
                                    s⟩, 
                                  m\&_⟩\( > \+N\)⟨⟩)\) ⇔ True\)}, {\((⟨⟨c, 
                                    s⟩, 
                                  m\&_⟩\( > \+N\)⟨⟨d, t⟩, 
                                  n\&_⟩)\)⇔(∨{({{\(s\( > \+T\)t\)}, {∧{({{s = t}, {\(c\( > \+C\)d\)}})} }, {∧{({{s = t}, {c = d}, {\(⟨m\&_⟩\( > \+N\)⟨n\&_⟩\)}})} }})} )}, {(Underscript[rdm, N])[⟨⟩, 
                              p] = (Underscript[0, N])}, {\(rdm\+N[⟨⟨c, 
                                  s⟩, 
                                m\&_⟩, ⟨⟩] = 0\+N\)}, {\(rdm\+N[⟨⟨c, s⟩, 
                                  m\&_⟩, ⟨⟨d, t⟩, 
                                  n\&_⟩]\)    =
{({{\(⟨⟨rdm\+C[c, d], s\(/\+T\)t⟩⟩\), ⇐, ∧{({{(Underscript[rdm, C])[c, d] ≠ (Underscript[0, C])}, {t (Underscript[∣ , T])s}})} }, {(Underscript[0, N]), ⇐, otherwise}})} 
}, {\(lcrd\+N[⟨⟨c, 
                                  s⟩, 
                                m\&_⟩, ⟨⟨d, t⟩, 
                                n\&_⟩]\ \  (*\ 
                              the\ least\ common\ reducible\ of\ ⟨⟨c, s⟩, 
                                  m\&_⟩\ modulo\ ⟨⟨d, t⟩, 
                                  n\&_⟩\ \ *) \  = 
⟨⟨lcrd\+C[c, d], 
                                lcm\+T[s, 
                                  t]⟩⟩\)}})}})
	]]

Some comments on the operations in the functor:

The element predicate (Underscript[ϵ, N]) expressed the fact that polynomials must be tuples of monomials that are ordered by \(TraditionalForm\`\( > \+T\)\). Monomials are tuples of length two with the first element being a non-zero coefficient taken from C and the second element being a "power product" taken from T.

Note that monomials must not have zero coefficients in this representation. Accordingly, the third clause in the definition of \(TraditionalForm\`+\+N\) in the definition checks for \(c ≠ \(-\+C d\)\) in order to avoid monomials with zeros in the sum of two polynomials!

The ordering \(TraditionalForm\`\( > \+N\)\) introduced on the polynomials is only partial even if the ordering \(TraditionalForm\`\( > \+T\)\) in the domain of power products is total.

The reduction multiplier \(TraditionalForm\`\(\(rdm\+N[⟨⟨c, 
              s⟩, 
            m\&_⟩, ⟨⟨d, t⟩, 
            n\&_⟩]\)\([\)\)\) of two non-zero polynomials is the singleton polynomial \(⟨⟨rdm\+C[c, d], 
          s\(/\+T\)t⟩⟩\) that consists of the only monomial \(⟨rdm\+C[c, d], s\(/\+T\)t⟩\) in case t (Underscript[∣ , T])s (t divides s in T). In all other cases we define it to be (Underscript[0, n]) so that in these cases no reduction takes place and, again, reducibility of p w.r.t. q can in all cases be decided by checking whether or not (Underscript[rdm, N])[ p, q] = (Underscript[0, N]).

The least common reducible \(lcrd\+N[⟨⟨c, 
            s⟩, 
          m\&_⟩, ⟨⟨d, 
            t⟩, n\&_⟩]\) is the singletion polynomial ⟨⟨(Underscript[lcrd, C])[c, d], 
          (Underscript[lcm, T])[s, t]⟩⟩ that consists of the only monomial ⟨(Underscript[lcrd, C])[c, d], 
        (Underscript[lcm, T])[s, t]⟩, where we refer to the (Underscript[lcrd, C])[c, d] in the coefficient domain C and to the (Underscript[lcm, T])[s, t] (the least common multiple) in the power product domain T. Of course, this reference to the least common multiple is the essence of Groebner bases construction in polynomial rings!

Attention: The quantifiers in the functor must not have bound variables that are identical to the bound variables in other functors. Hence, in this functor, we use 'j' as a bound variable in the definition of (Underscript[ϵ, N]) and not 'i' because 'i' was used in the functor 'tuples-division-semigroup-lexical'. This is a bug in the current implementation of functors in Theorema. It will be eliminated in the next version of Theorema.

Construction of Poly Domain in 3 Indeterminates over the Rationals

Definition["ℙ",
	({{𝕋03 = 
                tuples–division–semigroup–lexical[3]}, {ℚ0 = 
                rational–numbers–field[]}, {ℙ = 
                reduction–polynomials[ℚ0, 𝕋03]}})]

Theory["T",
	({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["tuples division semigroup lexical"]}, {Definition["reduction polynomials"]}, {Definition["ℙ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Element Operation

Compute[(Underscript[ϵ, ℙ])[⟨⟩]]

Compute[(Underscript[ϵ, ℙ])[
        (Underscript[1, ℙ])]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 11, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨6, 0, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨5, 11, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩, ⟨17, ⟨5, 1, 
              3⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨4, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 0, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨0, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[2]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2.3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 
              2, -2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 2⟩, 
            3⟩,   ⟨-1/
              2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 3, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 3, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Constants

Compute[(Underscript[1, ℙ])]

Compute[(Underscript[0, ℙ])]

Addition, Subtraction

\(Compute[⟨⟨2, ⟨3, 
              0, 4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \( + \+ℙ\)
⟨⟨5, ⟨3, 0, 
              3⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨1/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩]\)

\(Compute[⟨⟨2, ⟨3, 
              0, 4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \( - \+ℙ\)\(\(
\)\(⟨⟨5, ⟨3, 0, 
              3⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨1/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\)\)]\)

Multiplication

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 1\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨\(-5\), ⟨2, 2, 
              2⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

Ordering

\(Compute[\ 
      1\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ 
      1\+ℙ\ \ \( > \+ℙ\)\ 
        1\+ℙ]\)

\(Compute[\ 
      0\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ ⟨\(-1\)/2, ⟨0, 1, 
              3⟩⟩, \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 3, 
              2⟩⟩, \ ⟨\(-1\)/2, ⟨0, 1, 
              3⟩⟩, \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

Reduction Multiplier

Compute[
      (Underscript[rdm, ℙ])[
        (Underscript[0, ℙ]), ⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, 
        (Underscript[0, ℙ])]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨3, 0, 
              3⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 0, 
              2⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Least Common Reducible

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 0, 
              2⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨4, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 0, 
              2⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨4, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 3, 
              5⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Construction of Poly Domain in 2 Indeterminates over the Prime Field Modulo 5

Definition["ℙ",
	({{𝕋2 = 
                tuples–division–semigroup–lexical[2]}, {𝔽5 = prime–field[5]}, {ℙ = 
                reduction–polynomials[𝔽5, 𝕋2]}})]

Theory["T",
	({{Definition["Theorema general functions"]}, {Definition["prime field"]}, {Definition["tuples division semigroup lexical"]}, {Definition["reduction polynomials"]}, {Definition["ℙ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Apply for Computation

Compute[(Underscript[ϵ, ℙ])[⟨⟩]]

Compute[(Underscript[ϵ, ℙ])[
        (Underscript[1, ℙ])]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨7, ⟨3, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              7⟩⟩,   ⟨2/3, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              7⟩⟩,   ⟨3, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨33, 
              7⟩⟩,   ⟨3, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[1, ℙ])]

Compute[(Underscript[0, ℙ])]

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( + \+ℙ\)
⟨⟨4, ⟨7, 
              0⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨2, ⟨0, 
              1⟩⟩⟩]\)

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( - \+ℙ\)
⟨⟨4, ⟨7, 
              0⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨2, ⟨0, 
              1⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 1\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ 
      0\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨1, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨3, 
              1⟩⟩, \ \ ⟨1, ⟨1, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              1⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Example: Induction Proofs

Initialize Theorema Provers

Needs["Theorema`"];

Needs["Theorema`Provers`UserProvers`PCS`"]

SetGlobals[TraceLevel -> 0, DebugLevel -> 0, 
      SearchDepth -> 100, Prover -> PCS, 
      FormatMetas -> "Subscripted"]

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> Proved}];

$RecursionLimit = 1024;

$TmaSolveLevel = 3;

$NDDebug = False;

Off[General::spell]

Off[General::spell1]

SetGlobals[LabelStyle -> "Numeric", 
        Prover -> NNEqIndProver];
Needs["Theorema`Provers`Cascade`Cascade`"]; 
    Needs["Theorema`Provers`Cascade`ConjectureGenerator`"]

\(Needs["Theorema`Provers`UserProvers`GroebnerBasesProver`"]; $TmaProofPresentation\  = \ 100;\)

Theorema`Provers`PCS`Solver`Private`$TmaSolveLevel=3

SetOptions[Prove, transformBy -> ProofSimplifier, 
        TransformerOptions -> {branches -> 
              Proved}] ;

    $RecursionLimit = 1024;  Off[General::spell]; 
    Off[General::spell1]; $TmaQRTarget = {"kb", "goal"};

Inductive Definition of Addition

Definition["addition",any[m, n],
	({{m + 0 = m, " +0:"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + .:"}})]

Proof of Left Zero and Left Induction: Some Principles of Theorema Proving Style

Proposition["left zero",any[m, n],
	({{0 + n = n, "0+"}})]

Prove[Proposition["left zero"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved}}];

Prove[Proposition["left zero"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved, 
                    Failed}}];

Proposition["left induction",any[m, n],
	({{\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), ". +"}})]

Prove[Proposition["left induction"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved}}];

Prove[Proposition["left induction"],
	\(using -> ⟨Definition["addition"], 
              Proposition["left zero"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved}}];

Proof of Commutativity and Associativity: The Role of Lemmata and Sequence of Exploration

Proposition["commutativity of addition",any[m, n],
	({{m + n = n + m, " + = "}})]

Prove[Proposition["commutativity of addition"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved, 
                    Failed}}];

Prove[Proposition["commutativity of addition"],
	\(using -> ⟨Definition["addition"], Proposition["left zero"], 
              Proposition["left induction"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved, 
                    Failed}}];

Prove[Proposition["commutativity of addition"],
	\(using -> ⟨Definition["addition"], Proposition["left zero"], 
              Proposition["left induction"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved}}];

Proposition["associativity of addition",any[m, n, p],
	({{m + (n + p) = (m + n) + p, "+"}})]

Prove[Proposition["associativity of addition"],
	\(using -> ⟨Definition["addition"], Proposition["left zero"], 
              Proposition["left induction"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved}}];

Prove[Proposition["associativity of addition"],
	\(using -> ⟨Definition["addition"]⟩\),
	by -> NNEqIndProver,

	ProverOptions -> {TermOrder -> LeftToRight},transformBy -> ProofSimplifier,TransformerOptions -> {branches -> {Proved, 
                    Failed}}];

Multiplication: Subproofs Using Only Knowledge on Addition

Prove[\(Proposition["Associativity of Multiplication"], 
	
        using -> {Propositions["Some Equational Properties of Multiplication"], 
            Propositions["Equational Properties of Addition"]}, \ 
	
        by -> NNEqIndProver\)]// Timing

See notebooks on associativity of *.

Use Propositions Proved for the Next Proofs

Theorema tool "Expand Knowledge Base":

Propositions["equational properties of addition",any[m, n, p],
	({{0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}, {m + n = n + m, " + "}, {(m + n) + p = m + (n + p), "( + ) + "}})]

Prove[\(Propositions["equational properties of addition"], 
	
        using -> Definition["addition"], 
\ \ \ \ \ by -> 
          NNEqIndProver, proof–object -> "SuccessBranch", 
        ExpandKnowledge -> True\)]

Obtain Ideas for Lemmata from Failing Proofs

Theorema tool "Cascade":

\(\(Prove[Proposition["commutativity of addition"], 
	
        using -> Definition["addition"], 
        by -> Cascade[NNEqIndProver, ConjectureGenerator], 
        ProverOptions -> {TermOrder -> LeftToRight}];\)\)

This idea (in a slight modification) is also an essential ingredient for algorithm synthesis in Theorema: see "lazy thinking" method.

Lift Proved Knowledge to the Level of Special Provers

Special Provers S: Correct only in special theories T:

if  S derives goal G from knowledge K,

       then   G must be a logical consequence of T ⋃ K.

Example: associativity of *, this time with special prover (simplifier) for 0, \(TraditionalForm\`\(□\^+\)\), +  terms.

Prove[\(Proposition["Associativity of Multiplication"], 
	
        using -> {Propositions["Some Equational Properties of Multiplication"], 
            Propositions["Equational Properties of Addition"]}, \ 
	
        built–in -> {Property[\(+\(\(->\)\({Associative, 
                    Commutative}\)\)\)]}, 
	by -> NNEqIndProver, 
        proof–object -> "SuccessBranch"\)]// Timing

In Theorema, we implement "many" special provers (e.g. PCS method, Groebner bases, Zeilberger-Paule, Collins).

How do we prove the correctness of these methods? 

   On the object level. 
   How lift the correctness to the metalevel?

Use Accumulated Ideas of Mathematics: "Schemes"

This idea (in a slight modification) is the second essential ingredient for algorithm synthesis in Theorema: see "lazy thinking" method.

A Typical Definition Scheme:

(Underscript[∀ , P, Q])(alternating–quantification[Q, 
              P] ⇔ (Underscript[∀ , f])(Q[
                    f] ⇔ (Underscript[∀ , x])(Underscript[∃ , y])(Underscript[∀ , z]) P[f, x, y, z])).

Two Typical Proposition Scheme:

(Underscript[∀ , f, g, h])(is–commutative[
              f] ⇔ (Underscript[∀ , x, y])(f[x, y] = 
                  f[y, x])).

(Underscript[∀ , f, g, h])(is–homomorphic[f, g, 
              h] ⇔ (Underscript[∀ , x, y])(h[
                    f[x, y]] = g[h[x], h[y]])).

Two Typical Problems Schemes:

(Underscript[∀ , A, P, Q])(explicit–problem[A, P, Q]⇔(Underscript[∀ , x])({{P[A[x]]}, {Q[x, A[x]]}}) ).

(Underscript[∀ , A, P, Q])(canonical–simplifier[A, Q]⇔(Underscript[∀ , x])({{Q[x, A[x]]}, {Q[x, y] \[Implies] (A[x] = A[y])}}) ).

Two Typical Algorithm Schemes:

(Underscript[∀ , F, c, s, g, h1, h2])(divide–and–conquer[F, c, s, g, h1, h2]⇔(Underscript[∀ , x])(F[x]={({{s[x], ⇐, c[x]}, {g[F[h1[x]], F[h2[x]]], ⇐, otherwise}})} ))

(Underscript[∀ , G, lc, df])

    critical–pair–completion[G, lc, df]⇔({{(Underscript[∀ , F])(G[F]  = G[F, pairs[F]])}, {(Underscript[∀ , F])(G[
                      F, ⟨⟩] = F)}, {\(∀ \+\(F, g1, g2, p\&_\)\)(\(G[
                      F, ⟨⟨g1, 
                          g2⟩, p\&_⟩]\)=
where[f = lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],
{({{\(G[
                                  F, ⟨p\&_⟩]\), ⇐, h1 = h2}, {\(G[
                                  F⌢df[h1, 
                                      h2], ⟨p\&_⟩ ≍ ⟨\(⟨F\_k, 
                                        df[h1, 
                                        h2]⟩\)\( \[VerticalSeparator] \+\(k = 
                                        1, …, \[LeftBracketingBar]F\[RightBracketingBar]\)\)⟩]\), ⇐, otherwise}})} ])}})

Example: Set Theory Prover

Definition[\("reflexivity", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–reflexive\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x ∈ A\)x ∼ x\)\)\)]

Definition[\("symmetry", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–symmetric\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x, y ∈ A\)\((x ∼ y \[Implies] y ∼ x)\)\)\)\)]

Definition[\("transitivity", 
      any[\(∼\)\(\(,\)\(A\)\)], 
is–transitive\_A[ ∼ ] : \(\(⇔\)\(∀ \+\(x, y, z ∈ A\)\((x ∼ 
                    y ∧ y ∼ z \[Implies] x ∼ z)\)\)\)\)]

Definition["equivalence",any[∼,A],
is–(Subscript[equivalence, A])[ ∼ ]:⇔∧{({{is–(Subscript[reflexive, A])[ ∼ ]}, {is–(Subscript[symmetric, A])[ ∼ ]}, {is–(Subscript[transitive, A])[ ∼ ]}})} ]

Definition[\("class", 
      any[x, \(\(∼\)\(\(,\)\(A\)\)\)], 
class\_\(A,  ∼ \)[
          x] := {a ∈ A \[VerticalSeparator] 
            a ∼ x ∧ x ∈ A}\)]

Proposition[\("equal classes", 
      any[x ∈ A, y ∈ A, \(\(∼\)\(\(,\)\(A\)\)\)], 
      with[is–equivalence\_A[ ∼ ]], 
x ∼ y \[Implies] \((class\_\(A,  ∼ \)[x] = 
            class\_\(A,  ∼ \)[y])\)\)]

Prove[Proposition["equal classes"],
\(using -> ⟨Definition["equivalence"], 
            Definition["transitivity"], Definition["symmetry"], 
            Definition["class"]⟩\),
by -> SetTheoryPCSProver,
transformBy -> ProofSimplifier,TransformerOptions -> {branches -> Proved, 
              steps -> Useful},ShowOptions -> {},
\(ProverOptions -> {GRWTarget -> {"goal", "kb"}, AllowIntroduceQuantifiers -> True, 
              UseCyclicRules -> True, DisableProver -> {STC, PND}, 
              ApplyBuiltIns -> {}}\),SearchDepth -> 50]

(Proving needs approximately 1 minute.)

Example: The PCS Prover for Analysis

Principle of Lifting Knowledge to Inferencing

In this case, the "green" knowledge which we use for designing a special prover is an algorithm for solving systems of inequalities over the real numbers.

A Rough Sketch of the Method

A heuristic proof method (BB 2000) for predicate logic.

Generates "natural" proofs.

For formulae with alternating quantifiers.

Main idea:  Reduce proof of such formula on (real) functions to
                  to the solution of inequalities on the reals (objects).

Structure:

                   1. Use predicate logic rules (except "simplification" by =, =>, ⇔)
                   2. Simplify (using "semantic unification")
                   3. Solve inequalities.

An Example

Definition[\("limit:", any[f, a], 
	
      limit[f, a]⟺\ \(\(∀ \+ϵ\)\+\(ϵ > 0\)\(∃ \+N\(\(∀ \+n\)\+\(n ≥ N\)\[LeftBracketingBar]f[n] - 
                    a\[RightBracketingBar] < ϵ\)\)\)\)]

Proposition[\("limit of sum", 
      any[f, a, g, 
        b], 
	\((limit[f, a] ∧ 
            limit[g, b])\)\ \ \ \ \  \[Implies] \ \ \ \ \ limit[f + g, 
          a + b]\)]

Definition[\("+:", 
      any[f, g, x], 
	\((f + g)\)[x] = f[x] + g[x]\)]

Lemma[\("|+|", 
      any[x, y, a, 
        b, δ, ϵ], 
	\((\[LeftBracketingBar]\((x + 
                    y)\) - \((a + 
                    b)\)\[RightBracketingBar] < \((δ + ϵ)\))\)\ \ \ \ ⟸\ \ \ \((\[LeftBracketingBar]x - a\[RightBracketingBar] < δ ∧ \[LeftBracketingBar]y - 
                  b\[RightBracketingBar] < ϵ)\)\)]

Lemma[\("max", any[m, M1, M2], 
	
      m ≥ 
          max[M1, M2]\ \ \ \ \  \[Implies] \ \ \ \ \ \((m ≥ 
              M1 ∧ m ≥ M2)\)\)]

Theory["limit",
	({{Definition["limit:"]}, {Definition["+:"]}, {Lemma["|+|"]}, {Lemma["max"]}})]

Prove[Proposition["limit of sum"], 
      using -> Theory["limit"], by -> PCS]

Proof contains interesting algorithmic and didactic information!

Example: The Groebner Bases Prover for Geometrical Theorems

Principle of Lifting Knowledge to Inferencing

In this case, the "green" knowledge which we use for designing a special prover is an algorithm for solving systems of inequalities over the real numbers.

The Method

Each automated proof generated also contains an explanation of the method of reducing the proof problem to the problem of constructing a couple of Groebner bases.

Formula["Test",any[x, y],
	({{\(\((\ \ \((\(x\^2\) y - 3  x\ )\) ≠ 
                    0)\) ∨ \((\((x\ y + x + y)\) ≠ 
                    0)\) ∨ 
		\((\((\((\(x\^2\) y + 3  x = 
                            0)\) ∨ \((\((\(-2\)\ x\^2 + \(-7\)\ x\ y + 
                                x\^2\ y + 
                                x\^3\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2 + 
                                2\ x\^2\ y\^2)\) = 
                            0)\))\)
	 ∧ \((\((x\^2 + \(-x\)\ y + 
                            x\^2\ y + \(-2\)\ y\^2 + \(-2\)\ x\ y\^2)\) = 
                        0)\))\)\),           "B1"}})]

Prove[Formula["Test"], using -> {}, 
      by -> GroebnerBasesProver]

Example Geo Theorema Proving: Pappus Theorem

What does the theorem say geometrically?

Textbook formulation:

Let A, B,  C and A1, B1,  C1 be on two lines and P = A B1 ⋂ A1 B, Q = A C1 ⋂ A1 C, S = B C1 ⋂ B1 C. Then P, Q, and S are collinear.

Input to the system:

Proposition["Pappus",  any[A, B, A1, B1, C, C1, P, Q, S], 
      point[A, B, A1, B1] ∧ pon[C, line[A, B]] ∧ 
          pon[C1, line[A1, B1]] ∧ 
          inter[P, line[A, B1], line[A1, B]] ∧ 
          inter[Q, line[A, C1], line[A1, C]] ∧ 
          inter[S, line[B, C1], line[B1, C]] \[Implies] 
        collinear[P, Q, S]]

Input to the system:

Prove[Proposition["Pappus"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          Refutation -> True}]

Notebook generated automatically by the proving algorithm based on Groebner basis algorithm:

Example Origami Proving: Trisection an Angle (jointly with T. Ida)

We give an example of  trisecting an angle. This example shows a non-trivial use of Axiom (O6). The method of construction is due to H. Abe as described in [Geretschläger 2002, Fushimi 1980].   In the following we will explain the construction of trisecting a given angle using our computational origami system.

NewOrigami[Square[10, 
            MarkPoints -> {"A", "B", "C", "D"}], 
          FigureCaption -> "Step "];

We then introduce an arbitrary point, say E at the coordinate (2, 10), assuming that point A is at (0, 0).

PutPoint[{"E",  Point[2,  10]}];

Our problem is to trisect an angle ∠EAB. The method consists of the following seven steps (steps 3-9) of folds and unfolds.

Step 3: We make a fold to bring point A to D, to obtain the perpendicular bisector of segment AD .  This is the application of (O2). The points F and G, which will be  the terminal points of the crease,  are automatically generated by the system.

OFold[A, D];

Step 4: We unfold the origami and obtain the crease FG .

Unfold[];

Steps 5 and 6: Likewise we obtain the crease HI.

OFold[A, G];

Unfold[];

Step 7: This step is the crucial step of  the construction. We apply (O6).  We try to superpose G  and the line  that is the extension of  the segments AE, and to superpose  A and the line  that is the extension of  the segment HI, simultaneously. There are three possible fold lines to realize this superposition. The system responds with the query of "Specify the line number" together with the lines on the origami image.

OFold[G, AE, A, HI];

Which line(1,2,3)?

Step 8: We reply to the query by the call of OFold[Along->3,Move-> A, ...], which tells the system that we choose the line number 3. This gives the fold line that we are primarily interested in.  However, readers can easily see that the other two fold lines are also solutions (which trisect different angles).

OFold[Along -> 3, Move ->  A, 
        MarkCrease ->  False];

Step 9: We will copy  the points A and I on the other face that is below the face that A and I are on, and unfold the origami. The copied points appear as L and J (the names are automatically generated).

CopyPoint[{A,  I}]; Unfold[];

Step 10: Now we see that the segments AJ and AL trisect the angle  ∠EAB.

ShowOrigamiSegment[{{{A, E}}, {{A, J}}, {{A, L}}}];

Although it is not obvious to see that equational solving is performed, our system solves a set of polynomial equations, up to the third degree, at each step. In the case of steps 7 and 8, the system solves a cubic equation. This explains why we have (at most) 3 possible fold lines at step 7.

Proof of the correctness of the trisection method by Groebner Bases Method:

We now prove the following theorem with our system.

Theorem: The origami construction in section 3 trisects an angle.

∡EAB /3= ∡JAB/2 = ∡LAB.

Example: Proving Combinatorial Identities

Zeilberger, Paule, ... method. Groebner bases for non-commutative polyonomials play a role.

Example: Closed form for the following expression was an open problem for many years! The solution was given in P. Paule,  Computer-Solution of Problem 94-2, SIAM REVIEW Vol.37 (1995), 105-106 using the Paule-Schorn automated conjecture generator / prover.

Formula[\("SIAM series", 
	∑\+\(k = 1, …, n\)\(\(\((\(-1\))\)\^\(k + 1\)\) \((4\ k + 1)\) \(\((2\ k)\)!\)\)\/\(\(2\^k\) \((2\ k - 1)\) \(\((k + 1)\)!\) \(2\^k\) \(k!\)\)\)]

Simplify[Formula["SIAM series"], 
      by -> PauleSchorn–Telescope, 
      built–in -> Built–in["PauleSchorn"]]

Prove[Formula["SIAM series"], 
      by -> PauleSchorn–Telescope, 
      built–in -> Built–in["PauleSchorn"]]

System`FullSimplify[(((((((-1))^(1+k)) (2^(1-2 (1+k))) (2 (1+k))! (2+k))/((1+k)! (2+k)! (-1+2 (1+k))))-(((((-1))^k) (2^(1-2 k)) (2 k)! (1+k))/(k! (1+k)! (-1+2 k))))/((-(((-1))^k) (2^(-2 k)) (2 k)! (1+4 k))/(k! (1+k)! (-1+2 k))))]

Example: Algorithmic Algorithm Synthesis

The Algorithm Invention ("Synthesis") Problem

Given a problem specification P (in predicate logic), find an algorithm A such that

(Underscript[∀ , x]) P[x, A[x]].

Examples of specifications P:

P[x, y]  ⇔  is–greater[x, y]
P[x, y]  ⇔  
      is–sorted–version[x, y]
P[x, y]  ⇔  
      has–derivative[x, y]
P[x, y]  ⇔  
      are–factors–of[x, y]
P[x, y]  ⇔  
      is–Gröbner–basis[x, 
        y]
....

A general algorithm S for "all" P cannot exist (cf. B. Caviness 1970, ...)   but ...

There is a rich literature on algorithm synthesis methods.

The "Lazy Thinking" Method for Algorithm Synthesis [BB 2003]

Given a problem specification P

consider various "algorithm schemes" for A

and try to prove (automatically) (Underscript[∀ , x]) P[x, A[x]].

This proof will normally fail because nothing is known on the unspecified sub-algorithms in the algorithm scheme.

From the temporary assumptions and goals in the failing proof situation (automatically) generate such specifications for the unspecified sub-algorithms that would make the proof possible.

Now, apply the method recursively to the auxiliary functions.

This is "lazy"

we use the condensed algorithmic experience of others (in the schemes)

we start (routine) proving before we have an algorithm

we just wait until we fail in order to get an idea from the failure.

An Algorithm for Generating Sub-problems from Failing Correctness Proofs

A simple (but amazingly powerful) rule:

Collect temporary assumptions  T[ x0, ... A [  ],  ...  ]
and temporary goals G[ x0, ...m  [  A [  ]  ]  ]

and produces specification

(Underscript[∀ , X,   ... ,  Y,   ... ])  (T[X,...Y,...]    ⟹   G[Y,...m  [Y] ] ).

Details: see papers [BB 2003] and example.

Research topic: other rules.

How far can we go with this method?

By this method, we have synthesized, e.g., various sorting algorithms.

Can we automatically synthesize algorithms for non-trivial problems?  What is "non-trivial"?

Example of a non-trivial problem: construction of Gröbner bases.

Main algorithmic idea of Gröbner bases theory:  The "S-polynomials"  ("critical pairs") together with the S-polynomial theorem.

Hence, question: Can Lazy Thinking automatically invent the notion of S-polynomial and automatically deliver the S-polynomial theorem.

The Problem of Constructing Gröbner Bases

Find algorithm Gb such that

(Underscript[∀ , F])    (({{is–finite[ Gb[F] ]}, {is–Gröbner–basis[ Gb[F]]}, {ideal[F]=ideal[ Gb[F]].}}))

Definitions [BB 1965, 1970]:

is–Gröbner–basis[G]⇔is–confluent[ (Subscript[-> , G])].

Confluence of Division  (Subscript[-> , G])

(h1 (Subscript[-> , G])h2)⇔ (Underscript[∃ , g ∈ G])({({{lp[g] | lp[h1]}, {h2 = h1 - (lm[h1]/lm[g]) g}})} ),

is–confluent[->] :\(\(⇔\)\(∀ \+\(f1, f2\)\((f1\( ↔ \^*\)f2 \[Implies] 
              f1\(↓\^*\)f2)\)\)\)

Knowledge on the Concepts Involved

h1 (Subscript[-> , G])h2   \[Implies]  
          p  .  h1 (Subscript[-> , G])p  .  h2

etc.

Algorithm Scheme "Critical Pair / Completion"

({{A[F] =A[F, pairs[F]]}, {A[F, ⟨⟩]=F
}, {A[\(F, ⟨⟨g1, 
                  g2⟩, p\&_⟩\)]=
where[f=lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],
{({{A[\(F, ⟨p\&_⟩\)], ⇐, h1 = h2}, {A[F⌢df[h1, 
                                h2],\(⟨p\&_⟩\)≍⟨⟨(Subscript[F, k]),df[h1, h2]⟩ (Underscript[\[VerticalSeparator] , k = 
                                        1, …, \[LeftBracketingBar]F\[RightBracketingBar]])⟩], ⇐, otherwise}})} ]}})

This scheme can be tried in any domain, in which we have a reduction operation rd that depends on sets F of objects and a Noetherian relation ≻ which interacts with rd in the following natural way:

(Underscript[∀ , f, g])(f ⪰ 
            rd[f, g]).

The Essential Problem

The problem of synthesizing a Gröbner bases algorithm can now be also stated by asking whether starting with the proof of

(Underscript[∀ , F])    (({{is–finite[ A[F] ]}, {is–Gröbner–basis[ A[F]]}, {ideal[F]=ideal[ A[F]].}}))

we can automatically produce the idea that

lc[g1, g2]=lcm[lp[g1], lp[g2]]

and

df[h1, h2]=h1-h2

and prove that the idea is correct.

Now Start the (Automated) Correctness Proof

With current theorem proving technology, in the Theorema system, the proof attempt could be done automatically. (Not yet fully implemented.)

Details

Upon Termination

It should be clear that, upon termination, the final result is a finite set (of polynomials) G that has the property

(Underscript[∀ , g1, g2 ∈ G])(where[f = lc[g1, g2],h1 = trd[rd[f, g1], F],h2 = trd[rd[f, g2], F],∨{({{h1 = h2}, {df[h1, h2] ∈ G}})} ]).

(Termination proof has do be done extra!)

We Have to Prove

We now try to prove that, if G has this property, then

is–finite[G], 
ideal[F] = 
      ideal[G], 
is–Gröbner–basis[
      G],  
      i . e .  
      is–Church–Rosser[ (Subscript[-> , G])] .

Here, we only deal with the third, most important, property.

Using Available Knowledge

Using Newman's lemma and some elementary properties it can be shown that it is sufficient to prove

is–Church–Rosser[ (Subscript[-> , G])]⇔ (Underscript[∀ , p])(Underscript[∀ , f1, f2])(({({{p -> f1}, {p -> f2}})} )\[Implies]\(f1\(↓\^*\)f2\)).

Assumption

Let now the power product p and the polynomials f1, f2 be arbitary but fixed and assume

{({{p (Subscript[-> , G])f1}, {p (Subscript[-> , G])f2.}})}

We have to find a polyonomial g such that

({{\(\(f1\(\( -> \_G\)\^*\)g\)\(,\)\)}, {\(f2\(\( -> \_G\)\^*\)\(\(g\)\(.\)\)\)}})

From the Assumption

From the assumption we know that there exist polynomials g1 and g2 in G such that

({{lp[g1] | p,}, {f1 = rd[p, g1],}})
({{lp[g2] | p,}, {f2 = rd[p, g2].}})

From the final situation in the algorithm scheme we know that for these g1 and g2

∨{({{h1 = h2}, {df[h1, h2] ∈ G,}})}

where

({{h1 := trd[f1', G], f1' := rd[lc[g1, g2], g1], }, {h2 := trd[f2', G], f2' := rd[lc[g1, g2], g2].}})

Case h1=h2: In this case

\(lc[g1, 
          g2]\( -> \_g1\)\(rd[lc[g1, g2], g1]\(\( -> \_G\)\^*\)trd[
            rd[lc[g1, g2], g1], G]\) = 
trd[
          rd[lc[g1, g2], g2], G]\(\( ← \_G\)\^*\)rd[lc[g1, g2], 
          g2]\( ← \_g2\)\(\(lc[g1, g2]\)\(.\)\)\)

(Note that here we used the requirements rd[lc[g1,g2],g1]≺lc[g1,g2] and rd[lc[g1,g2],g2]≺lc[g1,g2].)

Hence, by elementary properties of polynomial reduction,

\(∀ \+\(a, q\)\(\((\ 
          a\ q\ lc[g1, 
                  g2]\( -> \_g1\)\(a\ q\ rd[lc[g1, g2], 
                    g1]\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
                    G]\) = 
a\ q\ trd[rd[lc[g1, g2], g2], 
                  G]\(\( ← \_G\)\^*\)a\ q\ rd[lc[g1, g2], 
                  g2]\( ← \_g2\)\ 
              a\ q\ lc[g1, g2]\ )\)\(.\)\)\)

Now we are stuck in the proof.

Use Specification Generation Algorithm

However, using the above specification generation rule, we see that we could proceed successfully with the proof if lc[g1,g2] satisfied the following requirement

({{(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies]((Underscript[∃ , a, q])(p = a q lc[g1, g2] ))), , (lc requirement)}})

With such an lc, we then would have

\(p\( -> \_g1\)rd[p, 
            g1] = \(a\ q\ rd[lc[g1, g2], g1]\(\( -> \_G\)\^*\)a\ q\ trd[
                rd[lc[g1, g2], g1], 
                G] = \(a\ q\ trd[rd[lc[g1, g2], g2], 
                  G]\(\( ← \_G\)\^*\)a\ q\ rd[lc[g1, g2], g2] = 
            rd[p, g2]\( ← \_g2\)p\)\)\)}

and, hence,

\(\(\(f1\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
          G]\)\(,\)\)\)

\(\(\(f2\(\( -> \_G\)\^*\)a\ q\ trd[rd[lc[g1, g2], g1], 
          G]\)\(,\)\)\)

i.e. we would have found a suitable g.

Summarizing the Specifications of the Unknown Subalgorithm lc

(lc requirement), which also could be written in the form:

(Underscript[∀ , p, g1, g2])(({({{lp[g1] | p}, {lp[g2] | p}})} )\[Implies](lc[g1, g2] | p)) ,

and the requirements:

rd[lc[g1, g2], g1] ≺ 
      lc[g1, g2], 
rd[lc[g1, g2], g2] ≺ 
      lc[g1, g2],

which, in the case of the domain of polynomials, are equivalent to

({{lp[g1] | lc[g1, g2],}, {lp[g2] | lc[g1, g2].}})

A Suitable lc

lcp[g1, g2] = lcm[lp[g1], lp[g2]]

is a suitable function that satisfies the above requirements.

Heureka! The crucial function lc (the "critical pair" function) in the critical pair / completion algorithm scheme has been "automatically" synthesized!

Case h1≠h2 and, hence, df[h1,h2]∈G:

In this part of the proof we are basically stuck right at the beginning.

We can try to reduce this case to the first case, which would generate the following requirement

({{\(∀ \+\(h1, h2\)\((h1\ \(\(↓\_{df[h1, 
                            h2]}\)\^*\)h2)\)\), (df requirement).  }})

(Looking to the knowledge base of elementary properties of polynomial reduction, it is now easy to find a function df  that satifies (df requirement), namely

df[h1, h2] = h1 - h2,

because, in fact,

\(∀ \+\(f, g\)\(\((f\ \(\(↓\_{f - 
                        g}\)\^*\)g)\)\(.\)\)\)

Heureka! The function df (the "completion" function) in the critical pair / completion algorithm scheme has been "automatically" synthesized!)

Namely,

Conclusion

I believe that, going into the direction of systems like Theorema, the following is / will soon be possible:

Computer-support, for the "working mathematician", of all aspects of doing mathematics will reach higher and higher levels including inventing, exploring, proving.

In particular, nonalgorithmic and algorithmic mathematics will be supportable in one common logical and software-technological frame (in other words, mathematics, and computer science will reconcile).

Mathematical software systems, in addition to providing algorithm libraries, will  have to provide huge mathematical knowledge libraries. Building up and using such libraries, essentially, is a task of formal logic. (Compare International MKM Network.)

The education of mathematicians will have to shift towards including in-depth training on the formal / logical aspects of mathematics.