 Demonstrations for context proveit.logic.equality¶

In :
import proveit
%begin demonstrations

Substitution¶

Equality is a fundamental concept of logic. When two mathematical operations are equal, then one may be substituted for the other. This is rule is defined by the substitution axiom:

In :
from proveit.logic.equality._axioms_ import substitution
from proveit._common_ import a, b, c, d, x, y, z, fx # we'll use these later
substitution

The English translation of this axiom is: for any function $f$ and any $x, y$ such that $x=y$, $f(x) = f(y)$. In other words, we may substitute $y$ for $x$ in any function whenever $x=y$. The equality of $x$ and $y$ transfers to an equality between $f(x)$ and $f(y)$. This is fundamental to the meaning of equality regardless of what $f$ does (as long as it can act on a single argument). We may specialize this axiom using any operation for $f$. For example,

In :
from proveit.logic import Not, Equals
substitution.specialize({fx:Not(x), x:a, y:b}, assumptions=[Equals(a, b)])

There are more convenient ways to apply this substitution rule than manual specialization that was demonstrated in the previous input. The Equals class has the substitution, subLeftSideInto and subRightSideInto methods for conveniently applying substitution and its variants, as we will demonstrate below. Each of these methods takes a lambdaMap argument to provide a context for the substitution -- what is being substituted and where. A lambdaMap can be an actual Lambda expression, an InnerExpr object, or if it is neither of these, it can be any other Expression for which the default will be to performa a global replacement.

In :
from proveit import Lambda
from proveit.number import Add, frac, Exp
expr = Equals(a, Add(b, frac(c, d), Exp(c, d)))

The globalRepl static method of Lambda is useful for creating a global replacement lambda map. Below, we create a map for replacing every occurence of $d$ in expr with anything else:

In :
gRepl = Lambda.globalRepl(expr, d)

We now use this lambda map to replace occurences of $d$ in expr with $y$:

In :
d_eq_y = Equals(d, y)
In :
d_eq_y.substitution(gRepl, assumptions=[d_eq_y])

Or we can take advantage of that a global replacement is performed by default when a non-Lambda expression is provided as the "lambdaMap".

In :
d_eq_y.substitution(expr, assumptions=[d_eq_y])

Either way, the generated proof is the same:

If we want to perform substitution for a specific inner expression, and not necessarily a global replacement, the proveit._core_.expression.InnerExpr class (aliased as proveit.InnerExpr) is extremely convenient. It uses some Python tricks via implementing the __getitem__ and __getattr__ methods. First, you create the InnerExpr object by calling the innerExpr() method on the top-level expression:

In :
innerExpr = expr.innerExpr()

The InnerExpr object displays itself with two important pieces of information: the lambda map that it represents and the inner expression of the top-level expression that would be replaced by this lambda map. The point is that we will be able to "dig" in to inner expressions of the top-level expression via accessing sub-expression attributes. For example, we next will "dig" into the "right hand side" (rhs) of the master expression:

In :
innerExpr = innerExpr.rhs

By accessing the rhs attribute, we created a new InnerExpr object that has the same top-level expression as the original but has a new current inner expression. Note that the InnerExpr class does not know anything about the rhs attribute itself; it is relying on the fact that the previous sub-expression has this attribute. The InnerExpr class also has tricks for getting an sub-expression with an index (or key):

In :
innerExpr = innerExpr.operands

Now will "dig" down to the denominator of $\frac{c}{d}$ and show how we use the InnerExpr class to replace a particular occurence of $d$ rather than a global replacement:

In :
innerExpr = innerExpr.denominator
In :
d_eq_y.substitution(innerExpr, assumptions=[d_eq_y])

Let us demonstrate this technique again, replacing the other occurrence of $d$. This time we do this more succinctly, without the extra pedogogial steps:

In :
d_eq_y.substitution(expr.innerExpr().rhs.operands.exponent, assumptions=[d_eq_y])

The substition method, that we demonstrated above, is a direct application of the substitution axiom. It proves the equality between some $f(x)$ and some $f(y)$. We often will want to take a shortcut to perform a statement substitution in which we prove some $P(y)$ is true assuming that $P(x)$ is true and $P(x) = P(y)$. For this, we have the subRightSideInto and subLeftSideInto methods.

If the expression that we want to substitute in is on the right hand side of the Equals object playing the role of $x=y$, then we use subRightSideInto:

In :
d_eq_y.subRightSideInto(gRepl, assumptions=[d_eq_y,expr])

We can also take advantage of the global replacement default and provide a non-Lambda Expression.

In :
d_eq_y.subRightSideInto(expr, assumptions=[d_eq_y,expr])

If the expression that we want to substitute in is on the left hand side of the Equals object playing the role of $x=y$, then we use subLeftSideInto:

In :
y_eq_d = Equals(y, d)
In :
y_eq_d.subLeftSideInto(gRepl, assumptions=[y_eq_d,expr])

Again, we can provide a non-Lambda Expression to do a simple global replacement.

In :
y_eq_d.subLeftSideInto(expr, assumptions=[y_eq_d,expr])

The proof uses a theorem the relies upon the substitution axiom, rather than using the substition axiom directly:

Reflexivity, symmetry, and transitivity¶

Reflexivity, symmetry, and transitivity are also fundamental properties of equality, in addition to the ability to perform substitution. Reflexivity is the fact that any mathematical object is equal to itself. Symmetry is the fact that $x = y$ and $y = x$ are equivalent (either both of these are true or both of these false). Transitivity is the ability to derive $x=z$ from $x=y$ and $y=z$. These are all axioms.

In :
from proveit.logic.equality._axioms_ import equalsReflexivity, equalsSymmetry, equalsTransitivity
In :
equalsReflexivity
In :
equalsSymmetry
In :
equalsTransitivity

equalsReversal is a useful theorem for applying the symmetry property of equality:

In :
from proveit.logic.equality._theorems_ import equalsReversal
equalsReversal # y=x derives from x=y

These three properties are applied automatically for Equals objects

Reflexivity is concluded automatically:

In :
Equals(a, a).prove()
In :
Equals(a, a).prove().proof()

Symmetric statements are derived as side-effects. Note that the KnownTruth.deriveSideEffects method employs a mechanism to prevent infinite recursion or this would not be possible (it would continually go back and forth, proving $y=x$ from $x=y$ then $x=y$ from $y=x$, ad infinitum)

In :
a_eq_b = Equals(a, b)
In :
Equals(b, a).prove([a_eq_b])

The reversed form may also be derived explicitly via deriveReversed. The proof is the same.

Transitivity derivations are attempted with automation via the conclude method using the trensitivitySearch function in proveit.logic.equality.transitivity_search. This performs a breadth-first, bidirectional search (meeting in the middle from both ends) over the space of KnownTruth objects representing equality and using appropriate assumptions. This is therefore reasonably efficient. Efficiency should not really be an issue, anyways, as long as proofs for each theorem are relatively small. A long proof should be broken up into several smaller proofs for lemma-like theorems. In that case (in the setting of small proofs), the space of KnownTruths will be small and this search algorithm will have ample efficiency.

In :
# We'll make this interesting by reversing some of the equations in the chain.
c_eq_b = Equals(c, b)
In :
d_eq_c = Equals(d, c)
In :
d_eq_z = Equals(d, z)
In :
a_eq_z = Equals(a, z).prove(assumptions=[a_eq_b, c_eq_b, d_eq_c, d_eq_z])

The applyTransivity method applies the transitivity relation explicity.

In :
a_eq_b.prove([a_eq_b]).applyTransitivity(c_eq_b, assumptions=[c_eq_b])

Evaluation¶

An evaluation is an equality in which the right hand side is an irreducible value (specifically, an instance of proveit.logic.irreducible_value.IrreducibleValue, aliased as proveit.logic.IrreducibleValue). An irreducible value represents a mathematical object in its simplest form. It cannot be reduced. The evaluation of an IrreducibleValue is itself. When an evaluation is proven, the associated KnownTruth is stored for future reference in Equals.evaluations for making other evaluations.

TRUE ($\top$) and FALSE ($\bot$) are both IrreducibleValues:

In :
from proveit.logic import TRUE, FALSE, IrreducibleValue
In :
isinstance(TRUE, IrreducibleValue)
Out:
True
In :
isinstance(FALSE, IrreducibleValue)
Out:
True
In :
TRUE.evaluation()

An IrreducibleValue should implement the evalEquality and notEqual methods to prove equality relations with other IrreducibleValues as appropriate.

In :
Equals(Equals(FALSE, TRUE), FALSE).deriveContradiction([Equals(FALSE, TRUE)])
In :
TRUE.evalEquality(TRUE)
In :
TRUE.evalEquality(FALSE)
In :
TRUE.notEqual(FALSE)

A proven expression will evaluate to TRUE.

In :
a_eq_T = a.evaluation([a])

A disproven expression will evaluate to FALSE.

In :
a_eq_F = a.evaluation([Not(a)])

If the expression to be evaluated is known to be equal to an expression that has already been evaluated, transitivity will automatically be applied.

In :
b_eq_F = b.evaluation([Equals(b, a), Not(a)])

When evaluating an expression, an evaluation of the operands will be attempted. The operation class is responsible for overridding the evaluate method in order to properly treat the operation applied to irreducible values or generate a more efficient proof as appropriate.

In :
from proveit.logic import Or, Not, inBool
In :
nested_eval = Or(a, Not(a)).evaluation([a])

Boolean equality¶

Equality with TRUE ($\top$) or FALSE ($\bot$) has special logical consequences. The Equals object has automation capabilities to treat these special kinds of equations.

In :
TRUE
In :
FALSE

Proofs via boolean equality are automatic via Equals.deduceSideEffects:

In :
a.prove([Equals(a, TRUE)])
In :
Not(b).prove([Equals(b, FALSE)])

Going the other direction, boolean equalities are proven automatically via Equals.conclude:

In :
Equals(x, TRUE).prove([x])
In :
Equals(TRUE, y).prove([y])
In :
Equals(c, FALSE).prove([Not(c)])
In :
Equals(FALSE, c).prove([Not(c)])

When something is equal to FALSE and known to be true, there is a contradiction. That is, FALSE is a consequence. The deriveContradiction method of Equals can be used to prove such a contradiction:

In :

Contradictions are useful in making contradiction proofs (reductio ad absurdum). The affirmViaContradiction and denyViaContradiction methods are useful in making such a proof. They both use deriveContradiction. For example:

In :
from proveit.logic import Implies, inBool
not_a__truth = Equals(a, FALSE).affirmViaContradiction(Not(a), [Implies(a, Equals(a, FALSE)), inBool(a)])
In :
not_a__truth.proof().numSteps()
Out:
13

It is more efficient to use denyViaContradiction when proving the negation of something. Here we prove the same as above but in fewer steps.

In :
not_b__truth = Equals(b, FALSE).denyViaContradiction(b, [Implies(b, Equals(b, FALSE)), inBool(b)])
In :
not_b__truth.proof().numSteps()
Out:
9

Equality and sets¶

All equality expressions are in the boolean set by the equalityInBool axiom. That is, given any two mathematical objects, they are either equal or not (even nonsense is either the same nonsense or different nonsense).

In :
eq_in_bool = Equals(a, b).deduceInBool()
Out:

A singleton is a set with one element. If $x=c$, then $x$ is in the singleton set of $\{c\}$:

In :
in_singleton_truth = Equals(x, c).deriveIsInSingleton([Equals(x, c)])

Not equals¶

The NotEquals operation is a more way of expressing that two mathematical objects are not equal to each other.

In :
from proveit.logic import NotEquals
In :
a_neq_b = NotEquals(a, b)
In :
a_neq_b.definition()

From $\lnot (a = b)$ one can derive $a \neq b$ and vice-versa, folding and unfolding the NotEquals.

In :
a_neq_b.prove([Not(a_eq_b)])
In :
Not(a_eq_b).prove([a_neq_b])

NotEquals also has a symmetry property which can be applied directly. It can be proven through automation.

In :
NotEquals(b, a).prove([a_neq_b])

Or explicitly via deriveReversed

If two objects are both equal and not equal, there is a contradiction.

In :