TH∃OREM∀

Bruno Buchberger

RISC and RICAM
Linz, Austria
Bruno.Buchberger@RISC.Uni-Linz.ac.at

Copyright Bruno Buchberger 2004.

Copyright Note: This file can be copied and stored under the following conditions:

- the file must be kept unchanged including the copyright note
- an note must be sent to buchberger@risc.uni-linz.ac.at
- the talk should be cited appropriately if material from this talk is used.

Acknowledgement to Theorema Group: 

T. Jebelean, T. Kutsia, (K. Nakagawa), M. Rosenkranz, W. Windsteiger.

A. Craciun, F. Piroi.

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

Integration in Theorema

Integration in one logic: a version of predicate logic.

Integration in one software system: implementation language ("meta language") is Mathematica:

A. Mathematica as a programming language (Theorema reasoners are programmed in Mathematica)

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

(In the future, we may use Theorema for A.)

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!

limit[f, 
        a]⟺ (Underscript[((Underscript[∀ , ϵ])), ϵ > 0])(Underscript[∃ , N])(Underscript[((Underscript[∀ , n])), (Underscript[((Underscript[∀ , ϵ])), ϵ > 0])(Underscript[∃ , N])(Underscript[((Underscript[∀ , n])), n ≥ N])\[LeftBracketingBar]f[n] - a\[RightBracketingBar] < ϵ])\[LeftBracketingBar]f[n] - 
                  a\[RightBracketingBar] < ϵ

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:

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"]⟩]\)

Tracing Computations

See proving.

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⟩⟩⟩]]

Induction Proofs

Initialize Theorema Provers

Needs["Theorema`"];

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

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

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;\)

Needs["Theorema`Provers`PauleSchorn`Simplifier`"]

Built–in["PauleSchorn",
	({{Built–in["Quantifiers"]}, {Built–in["Operators"]}, {Built–in["Numbers"]}, {Built–in["Number Domains"]}, {Built–in["Forward Difference"]}})]

Use[Built–in["PauleSchorn"]];
\(\(FormatVariables[
	FontWeight -> "Plain"\ , 
	
        FontSlant -> "Italic"
];\)\)
\(FormatArbitraryButFixedConstants[
	
      FontWeight -> "Plain"\ , 
	
      FontSlant -> "Plain"
]\)

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, 
                    Failed}}];

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

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

By this call, the following proof is generated automatically (including the English explanatory text):

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}}];

The proof generated automatically:

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

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

The proof generated automatically: more knowledge leads to shorter proofs!

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

Commutativity

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}}];

Proof fails: too little knowledge

Prover call with more knowledge

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

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

Proof succeeds: we use lemmata already proved earlier

Associativity

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}}];

Short proof using earlier lemmata

Prover call without lemmata

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

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

Long proof using only definition

Multiplication: Subproofs Using Only Knowledge on Addition

The prover call

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

The proof generated automatically

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of (( * ) * )fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: proved

We prove (( * ) * ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (( * ) * .IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IB.F) works.

Simplification of the lhs term:

(0*(Subscript[n, 1]))*(Subscript[p, 1]) =by (0*)

0*(Subscript[p, 1]) =by (0*)

0⌋

Simplification of the rhs term:

0*((Subscript[n, 1])*(Subscript[p, 1])) =by (0*)

0⌋

Alternative proof 2: pending

Pending proof of (( * ) * .IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (( * ) * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2]))*(Subscript[p, 2]) =by ( ^+*)

((Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]))*(Subscript[p, 2]) =by ( + )

((Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])*((Subscript[n, 2])*(Subscript[p, 2])) =by ( ^+*)

(Subscript[m, 1])*((Subscript[n, 2])*(Subscript[p, 2]))+(Subscript[n, 2])*(Subscript[p, 2]) =by (( * ) * .IH)

((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])+(Subscript[n, 2])*(Subscript[p, 2]) =by ( + )

(Subscript[n, 2])*(Subscript[p, 2])+((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Hence, it is sufficient to prove:

We prove (( * ) * .IS.S) by  induction on n.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (( * ) * .IS.S.IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IS.S.IB.F) works.

Simplification of the lhs term:

(0+(Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

(0 + 0)*(Subscript[p, 3]) =by ( +0)

0*(Subscript[p, 3]) =by (0*)

0⌋

Simplification of the rhs term:

0*(Subscript[p, 3])+((Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

0*(Subscript[p, 3])+0*(Subscript[p, 3]) =by (0*)

0+0*(Subscript[p, 3]) =by (0*)

0 + 0 =by ( +0)

0⌋

Alternative proof 2: pending

Pending proof of (( * ) * .IS.S.IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in (( * ) * .IS.S.IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))*(Subscript[p, 4]) =by (^++ )

(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))])*(Subscript[p, 4]) =by ( ^+*)

((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))*(Subscript[p, 4])+(Subscript[p, 4]) =by ( + )

(Subscript[p, 4])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))*(Subscript[p, 4]) =by ( + )

(Subscript[p, 4])+((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4]) =by (( + ) + )

(Subscript[p, 4])+(((Subscript[n, 3])+(Subscript[m, 1]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =by ( + )

(Subscript[p, 4])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by ( *  ^+)

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4]) =by ( ^+*)

((Subscript[n, 3])*(Subscript[p, 4])+(Subscript[p, 4]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4]) =by ( + )

((Subscript[p, 4])+(Subscript[n, 3])*(Subscript[p, 4]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4]) =by ( + )

((Subscript[p, 4])+(Subscript[n, 3])*(Subscript[p, 4]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4])⌋

Hence, it is sufficient to prove:

We try to prove (( * ) * .IS.S.IS.S) by  induction on p.

Induction Base:

A proof by simplification of (( * ) * .IS.S.IS.S.IB) works.

Simplification of the lhs term:

0+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*0 =by ( *0)

0 + 0⌋

Simplification of the rhs term:

(0+(Subscript[n, 3])*0)+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0 =by ( *0)

(0 + 0)+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0 =by ( *0)

(0 + 0) + 0 =by ( +0)

0 + 0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We simplify (( * ) * .IS.S.IS.S.IS).

Simplification of the lhs term:

(SuperPlus[(Subscript[p, 5])])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])]) =by ( *  ^+)

(SuperPlus[(Subscript[p, 5])])+((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))) =by (^++ )

(SuperPlus[((Subscript[p, 5])+((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =by ( + )

(SuperPlus[((Subscript[p, 5])+((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))]) =by (( + ) + )

(SuperPlus[(((Subscript[p, 5])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by (( + ) + )

(SuperPlus[((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[n, 3])))+(Subscript[m, 1])*(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))])⌋

Simplification of the rhs term:

((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])]) =by ( *  ^+)

((SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])]) =by ( *  ^+)

((SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))) =by (^++ )

(SuperPlus[((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))) =by (^++ )

(SuperPlus[(((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))))]) =by ( + )

(SuperPlus[(((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))))]) =by ( + )

(SuperPlus[(((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))]) =by (( + ) + )

(SuperPlus[((((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by ( + )

(SuperPlus[((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5]))))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by (( + ) + )

(SuperPlus[(((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[p, 5]))+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by ( + )

(SuperPlus[((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by (( + ) + )

(SuperPlus[(((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by ( + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by (( + ) + )

(SuperPlus[(((((Subscript[n, 3])+(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by (( + ) + )

(SuperPlus[((((((Subscript[n, 3])+(Subscript[p, 5]))+(Subscript[m, 1]))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by ( + )

(SuperPlus[(((((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[p, 5])))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by (( + ) + )

(SuperPlus[((((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[p, 5]))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =by ( + )

(SuperPlus[(((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[n, 3])))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))])⌋

Hence, it is sufficient to prove:

The proof of (( * ) * .IS.S.IS.S.IS.S)fails.(No applicable inference rule was found.)

Alternative proof 2: proved

We prove (( * ) * .IS.S.IS) by  induction on p.

Induction Base:

A proof by simplification of (( * ) * .IS.S.IS.IB) works.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*0 =by ( *0)

0⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*0+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*0 =by (( * ) * .IH)

(SuperPlus[(Subscript[n, 3])])*0+(Subscript[m, 1])*((SuperPlus[(Subscript[n, 3])])*0) =by ( *0)

0+(Subscript[m, 1])*((SuperPlus[(Subscript[n, 3])])*0) =by ( *0)

0+(Subscript[m, 1])*0 =by ( *0)

0 + 0 =by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (( * ) * .IS.S.IS.IS) works.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by (( * ) * .IS.S.IS.IH)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by (^++ )

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))]) =by ( + ^+)

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(SuperPlus[(Subscript[p, 6])])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by ( + ^+)

(SuperPlus[(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))])+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =by (^++ )

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =by ( + )

(SuperPlus[((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =by (( + ) + )

(SuperPlus[(((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =by ( + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Alternative proof 2: pending

Pending proof of (( * ) * .IS).

In a Nutshell: Ideas for (Automated) Exploration

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\)]

One proposition in the list after the other is proved and, when proved, add to the knowledge base, before the proof of the next proposition in the list is carried out. We do not show all the automatically generated proof notebooks here.

Obtain Ideas for Lemmata from Failing Proofs

Call of the "Cascade": Proof attempts plus automated generation of conjectures for lemmata from failing proof attempts

Theorem tool "Cascade":

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

Resulting sequence of proof notebooks

This call results in the automated generation of the following sequence of proof attempts and, finally, a successful proof of commutativity. Note that, in the course of producing these proof attempts and the final proof, the initial knowledge base is automatically enlarged by lemmata, and in fact quite natural and interesting lemmata, which are invented automatically in the course of analyzing the failing proof attempts:

Prove:

under the assumptions:

.... Proof fails and leads to the automated invention of the following lemma:

(Underscript[∀, m ])(0+m=m).

whose proof is now attempted next.

Prove:

under the assumptions:

.... This proof succeeds and, hence, the lemma can be added to the knowledge base and the proof of commutativity is attempted again.

Prove:

under the assumptions:

.... Proof fails and leads to the automated invention of the following lemma:

(Underscript[∀, n,m])((SuperPlus[n])+m=(SuperPlus[(n+m)])).

whose proof is now attempted next.

Prove:

under the assumptions:

.... This proof succeeds and, hence, the lemma can be added to the knowledge base and the proof of commutativity is attempted again.

whose proof is now attempted next.

Prove:

under the assumptions:

.... This proof succeeds and, hence, commutativity is proved.

The cascade can also be viewed as a kind of general completion procedure that goes far beyond the Knuth-Bendix completion procedure for equational theorem proving.

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

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

Resulting proof (compare it with the proof of associativity of * above): in particular, those lines in which (special simplifier) is called

Prove:

under the assumptions:

We prove (( * ) * ) by  induction on m.

Induction Base:

We take in (( * ) * .IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IB.F) works.

Simplification of the lhs term:

(0*(Subscript[n, 1]))*(Subscript[p, 1]) =by (0*)

0*(Subscript[p, 1]) =by (0*)

0⌋

Simplification of the rhs term:

0*((Subscript[n, 1])*(Subscript[p, 1])) =by (0*)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (( * ) * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2]))*(Subscript[p, 2]) =by ( ^+*)

((Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]))*(Subscript[p, 2]) =by (Special Simpl )

((Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])*((Subscript[n, 2])*(Subscript[p, 2])) =by ( ^+*)

(Subscript[m, 1])*((Subscript[n, 2])*(Subscript[p, 2]))+(Subscript[n, 2])*(Subscript[p, 2]) =by (( * ) * .IH)

((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])+(Subscript[n, 2])*(Subscript[p, 2]) =by (Special Simpl )

(Subscript[n, 2])*(Subscript[p, 2])+((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Hence, it is sufficient to prove:

We prove (( * ) * .IS.S) by  induction on n.

Induction Base:

We take in (( * ) * .IS.S.IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IS.S.IB.F) works.

Simplification of the lhs term:

(0+(Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

(0 + 0)*(Subscript[p, 3]) =by ( +0)

0*(Subscript[p, 3]) =by (0*)

0⌋

Simplification of the rhs term:

0*(Subscript[p, 3])+((Subscript[m, 1])*0)*(Subscript[p, 3]) =by ( *0)

0*(Subscript[p, 3])+0*(Subscript[p, 3]) =by (0*)

0+0*(Subscript[p, 3]) =by (0*)

0 + 0 =by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (( * ) * .IS.S.IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by (Special Simpl)

((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by ( *  ^+)

(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by (Special Simpl)

(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))])*(Subscript[p, 4]) =by (Special Simpl)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))])*(Subscript[p, 4]) =by ( ^+*)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4])+(Subscript[p, 4]) =by (Special Simpl )

(Subscript[p, 4])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =by (Special Simpl)

((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4])+(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4]) =by ( *  ^+)

((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4])+(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4]) =by (Special Simpl)

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =by ( ^+*)

((Subscript[n, 3])*(Subscript[p, 4])+(Subscript[p, 4]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =by (Special Simpl )

(Subscript[p, 4])+((Subscript[n, 3])*(Subscript[p, 4])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]))⌋

Hence, it is sufficient to prove:

We prove (( * ) * .IS.S.IS.S) by  induction on p.

Induction Base:

A proof by simplification of (( * ) * .IS.S.IS.S.IB) works.

Simplification of the lhs term:

0+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*0 =by ( *0)

0 + 0⌋

Simplification of the rhs term:

0+((Subscript[n, 3])*0+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0) =by ( *0)

0+(0+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0) =by ( *0)

0 + (0 + 0) =by (Special Simpl)

(0 + 0) + 0 =by ( +0)

0 + 0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (( * ) * .IS.S.IS.S.IS) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])]) =by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])]) =by ( *  ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3]))))+(SuperPlus[(Subscript[p, 5])]) =by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(SuperPlus[(Subscript[p, 5])]) =by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(Subscript[p, 5]))]) =by (Special Simpl)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =by (( * ) * .IS.S.IS.S.IH)

((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))+(Subscript[m, 1])*(Subscript[n, 3]))))^+ =by (Special Simpl )

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))^+⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])) =by (Special Simpl)

(Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =by ( *  ^+)

((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =by (Special Simpl)

(Subscript[n, 3])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =by ( *  ^+)

(Subscript[n, 3])+((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(SuperPlus[(Subscript[p, 5])]) =by ( + ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(Subscript[p, 5]))^+ =by (Special Simpl )

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))^+⌋

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}})} ])}})

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 2 minutes !!)

Proof generated automatically

Using (Proved) Knowledge for Better Provers: 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!

The proof generated automatically

Using (Proved) Knowledge for Better Provers: The Groebner Bases Prover for Geometrical Theorems

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]

The proof generated automatically

Using (Proved) Knowledge for Better Provers: 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))))]

Calling External Provers (e.g. Resolution)

Links from Theorema to various existing theorem provers, for example to the Otter prover:

<< "C:\PROGRAM FILES\ATP \
SYSTEMS\TMA2EXTERNAL\THEOREMA2EXTERNAL.M"

Definition["Inclusion",
		({{(Underscript[∀ , A, B])((A ⊆ 
                          B)⟺(Underscript[∀ , x])((x ∈ A)⟹(x ∈ 
                                B))), "⊆:"}})]
	Definition["Union",
		({{(Underscript[∀ , A, x])((x ∈ ⋃A)⟺(Underscript[∃ , Y])((x ∈ 
                                Y) ∧ (Y ∈ A))), "⋃:"}})]
	Definition["Powerset",
		({{(Underscript[∀ , A, x])((x ∈ 𝒫[
                            A])⟺(x ⊆ A)), "P:"}})]

Proposition["Union of powerset includes...",
		({{(Underscript[∀ , A])(A ⊆ ⋃𝒫[
                          A]), "⊆P⋃"}})]

ProveExternal[Proposition["Union of powerset includes..."],using->{Definition["Inclusion"],Definition["Union"],Definition["Powerset"]},by -> Otter]

Algorithm Synthesis

Rough Sketch

Want to prove:

(Underscript[∀, is–tuple[X]])is–sorted–version[X,sorted[X]]

Throw in an "idea":

(Underscript[∀, is–tuple[X]])(sorted[X]=\[LeftDoubleBracketingBar]special[X]⇐is–trivial–tuple[X],merged[sorted[left–split[X]],sorted[right–split[X]]]⇐otherwise\[RightDoubleBracketingBar])

All the auxiliary operations like "merged" etc. are unknown!

Try to prove the correctness theorem:

From the failing (!) proof generate necessary specification for the auxiliaries.

Now appy procedure recursively !

Example

First proof attempt generated with generation of subspecification

Pending proof of (13.4).

Pending proof of (8).

Second proof attempt generated with generation of subspecification

Pending proof of (41.4).

Third proof attempt generated with generation of subspecification

Final proof  generated

A Recent Achievement: Automated Synthesis of Groebner Bases Algorithm

Proving Provers Correct

We need some "quotation" mechanism!  M. Sato's system ?

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. Hence, computer-supported derivation of theorems from knowledge bases will be a future key tool. (See MKM 2001 at RISC, MKM 2003 at U Bologna, MKM 2004 at U Byalostok).

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