Our proofs are organized into hierarchy of contexts. A **context** is a kind of domain of knowledge and these may be interdependent. Each **context** contains zero or more **common expressions**, **axioms**, and **theorems**. The **context** web-page has links to one web-page each for the common expressions,
axioms, and theorems, as well as a demonstrations
web page containing relevant context-specific examples. **Common expressions** are named expressions that may be used when defining **axioms** and **theorems** as well as for convenience in the construction of **theorem** **proofs**, **demonstrations**, and may also be used externally (outside of the **context**). **Axioms** are named known truths that require no proof. These effectively define context-related operations and mathematical concepts. **Theorems** are named known truths that require a proof. Each theorem name, on the **theorems** web page, links to its proof page. **Proofs** may be constructed in any order and have not all been constructed yet. A **theorem** without a complete **proof** is regarded as *unproven*. Each **proof** page links to a dependencies page which lists all of the **axioms** used directly or indirectly in the proof, as well as any required *unproven* **theorems**. It also displays the **theorems** that depend directly upon that one. The final type of web page that is generated in this library is a web page of expression information that shows the full tree-like structure of each **expression**. The **expression information** pages of **axioms** and **theorems** also link to **dependencies** web pages.

Mathematical **expressions** are the basic building block of **Prove-It** proofs. These are represented with rendered LaTeX. As much as possible, this representation should reflect the internal contents of the **expression** object. However, to fully understand what is actually being represented by an **expression**, click on the rendered LaTeX to view its expression information web page.

**Expressions** form known truths that are used in the derivation steps of a **proof**. An **expression** has no intrinsic value type, unlike in conventional theorem-proving approaches. It does have a *type* that refers to the kind of operation or mathematical object. There are 9 *core types* recognized for having specific rules in proof derivations.

`Variable`

: A label that is interchangeable (as long as it is kept distinct from other labels) with no intrinsic meaning. It is usually represented by a single letter but can have any representation.`Literal`

: A label that is not interchangeable and has an intrinsic meaning. Specific operators ($\lnot, \land, +, \times$, etc.) and specific irreducibe values ($\top, \bot, 0, 5$, etc.) are all`Literal`

s. Furthermore, a problem-story`Variable`

in a particular**context**, representing some unknown but particular value, should also be a`Literal`

(e.g., "Ann has $a$ apples...").`Operation`

: The application of*operator(s)*on*operand(s)*. For example, $0 + 5 + 8$ and $1 < a \leq b < 3$ are examples of*operation*expressions. The**Prove-It**library defines many*types*derived from the*operation*type (e.g., for each specific operation), but the derivation rules only need to know that these are*operations*.`Lambda`

: A mapping defined by*parameter*`Variable`

s transforming to some*body*`Expression`

but only when the*parameter(s)*meet certain*condition(s)*. For example, $(x, y, z) \mapsto x+y/z~|~x \in \mathbb{R}, y \in \mathbb{R}, z \in \mathbb{R}, z \neq 0$ is a conditional**lambda**that converts three real numbers $x, y, z$ to $x + y/z$ as long as $z$ is not zero. Note that a`Lambda`

introduces`Variables`

into a new scope via the*parameters*. These*parameter*`Variable`

s are said to be*bound*in this new scope; occurrences outside this scope are not deemed to be the same thing. There is a special category of`Operation`

types called`OperationOverInstances`

that are essentially functionals acting on a`Lambda`

operand. $\forall$, $\exists$, $\sum$, and $\prod$ are examples of`OperationOverInstances`

. For example, $\forall_{x~|~Q(x)} P(x)$ is an expression that translates to "$P(x)$ is true for all values of $x$ for which $Q(x)$ is also true". Internally, this is represented as an $\forall$ operator acting on the conditional`Lambda`

map $x \mapsto P(x)~|~Q(x)$.`ExprList`

: A list of`Expression`

s that is used, for example, when there are multiple*operators*or*operands*of an`Operation`

or multiple*parameters*of a`Lambda`

.`ExprTensor`

: A multi-dimensional (e.g., two-dimensional) array of`Expression`

s. This can be used, for example, to represent a quantum circuit which is a two-dimensional graphical representation of a sequence of quantum operations. A 2-D representation of a matrix is a more basic example. More work is required to properly implement and test the*ExprTensor*class.*NamedExprs*: A mapping from keyword strings to`Expression`

s. This can be used to prevent ambiguity of an expression's internal representation.`Indexed`

: A particular indexed element of a`Variable`

where the`Variable`

is intended to serve as a placeholder for an`ExprList`

or`ExprTensor`

. It has a*base*which determines the indexing offset, typically $0$ or $1$. For example, $x_5$ represents the fifth or sixth element of $x$ in*base*$1$ or $0$ respectively. The*base*is typically not displayed and must be inferred by the context, though it is explicitly revealed in the expression information page. An`Indexed`

expression is typically contained within an`Iter`

(described next).`Iter`

: Represents an iteration of a*parameter*going from a*start*to an*end*in successive unit increments ($+1$). For example, $x_1 +~\ldots~+ x_n$ contains an`Iter`

of`Indexed`

`Variable`

. If we take $n$ to be $3$, this would expand to $x_1 + x_2 + x_3$. An`Iter`

has a*lambda map*,*start index(indices)*, and*end index(indices)*. In our example, the`Iter`

$x_1,~\ldots,x_n$, is the*operand*of an`proveit.number.addition.Add`

`Operation`

. The*lambda map*,*start index*and*end index*of the*iteration*are $i \mapsto x_i$, $1$, and $n$, respectively.

**Prove-It** has an `Expression`

class. The 9 *core types* are classes derived from the `Expression`

class. Each `Expression`

object has a class that is one of these 9 *core types* or a class derived from one of these. This object-oriented approach is convenient for accessing appropriately-named sub-expressions, calling convenient methods to apply **axioms** or **theorems** pertaining to the class, and implementing class-specific automation of obvious derivation steps.

**Expression Information Web Pages**

Clicking on generated mathematical expression in this library will take you to a
web page that shows the explicit breakdown of the **expression** into
a tree-like structure. The top of the page indicates the *type* (class)
of expression (again, not to be consued with a type-theory notion of its
value type) with a link to its documentation page. Clicking on the *type* at the top of this web page will, when this feature is implemented, take you to the code documentation for the **expression's** class. Currently these are dead links.

The first two notebook inputs of this page show Python code for generating and "checking" the **expression**. The first input shows the necessary `import`

commands. The second input builds the **expression** and checks, via `%check_expr`

, that this built expression is consistent with what is stored in a kind of database that **Prove-It** maintains. The third and final notebook input shows the command to display the *expression information* of the **expression** object via the `exprInfo()`

method. Its output is a table with the tree-like structure of the **expression** with all of its *sub-expressions*. The first entry, with index "0", is the full **expression**. Each entry lists the numbers of direct *sub-expressions* that are always later entries in the table.

A proven statement in **Prove-It** is called a **known truth**. These are represented in the form:

{*assumption expressions*} $\vdash$ *truth expression*

where the *assumption expressions* is a comma-delimited list of expressions and the *truth expression* is a single expression. When there are no assumptions, the **known truth** is simply displayed as

$\vdash$ *truth expression*

Any *unbound* variable in the *assumption expressions* and/or *truth expression* (not *bound* within the scope of any lambda expression) are deemed to be *arbitrary variables*. They can represent anything without altering its status as a **known truth**. This is not the case for literals which may only take on a single value (which may or may not be known).

As an example, $\{\lnot A\} \vdash A = \bot$, taking $A$ to be a *variable*, translates to "any $A$ equals false ($\bot$) assuming the logical negation of $A$ is a true fact". A main part of **Prove-It's** unique approach is that there is no intrinsic typing system to ensure that $A$ has a *Boolean* type (true ($\top$) or false ($\bot$) represented as the set $\mathbb{B} = \{\top, \bot\}$). Rather, it is inferred, in this case for example, from the *assumption* that the logical negation of $A$ is true. The logical negation of a value is only defined when that value is a *Boolean*. Otherwise it simply cannot be evaluated.

New **known truths** may derive from existing **known truths** via derivation rules. These rules include generalization and specialization which can actualize a change of an *unbound* *variable* to any other **expression**. Taking the previous example, *generalizing* this **known truth** will derive

$\vdash \forall_{A~|~\lnot A} A = \bot$.

This may then be *specialized* to produce any specific instance of $A$ for which $\lnot A$ is proven or assumed.

Each context contains a **common expressions** page that defines zero or more named expressions that can be used for convenience to build axioms and theorems as well as a general aid in proof construction. It may also be used in demonstrations and external to the **context**. Clicking on any of these **expressions** will take you to the expression information page.

**Axioms** are known truths that are accepted without **proof**. They provide the definitions for the various mathematical objects and operations. They can be **context**-specific; for example, a **context** may define specific literal quantities for a specific story problem or scope. They can also be used externally as desired. The expression information web page of an **axiom** has a link to a dependencies web page that shows all of the **theorems** whose **proof** depends directly upon this **axiom**. There are also dependencies web pages for each **proof** showing what **axioms** are used directly or indirectly in the **proof**. In this way, **axiom** usage is tracked for every **proof** so users can ensure that only appropriate **axioms** are used for any particulary **proof** of interest.

**Theorems** are known truths that require a proof. These must be derived from axioms or other **theorems** using derivation rules used to obtain new **known truths** for previous **known truths**. These **theorems** may be proven in any order and some of the **theorems** in this library have not yet been proven. By explicitly indicating what other **theorems** may be *presumed* in a given **proof**, we avoid circular logic. When a **theorem** does have a **proof**, it will have a dependencies web page, accessed via a link titled `dependencies`

on the **proof** page, that reveals all **axioms** used directly or indirectly in the **proof** as well as any dependent **theorems** that have not yet been proven.

Clicking on the name of a **theorem** on the theorems web page of a **context** will take you to its **proof** page. If the **proof** has been supplied, this will show the Python code used to generate its derivation, culminating in the `%qed`

command which displays all of the derivation steps starting from the proven **theorem** (step `0`

) and working its way backwards through the derivation, each step dependent upon *requirements* that are realized at later steps (a convenient check against circular logic within a **theorem** **proof**). The **proof** web page will link to a dependencies web page, via a link titled `dependencies`

that reveals all axioms used directly or indirectly in the **proof** as well as any dependent **theorems** that have not yet been proven.

New known truths may be derived from existing ones, in order to generate a proof of a thereom by using a small number of derivation rules that are available. These are as follows:

*Assumption*:

For any expression $A$, $A$ is known to be true if $A$ is assumed to be true. Thus,

$\{A\} \vdash A$

Note that the**Prove-It**system is indifferent to whether or not the assumed**expression**is a proper Boolean-type expression. While it is assumed, it does have a Boolean value (`TRUE`

to be specific), but that does not imply that it has a Boolean type more generally, when it is not assumed.*Axiom/theorem invocation*:

Introduces a known truth from an axiom or theorem and tracks its use in the tracked dependencies.*Axiom/theorem elimination*:

Converts**axioms**or**theorems**into assumptions and removes them from the tracked**dependencies**. Literals may be simultaneously converted to variables in this process. This must be done in a fully consistent manner (converting all**axioms**/**theorems**that involve the*literal*simultanously, and converting all of the*literals*that the**axioms**/**theorems**involve). (This has not yet been implemented in the**Prove-It**code.)*Hypothetical reasoning*:

Given a**known truth**with*assumptions*, converts any one of the assumptions into an antecedent in an explicit implication. For example, from

$\{A, B, C, \ldots\} \vdash Z$

derive

$\{A, C, \ldots\} \vdash B \Rightarrow Z$

Both forms have their use. Implications are important because they can be nested ("$\vdash$" cannot be nested). As with*assumptions*,**Prove-It**is indifferent about whether or not the*antecedent*and*consequent*of the*implication*are Boolean-type expression. For an*implication*to be true it only matters that the*consequent*is true if/when the*antecedent*is true; if the*antecedent*has no defined value or is non-Boolean, the*implication*is vacuously true regardless of whether or not the*consequent*can be evaluated.*Modus ponens*:

From an implication, derive its consequent given that the antecedent is known or assumed to be true. For example, from

$\{A, B, C\} \vdash Y \Rightarrow Z$

and

$\{B, C, D\} \vdash Y$

derive

$\{A, B, C, D\} \vdash Z$

The*assumptions*of the resulting**known truth**simply become the union of the*assumptions*of the prerequisite**known truths**. Furthermore, either or both of the prerequisite**known truths**may be incorporated in the*assumptions*list instead of having independent derivations. For example, the following may be introduced without any prerequisites:

$\{A, A \Rightarrow B\} \vdash B$*Generalization*

As mentioned above, any*unbound*variable in a**known truth**is deemed to be*arbitrary*. To transform such a fact into an explicit form,*generalization*may be used to introduce a universal quantification ($\forall$) over*arbitrary**variables*. Any of the*assumptions*of the original**known truth**may be listed as*conditions*of the universal quantification and removed from the*assumptions*list. Any*assumptions*containing the*unbound**variable(s)*must be converted to*conditions*in this manner because they must be included in the new*binding*of the*variable(s)*. Additional*conditions*may be added as desired because this can only weaken the**known truth**. As an example, suppose we have a**known truth**of the form

$\{x \in S, Q(x)\} \vdash P(x)$,

where $Q(x)$ and $P(x)$ take the place of**expressions**involving $x$ as an*unbound**variable*and $S$ may be any**expression**but should be a properly defined set in order for $x \in S$ to evaluate to true for any $x$. We can then derive, via*generalization*,

$\vdash \forall_{x \in S~|~Q(x)} P(x)$.

Note that the $x \in S$ notation of this universal quantification is a shorthand LaTeX representation in place of $\forall_{x~|~x \in S, Q(x)}$ but internally $x \in S$ is treated as a*condition*in the same manner as $Q(x)$. This is a simple, single-*variable*example, but multiple*variables*, in fact, may be*generalized*simultaneously. Also, multiple nested $\forall$ operations may be introduced simultaneously.*Specialization*and*relabeling*

*Specialization*is the reverse of*generalization*. It can transform a**known truth**with explicit universal quantification into a**known truth**with fewer $\forall$ operations. For example, given

$\{A, B\} \vdash \forall_{x~|~Q(x)} P(x),$

and

$\{B, C\} \vdash Q(x)$

we can derive

$\{A, B, C\} \vdash P(x)$,

As with*modus ponens*, the new*assumptions*are the union of the prerequisite*assumption*and there is flexibility in what is included in the*assumptions list*versus other**known truths**. For example,

$\{ \forall_{x~|~Q(x)} P(x), Q(x)\} \vdash P(x)$

may be derived without any prerequisites. Of course, in the*specialization*process, $x$ may be replaced with any expression, as long as it does not violate scoping restrictions of lambda**expression**. That is, the*unbound**variables*in the replacement of $x$ cannot be the same as any*parameter*of a*lambda*that contains an instance of*x*in the original**known truth**. For example, from

$\vdash \forall_{x} \exists_{y}~y=x,$

we**can**derive

$\vdash \exists_{y}~y=5$,

but we**cannot**derive

$\vdash \exists_{y}~y=y+5$.

Multiple*variables*and even multiple nested $\forall$ operations may be*specialized*simultaneously and some*variables*may be*relabeled*instead. The difference between*specializing*and*relabeling*is that the corresponding $\forall$ is not eliminated in the case of*relabeling*but the*variable*may only be replaced with another*variable*. This could be accomplished via*specializing*and then*generalization*but can also be done in one step via*relabeling*.

Finally, there are special*specialization*rules involving iterations and indexed**expression**. Specifically, when the*variable*of an*indexed***expression**is replaced, via specialization, with an expression list or expression tensor, the indexing must be performed, replacing the*indexed*expression with the particular*indexed*value (or an exception raised if it cannot be performed); and when the*indexed***expression**is contained within an*iteration*, the*iteration*must be expanded to reveal each particular*indexed*value. For example, when*specializing*

$\vdash \forall_{n \in \mathbb{N}} \forall_{x, y_1, \ldots, y_n \in \mathbb{C}}~x \cdot (y_1 + \ldots + y_n) = x \cdot y_1 + \ldots x \cdot + y_n$

(the distribution law) with $n \mapsto 3$, $x \mapsto x$, and $y \mapsto [a, b, c]$, we can derive

$\{x \in \mathbb{C}, a \in \mathbb{C}, b \in \mathbb{C}, c \in \mathbb{C} \} \vdash x \cdot (a + b + c) = x \cdot a + x \cdot b + x \cdot c$.

In this example, the*indexed***expressions**use*base*one, implicit in the LaTeX representation but explicit in the internal representation. To expand the*iteration*,**Prove-It**applies $+1$ to the*start index*successively until reaching the*end index*, performing evaluations along the way. The derivation step requires these evaluation**known truths**as prerequisites. In this example,

$\vdash 1+1=2$ and $\vdash 2+1=3$

are prerequisites.

The `dependencies`

link on a proof web page or on the expression information web page of an axiom or theorem will take you a web page that shows **dependencies** for the corresponding **axiom** or **theorem**. For **theorem** **dependencies**, this page lists all the **axioms** used directly or indirectly in the **proof** as well as any dependent **theorems** that have not yet been proven. Additionally, for both **axiom** and **theorem** **dependency** pages, it lists all of the **theorems** that directly depend on that **axiom**/**theoreom**.

The **demonstrations** web page of a **context** shows examples of how to use the operations and concepts defined in the **context** and should test automation capabilities. It is a useful regression testing tool as well as a tutorial for using what is defined in the **context**. Many of these have not been generated yet or are incomplete at this time.