logo

Axioms for the theory of proveit.logic.booleans.conjunction

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.logic import Equals, And, TRUE, FALSE, Forall, in_bool
from proveit import A, B, m, n
from proveit.core_expr_types import A_1_to_m
from proveit.numbers import Natural
In [2]:
%begin axioms
Defining axioms for theory 'proveit.logic.booleans.conjunction'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Truth table definitions:

In [3]:
and_t_t = Equals(And(TRUE, TRUE), TRUE)
Out[3]:
and_t_t:
In [4]:
and_t_f = Equals(And(TRUE, FALSE), FALSE)
Out[4]:
and_t_f:
In [5]:
and_f_t = Equals(And(FALSE, TRUE), FALSE)
Out[5]:
and_f_t:
In [6]:
and_f_f = Equals(And(FALSE, FALSE), FALSE)
Out[6]:
and_f_f:

Conjunction is only well-defined when each input is a Boolean:

In [7]:
left_in_bool = Forall((A, B), in_bool(A), conditions=[in_bool(And(A, B))]) 
Out[7]:
left_in_bool:
In [8]:
right_in_bool = Forall((A, B), in_bool(B), conditions=[in_bool(And(A, B))]) 
Out[8]:
right_in_bool:

Definition of multi-operand conjunction:

In [9]:
empty_conjunction = And() # base case
Out[9]:
empty_conjunction:
In [10]:
multi_conjunction_def = \
    Forall(m, Forall((A_1_to_m, B), 
                     Equals(And(A_1_to_m, B), And(And(A_1_to_m), B)).with_wrap_after_operator()),
           domain=Natural)
Out[10]:
multi_conjunction_def:
In [11]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.booleans.conjunction