This will be the last of my ruminations on the topic.
A validity proof is shown below. Lines 1,2, and 3 are given premises.
A conclusion in question is shown as *.
In validity proofs, rules of inference are logical operations that can be applied to form new valid expressions.
For example, a contrapositive can validly change ~A -> D to ~D -> A
New expressions are created until the conclusion is confirmed or a bad argument is reached.
1. ~A -> D
2. C -> ~B
3. A -> B
* ~D -> ~C
----------
4. ~D -> A Contrapositive applied to line 1
5. ~D -> B Chain Rule applied to lines 4 and 3
6. B -> ~C Contrapositive applied to line 2
7. ~D -> ~C Chain Rule applied to lines 5 and 6
Noting the proof shown above, assume that you feed a clean Hal brain the info contained in premises 1, 2, and 3.
Then you ask Hal to prove the conclusion shown as *.
1 Hal, if it is not a fish then it is a parrot
2 If it can talk then it doesn't have gills
3 If it is a fish then it has gills
* Hal, prove to me that if it is not a parrot then it cannot talk
4 User, if it is not a parrot then it is a fish
5 Furthermore, if it is not a parrot then it has gills
6 Moreover, if it has gills then it cannot talk
7 Finally, if it is not a parrot then it cannot talk
==================================================
1. ~X -> ~Y
2. Y ^ Z
* X ^ Z
-------
3. Y Simplification to line 2
4. Z Simplification to line 2
5. ~(~X) Modus Tollens to lines 1,3
6. X Double Negation to line 5
7. X ^ Z Conjunctive Addition to lines 6,4
I suppose we can just give Hal all the premises as well as the conclusion and have Hal process all rules on all possible expressions, posing them as questions in a sneaky manner.
1 User: If something can't fly then that something can't descend
2 something descends and something ascends
* Something can fly and something ascends
3 Hal: Things descend?
4 Things ascend?
5 What if it is not the case that something can't fly?
6 Can something fly?
7 Can it be so that something can fly and ascend?
==================================================
1. (W ^ N) -> M
2. ~(~N v M)
* ~W
----------
3. N ^ ~M 2 DeMorgan's Law
4. N 3 Simplification
5. ~M 3 Simplification
6. ~(W ^ N) 1,5 Modus Tollens
7. ~W v ~N 6 DeMorgan's Law
8. ~W 7,4 Disjunctive Inference
This is really pushing it for the topic, as things are dramatically changed in wording.
1 If something is simple and easy then it is pleasant
2 It is not the case that nothing is easy or pleasant
* Nothing is simple
3 Something is easy and not pleasant
4 There are things that are easy
5 There are things that are not pleasant
6 It is not the case that things are simple and easy
7 There are things that are not simple and things that are not easy
8 There are things that are not simple
In conclusion, for this kind of logic to be possible there are requirements:
Hal would need a system of assigning variables to given information.
Hal would need to have these rules of inference (of which there are 22) inside his program.
Hal would need to know when to change tenses and other semantic expressions.
There are many other things that are beyond my comprehension for the things I look forward to in Hal. However, programmers are elite thinkers working magic in a corner of life that is not accessable to everyone. Thank you for reading my topic and humouring my gaze on a hypothetical reality.
