logo
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))
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)))
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)])
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)
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)])
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)
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)
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)
In [25]:
unaryDisjunctionDef = Forall(A, Equals(Or(A), A), domain = Booleans)
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)
In [35]:
demorgansLawAndToOrBin = Forall((A,B), Or(A,B), conditions=[Not(And(Not(A), Not(B)))])
In [36]:
demorgansLawAndToOr = Forall(m, Forall(AA, Or(iterA1m), conditions=[Not(And(Iter(i, Not(Indexed(AA,i)), one, m)))]),domain = Naturals)
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)
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)
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