how to build a "theorem prover" in Excel
 

My objective is to teach formal logic (some theorems of propositional logic)
to people who may know the Excel basic functions and have some knowledge of
logic.

My idea is to use a very simple true table, so I can give it in a beginners
class.

Example : I want to prove the formula : (A^ B) - B

1st STEP (done!)
column A is associated to the function "A", in Excel
column B is associated to the function "B", in Excel
columns A, B., have the logic values of A and B
column C has the formula to prove

TABLE
A B (A^ B ) - B
1 0 0 = OR ((A*B) <= B) +0
2 1 0 = OR ((A*B) <= B) +0
3 0 1 = OR ((A*B) <= B) +0
4 1 1 = OR ((A*B) <= B) +0

result
A B (A^ B ) - B
1 0 0 1
2 1 0 1
3 0 1 1
4 1 1 1

So the given formula is true for all the values of A and B.

2nd STEP
It is given the formula (A^ B) - B written in cell C1,
and the true table must verify it automatically.
I tried the text functions, but it does not work

A B C
1 (A*B ) =< B
2 0 0 = ?
3 1 0 = ?
4 0 1 = ?
5 1 1 = ?

expected result
A B C
1 (A*B ) =< B
2 0 0 1
3 1 0 1
4 0 1 1
5 1 1 1

Any ideas ?

sorry for my English

Regards
Alvaro

how to build a "theorem prover" in Excel
 

I cannot recall how to interpret (A^B)-B
Is it A implies B, therefore if A is true B is true?

On to Excel. Why not use TRUE and FALSE in place of 1/0
But if you do want 1/10 then use =-- OR ((A*B) <= B)
This gets rid of the confusing + 0. Right after the = we have two negations
to coerce Boolean to numeric.
best wishes from Archimedes
--
Bernard Liengme
Microsoft Excel MVP
http://people.stfx.ca/bliengme

"socrates" wrote in message
...
My objective is to teach formal logic (some theorems of propositional
logic)
to people who may know the Excel basic functions and have some knowledge
of
logic.

My idea is to use a very simple true table, so I can give it in a
beginners
class.

Example : I want to prove the formula : (A^ B) - B

1st STEP (done!)
column A is associated to the function "A", in Excel
column B is associated to the function "B", in Excel
columns A, B., have the logic values of A and B
column C has the formula to prove

TABLE
A B (A^ B ) - B
1 0 0 = OR ((A*B) <= B) +0
2 1 0 = OR ((A*B) <= B) +0
3 0 1 = OR ((A*B) <= B) +0
4 1 1 = OR ((A*B) <= B) +0

result
A B (A^ B ) - B
1 0 0 1
2 1 0 1
3 0 1 1
4 1 1 1

So the given formula is true for all the values of A and B.

2nd STEP
It is given the formula (A^ B) - B written in cell C1,
and the true table must verify it automatically.
I tried the text functions, but it does not work

A B C
1 (A*B ) =< B
2 0 0 = ?
3 1 0 = ?
4 0 1 = ?
5 1 1 = ?

expected result
A B C
1 (A*B ) =< B
2 0 0 1
3 1 0 1
4 0 1 1
5 1 1 1

Any ideas ?

sorry for my English

Regards
Alvaro

how to build a "theorem prover" in Excel
 

"I cannot recall how to interpret (A^B)-B
(A^B)-B means: A and B, implies B

The proof of this formula in proposition logic is
(A^B) - B <= ~(A^B) v B <= ~A v ~B v B <= T
The above formula is true whatever the logical values of A and B.
Since ~B v B is true for whatever be the value of B

"Is it A implies B, therefore if A is true B is true?"
Let us analyse your logical expression :

(A - B) - (A-B)
Let us do C = (A -B) C represents the implication
Then
<= C - C
<= ~C v C
<= T
your formula is true whatever the logical values of A and B

What I want is to avoid to write the logical expression (in excel format) in
all the lines of the true table
For 2 variables is 4 lines
For 3 variables is 8 lines
.....
For 6 variables is 64 lines...!

What I want is to write the formula in normal logic frame only once.
Then the true table using any excel functon transforms the formula, and
computes it in all the lines.
If all the lines are "true" or 1, the formula is a tautology

Regards
Alvaro


************************************************** *********
I cannot recall how to interpret (A^B)-B
Is it A implies B, therefore if A is true B is true?

On to Excel. Why not use TRUE and FALSE in place of 1/0
But if you do want 1/10 then use =-- OR ((A*B) <= B)
This gets rid of the confusing + 0. Right after the = we have two negations
to coerce Boolean to numeric.
best wishes from Archimedes
--
Bernard Liengme
Microsoft Excel MVP
http://people.stfx.ca/bliengme

"socrates" wrote in message
...
My objective is to teach formal logic (some theorems of propositional
logic)
to people who may know the Excel basic functions and have some knowledge
of
logic.

My idea is to use a very simple true table, so I can give it in a
beginners
class.

Example : I want to prove the formula : (A^ B) - B

1st STEP (done!)
column A is associated to the function "A", in Excel
column B is associated to the function "B", in Excel
columns A, B., have the logic values of A and B
column C has the formula to prove

TABLE
A B (A^ B ) - B
1 0 0 = OR ((A*B) <= B) +0
2 1 0 = OR ((A*B) <= B) +0
3 0 1 = OR ((A*B) <= B) +0
4 1 1 = OR ((A*B) <= B) +0

result
A B (A^ B ) - B
1 0 0 1
2 1 0 1
3 0 1 1
4 1 1 1

So the given formula is true for all the values of A and B.

2nd STEP
It is given the formula (A^ B) - B written in cell C1,
and the true table must verify it automatically.
I tried the text functions, but it does not work

A B C
1 (A*B ) =< B
2 0 0 = ?
3 1 0 = ?
4 0 1 = ?
5 1 1 = ?

expected result
A B C
1 (A*B ) =< B
2 0 0 1
3 1 0 1
4 0 1 1
5 1 1 1

Any ideas ?

sorry for my English

Regards
Alvaro

how to build a "theorem prover" in Excel
 

A B (A^ B ) - B

As a side note, it's a little easier in vba.

Fx = (a And b) Imp b

--
Dana DeLouis


"alvaro" wrote in message ...

"I cannot recall how to interpret (A^B)-B
(A^B)-B means: A and B, implies B

The proof of this formula in proposition logic is
(A^B) - B <= ~(A^B) v B <= ~A v ~B v B <= T
The above formula is true whatever the logical values of A and B.
Since ~B v B is true for whatever be the value of B

"Is it A implies B, therefore if A is true B is true?"
Let us analyse your logical expression :

(A - B) - (A-B)
Let us do C = (A -B) C represents the implication
Then
<= C - C
<= ~C v C
<= T
your formula is true whatever the logical values of A and B

What I want is to avoid to write the logical expression (in excel format) in
all the lines of the true table
For 2 variables is 4 lines
For 3 variables is 8 lines
....
For 6 variables is 64 lines...!

What I want is to write the formula in normal logic frame only once.
Then the true table using any excel functon transforms the formula, and
computes it in all the lines.
If all the lines are "true" or 1, the formula is a tautology

Regards
Alvaro


************************************************** *********
I cannot recall how to interpret (A^B)-B
Is it A implies B, therefore if A is true B is true?

On to Excel. Why not use TRUE and FALSE in place of 1/0
But if you do want 1/10 then use =-- OR ((A*B) <= B)
This gets rid of the confusing + 0. Right after the = we have two negations
to coerce Boolean to numeric.
best wishes from Archimedes
--
Bernard Liengme
Microsoft Excel MVP
http://people.stfx.ca/bliengme

"socrates" wrote in message
...

My objective is to teach formal logic (some theorems of propositional
logic)
to people who may know the Excel basic functions and have some knowledge
of
logic.

My idea is to use a very simple true table, so I can give it in a
beginners
class.

Example : I want to prove the formula : (A^ B) - B

1st STEP (done!)
column A is associated to the function "A", in Excel
column B is associated to the function "B", in Excel
columns A, B., have the logic values of A and B
column C has the formula to prove

TABLE
A B (A^ B ) - B
1 0 0 = OR ((A*B) <= B) +0
2 1 0 = OR ((A*B) <= B) +0
3 0 1 = OR ((A*B) <= B) +0
4 1 1 = OR ((A*B) <= B) +0

result
A B (A^ B ) - B
1 0 0 1
2 1 0 1
3 0 1 1
4 1 1 1

So the given formula is true for all the values of A and B.

2nd STEP
It is given the formula (A^ B) - B written in cell C1,
and the true table must verify it automatically.
I tried the text functions, but it does not work

A B C
1 (A*B ) =< B
2 0 0 = ?
3 1 0 = ?
4 0 1 = ?
5 1 1 = ?

expected result
A B C
1 (A*B ) =< B
2 0 0 1
3 1 0 1
4 0 1 1
5 1 1 1

Any ideas ?

sorry for my English

Regards
Alvaro