logo

Demonstrations for the theory of proveit.logic.booleans

In [1]:
import proveit
from proveit.logic import Boolean, TRUE, FALSE, in_bool, Implies, Not, And, Or, Forall
from proveit.logic import Equals, NotEquals, InSet
from proveit import A, B, C, P, Q, PofA, QofA, Function
from proveit.logic import PofTrue, PofFalse, QimplPofTrue, QimplPofFalse
%begin demonstrations
In [2]:
Equals(TRUE, TRUE).prove()
In [3]:
Equals(FALSE, FALSE).prove()
In [4]:
NotEquals(TRUE, FALSE).prove()
In [5]:
in_bool(A).fold(assumptions=[Or(Equals(A, TRUE), Equals(A, FALSE))])
In [6]:
InSet(TRUE, Boolean).prove()
In [7]:
InSet(FALSE, Boolean).prove()
In [8]:
in_bool(A).prove(assumptions=[A])

in_bool_if_false

In [9]:
in_bool(A).conclude(assumptions=[Not(A)])
In [10]:
NotEquals(A, FALSE).prove(assumptions=[A])

from_not_false

In [11]:
A.prove(assumptions=[NotEquals(A, FALSE), in_bool(A)])

fold_forall_over_bool

In [12]:
Forall(A, PofA, domain=Boolean).prove(assumptions=[PofTrue, PofFalse])

fold_conditioned_forall_over_bool

In [13]:
Forall(A, PofA, domain=Boolean, conditions=[QofA]).prove(assumptions=[QimplPofTrue, QimplPofFalse])

forall_bool_eval_true

In [14]:
Equals(Forall(A, PofA, domain=Boolean), TRUE).prove(assumptions=[Equals(PofTrue, TRUE), Equals(PofFalse, TRUE)])

unfold_forall_over_bool

In [15]:
Forall(A, PofA, domain=Boolean).unfold(assumptions=[Forall(A, PofA, domain=Boolean)])

ForallBoolEvalFalseViaFF

In [16]:
#Implies(And(Equals(PofTrue, FALSE), Equals(PofFalse, FALSE)), Equals(Forall(A, PofA, domain=Boolean), FALSE)).prove().proof()

ForallBoolEvalFalseViaFT

In [17]:
#Implies(And(Equals(PofTrue, FALSE), Equals(PofFalse, TRUE)), Equals(Forall(A, PofA, domain=Boolean), FALSE)).prove().proof()

ForallBoolEvalFalseViaTF

In [18]:
#Implies(And(Equals(PofTrue, TRUE), Equals(PofFalse, FALSE)), Equals(Forall(A, PofA, domain=Boolean), FALSE)).prove().proof()
In [19]:
Or(A, Not(A)).prove(assumptions=[in_bool(A)])

from_excluded_middle

In [20]:
Forall(A, C, domain=Boolean,conditions=[Implies(A, C),Implies(Not(A), C)]).prove()
In [21]:
example_forall = Forall(A, Forall(B, Function(P, [A, B]), domain=Boolean), domain=Boolean)
example_forall:
In [22]:
example_forall.all_instance_exprs()[-1]
In [23]:
%end demonstrations