Guide to the Prove-It library of proofs

Theory Web Pages

Our proofs are organized into hierarchy of theories. A theory is a kind of domain of knowledge and these may be interdependent. Each theory contains zero or more common expressions, axioms, and theorems. The theory 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 theory-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 theory). Axioms are named judgments that require no proof. These effectively define theory-related operations and mathematical concepts. Theorems are named judgments 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.

Expressions

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 judgments 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 Literals. Furthermore, a problem-story Variable in a particular theory, 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 Variables 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 Variables 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)$.
• ExprTuple: A list of Expressions that is used, for example, when there are multiple operators or operands of an Operation or multiple parameters of a Lambda.
• ExprArray: A multi-dimensional (e.g., two-dimensional) array of Expressions. 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 ExprArray class.
• NamedExprs: A mapping from keyword strings to Expressions. 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 ExprTuple or ExprArray. 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 theory, 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 expr_info() 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.

Known Truths

A proven statement in Prove-It is called a judgment. 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 judgment is simply displayed as
$\vdash$ truth expression The turnstile symbol, $\vdash$ will hyperlink to the proof of the judgment.

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 judgment. 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 judgments may derive from existing judgments via derivation rules. These rules include generalization and instantiation which can actualize a change of an unbound variable to any other expression. Taking the previous example, generalizing this judgment will derive
$\vdash \forall_{A~|~\lnot A} A = \bot$.
This may then be instantiated to produce any specific instance of $A$ for which $\lnot A$ is proven or assumed.

Proof Web Pages

Clicking on the turnstile symbol, $\vdash$, of a judgment will take you to its proof page. This displays all of the derivation steps starting from the proven judgment (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).

Common Expression Web Pages

Each theory 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 theory. Clicking on any of these expressions will take you to the expression information page.

Axiom Web Pages

Axioms are judgments that are accepted without proof. They provide the definitions for the various mathematical objects and operations. They can be theory-specific; for example, a theory 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.

Theorem Web Pages

Theorems are judgments that require a proof. These must be derived from axioms or other theorems using derivation rules used to obtain new judgments for previous judgments. 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.

Theorem Proof Web Pages

Clicking on the name of a theorem on the theorems web page of a theory 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 theorem 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 theorem proof as well as any dependent theorems that have not yet been proven.

Derivation Rules

New judgments 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 judgment 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 judgment 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 judgment simply become the union of the assumptions of the prerequisite judgments. Furthermore, either or both of the prerequisite judgments 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 judgment 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 judgment 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 judgment. As an example, suppose we have a judgment 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 judgment with explicit universal quantification into a judgment 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 judgments. For example,
  $\{ \forall_{x~|~Q(x)} P(x), Q(x)\} \vdash P(x)$
  may be derived without any prerequisites. Of course, in the instantiation 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 judgment. 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 instantiated simultaneously and some variables may be relabeled instead. The difference between instantiating 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 instantiating and then generalization but can also be done in one step via relabeling.
  
  Finally, there are special instantiation rules involving iterations and indexed expression. Specifically, when the variable of an indexed expression is replaced, via instantiation, 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 instantiating
  $\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 judgments as prerequisites. In this example,
  $\vdash 1+1=2$ and $\vdash 2+1=3$
  are prerequisites.

Dependencies Web Pages

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.

Demonstrations Web Pages

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