logo

Demonstrations for the theory of proveit.logic.booleans.implication

In [1]:
from proveit.logic import in_bool, Implies, Not, Equals, NotEquals, FALSE, TRUE, NotEquals, Iff, And
from proveit import A, B, C, D
%begin demonstrations

Transitivity

In [2]:
D.prove(assumptions=[A, Implies(A, B), Implies(B, C), Implies(C, D)])
, , ,  ⊢  

Contraposition

In [3]:
Implies(A, B).contrapose(assumptions=[Implies(A, B), in_bool(A)])
,  ⊢  
In [4]:
Implies(Not(A), B).contrapose(assumptions=[Implies(Not(A), B), in_bool(A)])
,  ⊢  
In [5]:
Implies(A, Not(B)).contrapose(assumptions=[Implies(A, Not(B)), in_bool(A)])
,  ⊢  
In [6]:
Implies(Not(A), Not(B)).contrapose(assumptions=[Implies(Not(A), Not(B)), in_bool(A)])
,  ⊢  
In [ ]:
In [ ]:

From tutorial number 3 (implication): An implication has an antecedent and a consequent. If the antecedent is true, the consequent must also be true. Prove-It has an Implies operation that may be used to represent an implication, formatted with the $\Rightarrow$ symbol.

Below, it makes sense that True would imply itself, similar to the fact that $x$ is equal to itself. If we can prove that the Left Hand Side of the implication is True then we can automatically prove that the Right Hand Side is True as well.

In [7]:
Implies(TRUE, TRUE).prove()
 ⊢  

Based upon the above explanation, we can also prove that this expression is True.

In [8]:
Equals(Implies(TRUE, TRUE), TRUE).prove()
 ⊢  

On the other hand. If we can prove that the Left Hand Side is False it doesn't matter what the Right Hand Side is because the entire expression is false. This is taken to the extreme in the Boolean case where False implies both False (which makes sense) and True.

In [9]:
Implies(FALSE, FALSE).prove()
 ⊢  

Therefore, the expression is True.

In [10]:
Implies(FALSE, FALSE).evaluation()
 ⊢  

While False $\Rightarrow$ True may seem contradictory, the Right Hand Side of the expression doesn't matter because the Left Hand Side is False. Therefore, we can automatically conclude that the expression is False.

In [11]:
Implies(FALSE, TRUE).prove()
 ⊢  

Similarly, this expression is True.

In [12]:
Equals(Implies(FALSE, TRUE), TRUE).prove()
 ⊢  

However, the only expression of this type that does not evaluate to True, is the case where True implies False. This case cannot be True because we automatically conclude the Right Hand Side to be True if the Left Hand Side is True. In this case, the Right Hand Side is False, therefore the expresssion cannot be True.

In [13]:
Equals(Implies(TRUE, FALSE),FALSE).prove()
 ⊢  

Similar to the way that we can prove True $\Rightarrow$ True, we can also prove that anything implies itself.

In [14]:
Implies(B,B).prove()
 ⊢  
In [15]:
Not(Implies(TRUE, FALSE)).prove()
 ⊢  

The following case is another example of the fact that it doesn't matter what the Right Hand Side is if the Left Hand Side is False. This time, we are given $\lnot A$, which we take to be True. Then, by definition, $A$ must be False. Therefore, the Right Hand Side can be anything, in this case $B$.

In [16]:
nA = Not(A)
nA:
In [17]:
Implies(A,B).prove(assumptions=[nA])
 ⊢  
In [18]:
Implies(A, C).prove(assumptions=[Implies(A,B), Implies(B,C)])
,  ⊢  
In [19]:
A.prove(assumptions=[Implies(Not(A),FALSE), in_bool(A)])
,  ⊢  
In [20]:
Implies(Not(A),B).deny_antecedent(assumptions=[Not(B), in_bool(A), Implies(Not(A),B)])
, ,  ⊢  
In [21]:
Implies(A,B).deny_antecedent(assumptions=[Not(B), in_bool(A), Implies(A,B)])
, ,  ⊢  
In [22]:
Not(A).prove(assumptions=[Implies(A, FALSE),in_bool(A)])
,  ⊢  
In [23]:
Implies(A,FALSE).derive_via_contradiction(assumptions=[Implies(A, FALSE)])
 ⊢  
In [24]:
Implies(B,A).prove(assumptions=[Not(Implies(A,B))])
 ⊢  
In [25]:
Iff(A, B).prove(assumptions=[Implies(A,B), Implies(B,A)])
,  ⊢  
In [26]:
Not(Iff(B,A)).prove(assumptions=[Not(Implies(B,A))])
 ⊢  
In [27]:
Not(Iff(B,A)).prove(assumptions=[Not(Implies(A,B))])
 ⊢  
In [28]:
Iff(TRUE, TRUE).prove()
 ⊢  
In [29]:
Equals(Iff(TRUE, TRUE), TRUE).prove()
 ⊢  
In [30]:
Iff(FALSE, FALSE).prove()
 ⊢  
In [31]:
Equals(Iff(FALSE, FALSE), TRUE).prove()
 ⊢  
In [32]:
Equals(Iff(TRUE, FALSE), FALSE).prove()
 ⊢  
In [33]:
Not(Iff(TRUE, FALSE)).prove()
 ⊢  
In [34]:
Equals(Iff(FALSE, TRUE), FALSE).prove()
 ⊢  
In [35]:
Not(Iff(FALSE, TRUE)).prove()
 ⊢  
In [36]:
Implies(A,B).prove(assumptions=[Iff(A,B)])
 ⊢  
In [37]:
Implies(A,B).prove(assumptions=[Iff(B,A)])
 ⊢  
In [38]:
Iff(A,B).derive_right(assumptions=[A, Iff(A,B)])
,  ⊢  
In [39]:
Iff(A,B).derive_left(assumptions=[A, Iff(A,B)])
,  ⊢  
In [40]:
Iff(B,A).prove(assumptions=[Iff(A,B)])
 ⊢  
In [41]:
Iff(A,B).apply_transitivity(Iff(B,C), assumptions=[Iff(A,B), Iff(B,C)])
,  ⊢  

SEE CONTRAPOSITION ABOVE

In [42]:
Implies(A, Not(Not(B))).conclude_via_double_negation(assumptions=[Implies(A,B)])
 ⊢  
In [43]:
Equals(A,B).prove(assumptions=[Iff(A,B),in_bool(B), in_bool(A)])
, ,  ⊢  
In [44]:
Equals(A,B).prove(assumptions=[Implies(A,B), Implies(B,A), in_bool(B), in_bool(A)])
, , ,  ⊢  
In [45]:
in_bool(Implies(A,B)).prove(assumptions=[in_bool(B), in_bool(A)])
,  ⊢  
In [46]:
in_bool(Iff(A,B)).prove(assumptions=[in_bool(B), in_bool(A)])
,  ⊢  

Axioms

In [47]:
Iff(A, B).definition()
 ⊢  
In [48]:
%end demonstrations