[FOM] Truth value algorithm for tokens

[Axiomize@aol.com]

On 30 Oct 2002, Sandy Hodges wrote:

> I've posted a write-up of my latest algorithm.  As always,
> comments and refutations are appreciated.

> Token a:  ~ Fa(d) & (0=0 <=> Fa(c))    false
> Token b:  ~ ((Tr(c) => Tr(d)) or Fa(a))    gap
> Token c:  (Tr(g) or 1=0) & Fa(d) <=> (~ Tr(f) <=> 1=0)    gap
> Token d:  0=0 <=> Tr(d) or Tr(a)    gap
> Token e:  1=0 & Tr(c) <=> (Tr(e) <=> Fa(g))    gap
> Token f:  ~ ((0=0 <=> Tr(c)) or (Fa(b) <=> Tr(c)))    gap
> Token g:  ~ Fa(h) & (Fa(d) => Fa(e))    true
> Token h:  ~ (Tr(b) & (Fa(a) or Tr(g)))    true

Is this not the satisfiability (SAT) problem?  That is, each token is a 
Boolean variable, each such variable x that states a formula y means that x<=>
y, creating xv~y and ~xvy, and if the resulting clauses are not satisfiable 
then we have a paradox.

"This is false." yields clauses x and ~x, while "This is true." yields clause 
xv~x.

If gap is allowed as a value, then we have the multivalued satisfiablility 
problem.  In this case, each 3-valued variable can be encoded into 2 Boolean 
variables, or 3 Boolean variables where each original value (true, false, 
gap) is represented by a separate Boolean variable ("one-hot encoding").

One-hot encoded, let Boolean variables a1, a2 and a3 represent Token a being 
true, false and gap, respectively, and similarly for Tokens b-h.  Then the 
clauses by definition of the variables for Token a are:

a1 v a2 v a3
~a1 v ~a2
~a1 v ~a3
~a2 v ~a3

Token a states a1<=>(~d2^c2) creating a1v~(~d2^c2) and ~a1v(~d2^c2) for 
clauses:

a1 v d2 v ~c2
~a1 v ~d2
~a1 v c2

and similarly for the other tokens.

Would it be better to use established terminology and relate your methods to 
the vast literature on the SAT problem (e.g. the Davis-Putnam algorithm and 
its derivatives)?

Charlie Volkstorf
Cambridge, MA

> Sandy Hodges / Alameda,  California,   USA
> mail to SandyHodges at attbi.com will reach me.