Abstract: This note describes how small Joy sets (of up to 32 members) can be used to encode the lines in a truth table for up to five propositions. This results in a surprisingly simple method of providing truth table tests for the modal status of formulas (or other modal predicates).

Contents:

• Truthfunctional and set-theoretic operations
• Set operations in Joy
• Truth tables for Joy postfix formulas
• Using minimally parenthesised infix notation
• Using Cambridge notation
• Other applications

Truth tables are the simplest way to determine the modal status of a formula: if it is true in all lines then it is a tautology, if it is false in all lines then it is a contradiction, and if it is true in some lines and false in others then it is contingent. The truthfunctional connectives are normally taken to operate on the two truth values, true and false. There is an obvious relationship between the connectives in a formula and the set of lines in the truth table in which the formula is true: The set of lines in which the negation of a formula is true is just the set-theoretic complement of the lines in which the formula itself is true, the set of lines in which the conjunction of two formulas is true is just the set-theoretic intersection of the lines in which both component formulas are true, and so on.

Hence, instead of evaluating a formula line by line in the truth table, one could just use the set-theoretic operations to determine the set of lines in which the formula is true. Whether this is efficient depends on the relative speed of the truthfunctional (one-bit) operations and the set-theoretic (many-bit) operations. Most computers now have word-wide Boolean operations and 32 or even more bits per word. and So, set-theoretic operations on sets of up to 32 or even more members are as efficient as are the truthfunctional operations. This can be exploited for truth tables, and it has the potential of improving performance of small truth tables by a factor of up to 32, and even higher for larger size words. With 32 bits per word, a single word can codify the set of lines of a truth table generated by five propositions (2^5 = 32).

Of course nothing can escape the eventual exponential explosion. For six propositions the truth table has 2^6 = 64 lines, and, as always, any additional proposition doubles the size. So, a six proposition truth table would need to be encoded in two words, and then it doubles. However, the 32-fold increase in speed will hold no matter how many words are needed for the truth table. Moreover, computers with 64-bit words are already becoming more common, and 128-bit words are not far off. Indeed, some machines alredy have 128-bit registers, and a few can operate on several such registers in one cycle.

The rest of this note illustrates the general principle, using just one 32-bit word per truth table, and hence is restricted to a maximum of 5 propositions per table.

Set operations in Joy

The language Joy has as small sets of (generallly 32) integers from 0 onwards (generally up to 31). These integers can be taken to be the line numbers of a truth table, starting with line number 0.

What is needed, for each atomic proposition, is the set of line numbers of the lines in which that proposition is true. In the usual way of writing truth tables, these are the five guide columns. In setlib.joy, the standard Joy libray for (small and large) sets, there is a module ss for small (32-bit) sets which contains, among others, just the right definitions for the current purpose. These definitions are here reproduced for convenience:

    s1  == { 0  2  4  6  8 10 12 14 16 18 20 22 24 26 28 30 };
    s2  == { 0  1  4  5  8  9 12 13 16 17 20 21 24 25 28 29 };
    s4  == { 0  1  2  3  8  9 10 11 16 17 18 19 24 25 26 27 };
    s8  == { 0  1  2  3  4  5  6  7  8 17 18 19 20 21 22 23 };
    s16 == { 0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 };

The names for these sets have been chosen because they are descriptive for general use, but they are not customary in logic. Moreover, since these sets are defined inside a module, they would have to be referenced as ss.s1, ss.s2, ss.s4 and so on. But this is easily overcome by some definitions, chosing p, q, r and so on. Also, it is necessary to load the setlib.joy library:

"setlib" libload.

DEFINE
  p == ss.s1; q == ss.s2; r == ss.s4; s == ss.s8; t == ss.s16.

Joy has the Boolean operators 'and', 'or' and 'not', and they are defined for the two Boolean types of truth values and (small) sets. So these three can already be used for the operations on sets of lines.

But in logic one frequently uses material implication and material equivalence, and these operations will be needed. In the definition below they have been chosen as say, 'imp' and 'iff'. Also, a set of lines represents a tautology if and only if it comprises all lines if and only if it is the universal set. In the definition below the predicate 'tautology' is defined to be true if the complement of the set is empty.

DEFINE
  imp == [not] dip or;
  iff == [imp] [swap imp] cleave and popd;
  tautology == not null
END

No further definitions are needed. The Joy interpreter can now read formulas in Joy postfix notation and determine whether they are tautologies. It does so simply by executing them and then use tre 'tautology' predicate to determine whether what is on top of the stack is the unversal set.

p q imp p and  q  imp tautology.
true
p q imp q and  p  imp tautology.
false
p q or  p r imp  q s imp  and and   r s or   imp  tautology.
true
p q or  p r imp  q s imp  and and   r s and  imp  tautology.
false

A formula that is not a tautology is either contingent or it is a contradiction. It might be useful to have two more predicates for this. But simpler still is to have a function 'modality' which simply determines which of the three possibilities obtains.

DEFINE
  modality ==
	[ [ [null] "contradiction" ]
	  [ [not null] "tautology" ]
	  [ "contingent" ] ]
	cond
	popd
END

p p not and   modality.
"contradiction"
p q not and   modality.
"contingent"
p p not  or   modality.
"tautology"

p q imp p and  q  imp modality.
"tautology"
p q imp p and  q  imp not  modality.
"contradiction"
p q imp q and  p  imp modality.
"contingent"
p q imp q and  p  imp not  modality.
"contingent"
p q imp  p not q imp  iff  modality.
"contingent"
p q imp  q not p not imp  iff  modality.
"tautology"
p q or  p r imp  q s imp  and and   r s or   imp  modality.
"tautology"
p q or  p r imp  q s imp  and and   r s or   imp  not  modality.
"contradiction"
p q or  p r imp  q s imp  and and   r s and  imp  modality.
"contingent"
p q or  p r imp  q s imp  and and   r s and  imp  not  modality.
"contingent"

Reverse Polish notation may be second nature to Joy programmers, but it is not to logicians who would prefer a more familiar notation. The Joy system has a library symlib.joy for symbolic manipulation. It includes many translators from various notations to others. One familiar notation is infix, with precedences for the binary operators to minimise the need for parentheses. The translating function to reverse Polish is called Min2Rev. But the library has to loaded, and it needs to be told which operators are to be used, and what their precedences are:

"symlib"  libload.

DEFINE
  unops == [not];
  bin3ops == [and];
  bin2ops == [or];
  bin1ops == [imp iff];
END

[ [p imp q] and p  imp  q ] Min2Rev i tautology.
true
[ [p imp q] and q  imp  p ] Min2Rev i tautology.
false

DEFINE
  Mtautology == Min2Rev i tautology;
  Mmodality  == Min2Rev i modality
END

[ [p imp q] iff [not p or q] ]  Mtautology.
true
[ [p imp q] iff [not q or p] ]  Mtautology.
false
[ [p or q] and [p imp r] and [q imp s]  imp  [r or s] ]  Mmodality.
"tautology"
[ [p imp q] iff [q imp p] ]  Mmodality.
"contingent"

[ [ [p imp q] and [q imp r] and [r imp s] and [s imp t] ]
  imp [p imp t] ]
Mmodality.
"tautology"

[ [[p imp q] and [q imp r] and [s imp r] and [s imp t]]
  imp  [p imp t] ]
Mmodality.
"contingent"

In the symlib.joy library there is also a translator from Cambridge (or Lisp) style notation to Joy notation. The translator is called Cam2Rev, and it is useful to define the following operators straight away:

DEFINE
  Ctautology == Cam2Rev i tautology;
  Cmodality  == Cam2Rev i modality
END

[ iff [not [or p q]]  [and [not p] [not q]] ]  Ctautology.
true
[ imp [and [imp p q] [imp q r]]  [imp p r] ]  Cmodality.
"tautology"
[ imp [and [imp p q] [imp r q]]  [imp p r] ]  Cmodality.
"contingent"

Testing whether the modal status of a single formula is not the only thing one might do. Another obvious application would be a fixed database as a premise, and then several queries as conclusions to determine whether certain facts can be deduced from the database. Not so obvious would be a reverse example, which tests, for several inputs, whether a fixed conclusion follows - and even gives advice accordingly.

For the advice to be at all meaningful, the usual single letter atomic formulas are not so intuitive. It is preferable to use multi-letter formulas, and their lines in the truth table now have to be defined as before:

DEFINE

  raining == ss.s1; windy == ss.s2; cold == ss.s4;
  hot == ss.s8; humid == ss.s16;

  badweather ==
    [ raining and windy  or  cold and windy  or
      raining and cold  or  hot and  humid ]
END

DEFINE
  takeadvice ==
    Min2Rev i
    [ null ]
    [ "inconsistent data" ]
    [ badweather Min2Rev i
      [ [ [and null] "go out" ]
        [ [imp not null] "stay home" ]
        [ "insufficient data" ] ]
      cond ]
    ifte
    popd
END

[ raining and not cold and not [humid or raining] ]		takeadvice.
"inconsistent data"
[ windy and hot and not [hot and not windy] and not raining ]	takeadvice.
"insufficient data"
[ cold and windy ]						takeadvice.
"stay home"
[ not [windy or raining or humid] ]				takeadvice.
"go out"