Logic Calculation part 2

The purpose of Mathcalc8's logic module is to simplify the arithmetic/multiplication formulation that we had introduced in the post 'Logic Part 1'. The logic module uses a function called 'slogic' to evaluate any logical formula and the logical operations in the logical formula are implemented by the following functions :

1. ~x : not(x) or uses '1 - x'
2. x Λ y : and(x,y) or multiplication operator 'x*y'
3. x V y : or(x,y)
4. x → y : imply(x,y)

Uses the last example of the post 'Logic Part 1' :

(x → y) → (~y → ~x)

It can be inputed into Matcalc8 as follows :
Input 1 : clear()
Input 2 : slogic('imply(imply(x,y),imply(not(y),not(x)))')
Ans. (1)*1
The result is (1)*1 (ie. 1). The function 'slogic' do a symbolic expansion of the logical formula and the final result shows that all the expanded terms are exactly cancelled except for the value 1.
Before we continues, we introduces another method to handle the above question. It is called  'proof by contradiction'.
First, noticing the following equivalence argument :

p → q is always true ↔ p Λ not(q) is always false

This argument is actually followed by :

x → y = ~x V y = ~(x Λ ~y)

which are shown as follows :
Input 3 : slogic('or(not(x),y)')
Ans. (1)*1+(-1)*x+(1)*x*y
Input 4 : slogic('not(x*not(y))')
Ans. (1)*1+(-1)*x+(1)*x*y
The answers are both equal to 1 - x + xy which is the logical formula for x → y
With this argument, input 2 can be simplified by replacing the first 'imply' function with an '*'. Input 2 then becomes the following expression and the target of the expression is not 1 but 0 (ie. always false condition):
Input 5 : slogic('imply(x,y)*not(imply(not(y),not(x)))')
Ans. 0
The result is 0. This means that all terms of the logical formula are cancelled and the logical formula is always false.

An always false logical formula is what we called a 'conflict' or 'contradiction' condition.
One advantage of using arithmetic/multiplication formulation to logic is that it can be more easy to find conflict within a set of premises.
Below is an example :
A set of logical statements are listed below as premises :

1. p → q
2. q → r
3. ~r
4. p

We can check the consistence of the above logical statements by using 'and' operations to join all the statements together to form a logical formula :
Input 6 : slogic('imply(p,q)*imply(q,r)*not(r)*p')
Ans. 0

A value of 0 means that there exists conflict. (Note : if the answer is 1, the premises are consistence but they cannot be useful to draw any conclusions) For this example, it is quite obvious that there is a contradiction. Since (from 4) p is true, then (from 1) q is true, and this imply (from 2) r is true. But (from 3) not(r) is true. Since r and not(r) cannot be true at the same time, there results a contradiction.
Below is another example that looks more complicated :

1. a Λ b → c
2. ~c → d Λ f
3. ~f → h Λ a
4. d → false

Input 7 : slogic('imply(a*b,c)*imply(not(c),d*f)*imply(not(f),h*a)*imply(d,0)')
Ans. (1)c*f + (-1)*c*d*f + (1)*a*c*h + (-1)*a*c*d*h + (-1)*a*c*f*h + (1)*a*c*d*f*h
Since the answer is not 0 or 1, these set of premises do not contains contradiction or it is a logical tautolgy.
From the answer, we can also see that all terms contains 'c', this means that these set of premises imply c.
We can check by adding not(c) to the premises :
Input 8 : slogic('imply(a*b,c)*imply(not(c),d*f)*imply(not(f),h*a)*imply(d,0)*not(c)')
Ans. 0
As expected, it gives 0, a contradiction.