b
We can test it with the classic "ex contradictione quodlibet" (ECQ) example - "if p and not p, then q" for any q:
% lf'solve <<
>>q p
q
So formally, ''q'' is true, whatever it is :) If this sounds overly theoretic, here's a tricky practical example in puzzle solving, Lewis Carroll's last sorites (pp. 123f.). The task is to conclude
something from the following premises:
1. The only animals in this house are cats
1. Every animal is suitable for a pet, that loves to gaze at the moon
1. When I detest an animal, I avoid it
1. No animals are carnivorous, unless they prowl at night
1. No cat fail to kill mice
1. No animals ever take to me, except what are in this house
1. Kangaroos are not suitable for pets
1. None but carnivora kill mice
1. I detest animals that do not take to me
1. Animals that prowl at night always love to gaze at the moon
These are encoded to the following one-letter predicates:
* a - avoided by me
* c - cat
* d - detested by me
* h - house, in this
* k - kill mice
* m - moon, love to gaze at
* n - night, prowl at
* p - pet, suitable for
* r - (kanga)roo
* t - take to me
* v - (carni)vorous
So the problem set can be restated, in Spencer-Brown's terms, as
c p a n k h v td m
I first don't understand why all premises can be just written in a row, which amounts to implicit "or", but it seems to work out well.
As we've seen that x is true for any x, we can cancel out such tautologies.
For this, we reformat the expression to a list of values of type x or
!x, that is in turn dumped into a local [array] for existence checking. And when both x and !x exist, they are removed from the expression:
}
proc lf'cancel expression {
set e2 [string map {"< " ! "> " ""} [split $expression ""]]
foreach term $e2 {if {$term ne ""} {set a($term) ""}}
foreach var [array names a ?] {
if [info exists a(!$var)] {
set expression [string map [list <$var> "" $var ""] $expression]
}
}
set expression
}
puts [lf'cancel {c p a n k h v td m}]
if 0 {
which results in:
a
translated back: "I avoid it, or it's not a kangaroo", or, reordered,
" a" which by (4) means, "All kangaroos are avoided by me".
----
Afterthought: See also [NAND] for how all Boolean operations can be constructed out of the single NAND ("not-and") operator.
----
See also http://www.lawsofform.org/ and whatever Google brings up for "Spencer-Brown laws form"
----
'''A Little Bit O' History'''
* Ampheck : http://planetmath.org/encyclopedia/Ampheck.html
'''Links Lately Added'''
* http://planetmath.org/encyclopedia/LogicalGraph.html
* http://planetmath.org/encyclopedia/MinimalNegationOperator.html
* http://planetmath.org/encyclopedia/ZerothOrderLogic.html
Jon Awbrey : http://www.mywikibiz.com/Directory:Jon_Awbrey
----
[Arts and Crafts of Tcl-Tk Programming]
----
!!!!!!
%|[Category Mathematics]|%
!!!!!!