# Axioms for the theory of proveit.logic.booleans.disjunction¶

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 TRUE, FALSE, Not, Or, Equals, Forall, in_bool
from proveit import A, B, n, m
from proveit.core_expr_types import B_1_to_n, A_1_to_m
from proveit.numbers import Natural

In [2]:
%begin axioms

Defining axioms for theory 'proveit.logic.booleans.disjunction'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


### Truth table definitions:¶

In [3]:
or_t_t = Equals(Or(TRUE, TRUE), TRUE)

or_t_t:
In [4]:
or_t_f = Equals(Or(TRUE, FALSE), TRUE)

or_t_f:
In [5]:
or_f_t = Equals(Or(FALSE, TRUE), TRUE)

or_f_t:
In [6]:
or_f_f = Equals(Or(FALSE, FALSE), FALSE)

or_f_f:

### Disjunction only well-defined when each input is a Boolean:¶

In [7]:
left_in_bool = Forall((A, B), in_bool(A), conditions=[in_bool(Or(A, B))])

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

right_in_bool:

### Definition of multi-operand disjunction¶

In [9]:
empty_disjunction = Not(Or()) # base case

empty_disjunction:
In [10]:
multi_disjunction_def = \
Forall(m, Forall((A_1_to_m, B),
Equals(Or(A_1_to_m, B), Or(Or(A_1_to_m), B)).with_wrapping_at(2)),
domain=Natural)

multi_disjunction_def:
In [11]:
%end axioms

These axioms may now be imported from the theory package: proveit.logic.booleans.disjunction