# Axioms for context proveit.logic.boolean.disjunction¶

In [1]:
from proveit.logic import Equals, Or, TRUE, FALSE, Forall, inBool
from proveit._common_ import A, B, BB, n
from proveit.logic._common_ import iterB1n
from proveit.number import Naturals

In [2]:
%begin axioms

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


### Truth table definitions:¶

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

Out[3]:
orTT:
In [4]:
orTF = Equals(Or(TRUE, FALSE), TRUE)

Out[4]:
orTF:
In [5]:
orFT = Equals(Or(FALSE, TRUE), TRUE)

Out[5]:
orFT:
In [6]:
orFF = Equals(Or(FALSE, FALSE), FALSE)

Out[6]:
orFF:

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

In [7]:
leftInBool = Forall((A, B), inBool(A), conditions=[inBool(Or(A, B))])

Out[7]:
leftInBool:
In [8]:
rightInBool = Forall((A, B), inBool(B), conditions=[inBool(Or(A, B))])

Out[8]:
rightInBool:

### Definition of multi-operand disjunction¶

In [9]:
emptyDisjunction = Equals(Or(), FALSE) # base case

Out[9]:
emptyDisjunction:
In [10]:
multiDisjunctionDef = Forall(n, Forall((A, BB), Equals(Or(iterB1n, A), Or(Or(iterB1n), A))),
domain=Naturals)

Out[10]:
multiDisjunctionDef:
In [11]:
%end axioms

Axioms may be imported from autogenerated _axioms_.py