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

In [1]:
from proveit import varIter
from proveit import Lambda, Iter, Indexed
from proveit._common_ import A, B, C, D, E, AA, BB, CC, DD, EE, i, j, k, l, m, n
from proveit.logic import Or, TRUE, FALSE, Forall, Implies, Not, inBool, And, Booleans, Equals, Set
from proveit.logic._common_ import iterA1l, iterA1m, iterB1m, iterC1m, iterC1n, iterD1n
from proveit.number import Naturals, NaturalsPos, Add, Exp, one, LessEq, LesserSequence
%begin theorems

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

In [2]:
trueOrTrue = Or(TRUE, TRUE)

Out[2]:
In [3]:
trueOrFalse = Or(TRUE, FALSE)

Out[3]:
In [4]:
falseOrTrue = Or(FALSE, TRUE)

Out[4]:
In [5]:
falseOrFalseNegated = Not(Or(FALSE, FALSE))

Out[5]:
In [6]:
orIfBoth = Forall((A, B), Or(A, B), conditions=[A, B])

Out[6]:
In [7]:
orIfOnlyLeft = Forall((A, B), Or(A, B), conditions=[A, Not(B)])

Out[7]:
In [8]:
orIfOnlyRight = Forall((A, B), Or(A, B), conditions=[Not(A), B])

Out[8]:
In [9]:
neitherIntro = Forall((A, B), Not(Or(A, B)), conditions=[Not(A), Not(B)])

Out[9]:
In [10]:
binaryOrContradiction = Forall((A, B), FALSE, conditions=(Or(A, B), Not(A), Not(B)))

Out[10]:
In [11]:
leftIfNotRight = Forall((A, B), A, domain=Booleans, conditions=(Or(A, B), Not(B)))

Out[11]:
In [12]:
rightIfNotLeft = Forall((A, B), B, domain=Booleans, conditions=(Or(A, B), Not(A)))

Out[12]:

This constrained singular constructive dilemma will require a single provable $C$ be designated as a Boolean. The "unconstrained" version will drop this constraint, using the constrained version as a convenient Lemma. This will all culminate to the constructive dilemma, below, that can prove some $C \lor D$ given $A \lor B$, $A \Rightarrow C$ and $B \Rightarrow D$.

In [13]:
constrainedSingularConstructiveDilemma = Forall((A, B, C), C, conditions=[Or(A, B), Implies(A, C), Implies(B, C)],
domain=Booleans)

In [14]:
singularConstructiveDilemma = Forall((A, B), Forall(C, C, conditions=[Implies(A, C), Implies(B, C)]),
domain=Booleans, conditions=[Or(A, B)])

Out[14]:
In [15]:
singularConstructiveMultiDilemma = Forall((m),Forall((AA), Forall(C, C, conditions=[Iter(i,Implies(Indexed(AA,i), C), one, m)]), domain=Exp(Booleans,m),conditions=[Or(varIter(AA, one, m))]),domain = Naturals)

Out[15]:
In [ ]:


In [16]:
orIfLeft = Forall((A, B), Or(A, B), domain=Booleans, conditions=[A])

Out[16]:
In [17]:
orIfRight = Forall((A, B), Or(A, B), domain=Booleans, conditions=[B])

Out[17]:
In [18]:
constructiveDilemma = Forall((A, B, C, D), Or(C, D), domain=Booleans,
conditions=[Or(A, B), Implies(A, C), Implies(B, D)])

Out[18]:
In [19]:
constructiveMultiDilemma = Forall((m),Forall((AA, BB), Or(varIter(BB, one, m)), domain=Exp(Booleans,m),
conditions=[Or(iterA1m), Iter(i,Implies(Indexed(AA,i), Indexed(BB,i)), one, m)]), domain = Naturals)

Out[19]:
In [20]:
destructiveDilemma = Forall((A, B, C, D), Or(Not(A), Not(B)), domain=Booleans,
conditions=[Or(Not(C), Not(D)), Implies(A, C), Implies(B, D)])

Out[20]:
In [21]:
destructiveMultiDilemma = Forall((m),Forall((AA, BB), Or(Iter(i, Not(Indexed(BB,i)), one, m)), domain=Exp(Booleans,m), conditions=[Or(Iter(i, Not(Indexed(AA,i)), one, m)), Iter(i,Implies(Indexed(AA, i), Indexed(BB, i)),one,m)]), domain = Naturals)

Out[21]:
In [22]:
notLeftIfNeither = Forall((A, B), Not(A), conditions=(Not(Or(A, B))))

Out[22]:
In [23]:
notRightIfNeither = Forall((A, B), Not(B), conditions=(Not(Or(A, B))))

Out[23]:
In [ ]:


In [24]:
unaryDisjunctionLemma = Forall(A, (Equals(Or(A), Or(FALSE, A))), domain = Booleans)

Out[24]:
In [25]:
unaryDisjunctionDef = Forall(A, Equals(Or(A), A), domain = Booleans)

Out[25]:
In [26]:
eachInBool = Forall((m, n), Forall((AA, B, CC), inBool(B), conditions=inBool(Or(iterA1m, B, iterC1n))),
domain=Naturals)

Out[26]:
In [27]:
orIfAny = Forall((m, n), Forall((AA, B, CC), Or(iterA1m, B, iterC1n),
domains=[Exp(Booleans, m), Booleans, Exp(Booleans, n)], conditions=[B]),
domain=Naturals)

Out[27]:
In [28]:
notOrIfNotAny = Forall(m, Forall(AA, Not(Or(iterA1m)),
conditions=[Iter(i, Not(Indexed(AA, i)), one, m)]),
domain=Naturals)

Out[28]:
In [29]:
orContradiction = Forall(m, Forall(AA, FALSE, conditions=(Or(iterA1m), Iter(i, Not(Indexed(AA, i)), one, m))),
domain=Naturals)

Out[29]:
In [ ]:


In [30]:
trueEval = Forall((m, n), Forall((AA, CC), Equals(Or(iterA1m, TRUE, iterC1n), TRUE),
domains=[Exp(Booleans, m), Exp(Booleans, n)]),
domain=Naturals)

Out[30]:
In [31]:
falseEval = Forall(m, Forall(AA, Equals(Or(iterA1m), FALSE), domain=Exp(Set(FALSE), m)),
domain=Naturals)

Out[31]:
In [ ]:


In [32]:
binaryClosure = Forall((A, B), inBool(Or(A, B)), domain=Booleans)

Out[32]:
In [33]:
closure = Forall(m, Forall(AA, inBool(Or(iterA1m)), domain=Exp(Booleans, m)),
domain=Naturals)

Out[33]:
In [34]:
demorgansLawAndToOrBinExplicit = Forall((A,B), Or(A,B), conditions=[Not(And(Not(A), Not(B)))], domain = Booleans)

Out[34]:
In [35]:
demorgansLawAndToOrBin = Forall((A,B), Or(A,B), conditions=[Not(And(Not(A), Not(B)))])

Out[35]:
In [36]:
demorgansLawAndToOr = Forall(m, Forall(AA, Or(iterA1m), conditions=[Not(And(Iter(i, Not(Indexed(AA,i)), one, m)))]),domain = Naturals)

Out[36]:
In [37]:
commutation = Forall((A, B), Equals(Or(A, B), Or(B, A)), domain=Booleans)

Out[37]:
In [38]:
leftwardCommutation = Forall((l, m, n),Forall((AA,BB,C,DD), Equals(Or(iterA1l, iterB1m, C, iterD1n), Or(iterA1l, C, iterB1m, iterD1n)),
domains = [Exp(Booleans, l), Exp(Booleans,m), Booleans, Exp(Booleans, n)]),
domain = Naturals)

Out[38]:
In [39]:
rightwardCommutation = Forall((l, m, n),Forall((AA,B,CC,DD), Equals(Or(iterA1l, B, iterC1m, iterD1n), Or(iterA1l, iterC1m, B, iterD1n)),
domains = [Exp(Booleans, l), Booleans, Exp(Booleans,m), Exp(Booleans, n)]),
domain = Naturals)

Out[39]:
In [40]:
commute = Forall((A, B), Or(B, A), conditions=[Or(A, B)])

Out[40]:
In [41]:
rightwardCommute = Forall((l, m, n), Forall((AA,B,CC,DD), Or(iterA1l, iterC1m, B, iterD1n),
conditions=[Or(iterA1l, B, iterC1m, iterD1n)]),
domain = Naturals)

Out[41]:
In [42]:
leftwardCommute = Forall((l, m, n), Forall((AA,BB,C,DD), Or(iterA1l, C, iterB1m,iterD1n),
conditions=[Or(iterA1l, iterB1m, C, iterD1n)]),
domain = Naturals)

Out[42]:
In [43]:
association = Forall((l,m,n), Forall((AA,BB,CC), Equals(Or(iterA1l, iterB1m, iterC1n),
Or(iterA1l, Or(iterB1m), iterC1n)),
domains = [Exp(Booleans,l), Exp(Booleans,m), Exp(Booleans,n)]),
domain=Naturals)

Out[43]:
In [44]:
disassociation = Forall((l,m,n), Forall((AA,BB,CC), Equals(Or(iterA1l, Or(iterB1m), iterC1n),
Or(iterA1l, iterB1m, iterC1n)),
domains = [Exp(Booleans,l), Exp(Booleans,m), Exp(Booleans,n)]),
domain=Naturals)

Out[44]:
In [45]:
associate = Forall((l,m,n), Forall((AA,BB,CC), Or(iterA1l, Or(iterB1m), iterC1n),
conditions=[Or(iterA1l, iterB1m, iterC1n)]),
domain=Naturals)

Out[45]:
In [46]:
disassociate = Forall((l,m,n), Forall((AA,BB,CC), Or(iterA1l, iterB1m, iterC1n),
conditions=[Or(iterA1l, Or(iterB1m), iterC1n)]),
domain=Naturals)

Out[46]:
In [47]:
%end theorems

Theorems may be imported from autogenerated _theorems_.py