logo

Axioms for the theory of proveit.core_expr_types.conditionals

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import Conditional, ConditionalSet, ExprRange, IndexedVar
from proveit import a, b, c, i, m, n, Q
from proveit.logic import Implies, Forall, Equals, TRUE, FALSE, Or
from proveit.numbers import one, Natural
In [2]:
%begin axioms
Defining axioms for theory 'proveit.core_expr_types.conditionals'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

A Conditional is defined to evaluate to its value when the condition is TRUE:

In [3]:
true_condition_reduction = Forall(a, Equals(Conditional(a, TRUE), a))
Out[3]:
true_condition_reduction:

The condition is either true or not true but otherwise it doesn't matter if it is a Boolean. Therefore, a condition of $Q$ is the same as a condition of $Q=\top$

In [4]:
condition__as__condition_eq_true = \
    Forall((a, Q), Equals(Conditional(a, Q), 
                          Conditional(a, Equals(Q, TRUE))).with_wrap_before_operator())
Out[4]:
condition__as__condition_eq_true:

If two values are equal when the condition is satisfied, one may replace the other within the Conditional.

In [5]:
conditional_substitution = \
    Forall((a, b, Q), Equals(Conditional(a, Q),
                             Conditional(b, Q)).with_wrap_before_operator(),
          conditions=[Implies(Q, Equals(a, b))])
Out[5]:
conditional_substitution:

If one and only one Conditional in a ConditionalSet is True, equate the ConditionalSet to the Conditional.

In [6]:
# singular_truth_reduction = \
#     Forall((m, n), 
#            Forall((a, b, c), 
#                   Equals(ConditionalSet(var_range(a, one, m), b, var_range(c, one, n)), b), 
#                   conditions=[Equals(Or(var_range(a, one, m)), FALSE), Equals(Or(var_range(c, one, n)), FALSE)]), 
# domain=Natural)
In [7]:
singular_truth_reduction = \
    Forall((m, n), 
           Forall((a, b, c), 
                  Equals(ConditionalSet(ExprRange(i, Conditional(IndexedVar(a, i), FALSE), one, m), b, 
                                        ExprRange(i, Conditional(IndexedVar(c, i), FALSE), one, m)), b)), 
                  domain=Natural)
Out[7]:
singular_truth_reduction:
In [8]:
%end axioms
These axioms may now be imported from the theory package: proveit.core_expr_types.conditionals