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 iterA1m, iterC1n, iterB1n
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 [30]:
group = Forall((l,m,n), Forall((AA,BB,CC),Or(Iter(i, Indexed(AA,i), one, l), Or(Iter(j,Indexed(BB,j),one,m)), Iter(k, Indexed(CC,k),one,n)), conditions=[Or(Iter(i, Indexed(AA,i), one, l), Iter(j,Indexed(BB,j),one,m), Iter(k, Indexed(CC,k),one,n))], domains = [Exp(Booleans,l), Exp(Booleans,m), Exp(Booleans,n)]),domain = Naturals)
Out[30]:
In [31]:
swap = Forall((l,m,n),Forall((AA,B,CC,D,EE), Or(varIter(AA, one, l), D, varIter(CC, one, m), B, varIter(EE, one, n)), conditions=[Or(varIter(AA, one, l), B, varIter(CC, one, m), D, varIter(EE, one, n))], domains = [Exp(Booleans, l), Booleans, Exp(Booleans,m), Booleans, Exp(Booleans, n)]), domain = Naturals)
Out[31]:
swap:
In [32]:
groupSwap = Forall((i,j,k,l,m), 
                   Forall(AA, Or(varIter(AA, one, i), varIter(AA, Add(k, one), l), varIter(AA, Add(j, one), k), 
                                varIter(AA, Or(i, one), j), varIter(AA, Add(l, one), m)),
                          conditions=[Or(iterA1m)]),
                   domain = Naturals, conditions=[LesserSequence([LessEq._operator_]*4, (i,j,k,l,m))])
Out[32]:
In [33]:
trueEval = Forall((m, n), Forall((AA, CC), Equals(Or(iterA1m, TRUE, iterC1n), TRUE),
                                 domains=[Exp(Booleans, m), Exp(Booleans, n)]),
                  domain=Naturals)
Out[33]:
In [34]:
falseEval = Forall(m, Forall(AA, Equals(Or(iterA1m), FALSE), domain=Exp(Set(FALSE), m)),
                   domain=Naturals)
Out[34]:
In [ ]:
 
In [35]:
binaryClosure = Forall((A, B), inBool(Or(A, B)), domain=Booleans)
Out[35]:
In [36]:
closure = Forall(m, Forall(AA, inBool(Or(iterA1m)), domain=Exp(Booleans, m)),
                 domain=Naturals)
Out[36]:
In [37]:
demorgansLawAndToOrBin = Forall((A,B), Or(A,B), conditions=[Not(And(Not(A), Not(B)))], domain=Booleans)
In [38]:
demorgansLawAndToOr = Forall(m, Forall(AA, Or(iterA1m), conditions=[Not(And(Iter(i, Not(Indexed(AA,i)), one, m)))], domain=Exp(Booleans, m)),domain = Naturals)
In [39]:
%end theorems
Theorems may be imported from autogenerated _theorems_.py