logo
In [1]:
from proveit import varIter
from proveit import Lambda, Iter, Indexed
from proveit._common_ import A, B, C, D, AA, CC, 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
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]:
orIfLeft = Forall((A, B), Or(A, B), domain=Booleans, conditions=[A])
Out[15]:
In [16]:
orIfRight = Forall((A, B), Or(A, B), domain=Booleans, conditions=[B])
Out[16]:
In [17]:
constructiveDilemma = Forall((A, B, C, D), Or(C, D), domain=Booleans, 
                             conditions=[Or(A, B), Implies(A, C), Implies(B, D)])
In [18]:
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[18]:
In [19]:
notLeftIfNeither = Forall((A, B), Not(A), conditions=(Not(Or(A, B))))
Out[19]:
In [20]:
notRightIfNeither = Forall((A, B), Not(B), conditions=(Not(Or(A, B))))
Out[20]:
In [ ]:
 
In [21]:
eachInBool = Forall((m, n), Forall((AA, B, CC), inBool(B), conditions=inBool(Or(iterA1m, B, iterC1n))),
                    domain=Naturals)
Out[21]:
In [22]:
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[22]:
In [23]:
notOrIfNotAny = Forall(m, Forall(AA, Not(Or(iterA1m)),  
                                 conditions=[Iter(i, Not(Indexed(AA, i)), one, m)]),
                       domain=Naturals)
Out[23]:
In [24]:
orContradiction = Forall(m, Forall(AA, FALSE, conditions=(Or(iterA1m), Iter(i, Not(Indexed(AA, i)), one, m))),
                         domain=Naturals)
Out[24]:
In [25]:
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[25]:
In [26]:
trueEval = Forall((m, n), Forall((AA, CC), Equals(Or(iterA1m, TRUE, iterC1n), TRUE),
                                 domains=[Exp(Booleans, m), Exp(Booleans, n)]),
                  domain=Naturals)
Out[26]:
In [27]:
falseEval = Forall(m, Forall(AA, Equals(Or(iterA1m), FALSE), domain=Exp(Set(FALSE), m)),
                   domain=Naturals)
Out[27]:
In [ ]:
 
In [28]:
binaryClosure = Forall((A, B), inBool(Or(A, B)), domain=Booleans)
Out[28]:
In [29]:
closure = Forall(m, Forall(AA, inBool(Or(iterA1m)), domain=Exp(Booleans, m)),
                 domain=Naturals)
Out[29]:
In [30]:
%end theorems
Modifying theorem groupSwap in proveit.logic.boolean.disjunction context
groupSwap expression notebook is being updated
Theorems may be imported from autogenerated _theorems_.py