logo
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 NaturalsPos
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(A, iterB1n), Or(A, Or(iterB1n)))),
                             domain=NaturalsPos)
Out[10]:
multiDisjunctionDef:
In [11]:
%end axioms
Axioms may be imported from autogenerated _axioms_.py