#!/usr/local/bin/perl --       #-*-Perl-*-
#
# This program checks which truth tables are valid for a given set of
# logical axioms.  The axioms are those of the logical system L, but
# could be changed without much problem.

# by default, it does the usual 2-valued logic, but this can be
# overridden using the -t option.  However, since it checks most
# possibilites for truth tables, it is EXTREMELY slow for a 4-valued
# logic.  One could prune the tree of possibilities, but that would be
# like work. 

# The basic scheme is that the truth tables are viewed as an integer
# in base n (where there are n nontrivial columns in the truth table),
# and we just try each in turn.  If any logical axiom does not give a
# true value for some input, this "logic" is not valid and we move on
# to the next.

#    Scott Sutherland,           February 2000
#    scott@math.sunysb.edu
#
use integer;
use Getopt::Std;
#
#  default settings for switches
$verbose=0;
# below are the possible "truth values"
@values = ("T", "F" );     # the first is "exceptional" or "true"
$maxvaluesize=1;
#
#
#  parse command line to override defaults.
#    -v means tell tables which fail, and why
#    -t a,b,c  means use a, b, and c as truth values, with 
#              the first (a) being "true"
getopts('vt:');  # parse arguments
if ( $opt_v) {$verbose=1;}

if ( $opt_t) {
    @values = split(/,/,$opt_t);
    foreach $a (@values) { 
	if (length($a) > $maxvaluesize) { $maxvaluesize=length($a);}
    }
    if ($maxvaluesize>1) {
	for ($i=0; $i<=$#values; $i++) {
	    $values[$i] .= ' 'x(1+$maxvaluesize-length($values[$i]));
	}
    }
}

#
#
$T = $values[0];           # the first value is the true one.
$nvalues = $#values + 1;

#ipairs are the relevant pairs in implication.  We mostly build this to
#avoid considering obvious contradictions and limit our search a bit.
@ipairs = ();
foreach $a ( @values) { 
    foreach $b ( @values ) {
	if ( $a ne $b) { push( @ipairs, $a.$b);} #MP+axioms force A=>A 
    }
}

########### now check what works
tablehead();
for ($j=0; $j< $nvalues**($#ipairs+1); $j++) {
    for ($i=0; $i< $nvalues ** $nvalues; $i++) {
	buildtable($i,$j);
	if (&testtable==0 || $verbose==1 ) { #only print suitable truth tables.
	    printtable($i,$j);
	    print($message."\n");
	}
    }
}

################################# subs below here ###################
sub buildtable {
    local ($nnum, $inum) = ($_[0], $_[1]);
    local ($a, $b, $rest,  $rem, $i);

    # first, set the whole table to "true"
    foreach $a ( @values) { 
	$N{$a} = $T;
        foreach $b ( @values ) { $I{$a.$b} = $T;}
    }
    
    # now set the not-true values
    $rest=$nnum;
    for ($i=0; $rest > 0; $i++) {
	$rem = $rest % $nvalues;
	if ( $rem != 0) { $N{$values[$i]} = $values[$rem] };
	$rest = $rest / $nvalues;
    }

    $rest=$inum;
    for ($i=0; $rest > 0; $i++) {
	$rem = $rest % $nvalues;
	if ( $rem != 0) { $I{$ipairs[$i]} = $values[$rem] };
	$rest = $rest / $nvalues;
    }
}


# this checks whether, for a given meaning of not and implies (ie, for
# a given truth table) the various axioms are tautologies.
#
sub testtable {
    local ($a, $b, $c);
    $message = " ";

   

    foreach $a ( @values ) {
    # check the axioms
      foreach $b ( @values ) {
	  if (A1($a, $b) ne $T ) {
	      $message=sprintf("A1 fails for a=%s b=%s", $a, $b);
	      return(1); 
	  }
	  foreach $c  ( @values ) {
	      if ( A2($a, $b, $c) ne $T ) {
		  $message=sprintf("A2 fails for a=%s b=%s c=%s",$a, $b, $c);
		  return(1);
	      }
	  }
	  if ( A3($a, $b) ne $T ) { 
	      $message=sprintf("A3 fails for a=%s b=%s", $a, $b);
	      return(1); 
	  }
      }
    # check Modus Ponens
      if (MP($a) ne $T) {
	  $message=sprintf("MP(%s) fails", $a);
	  return(1);
      }

  }
  return(0);
}
#
# print a suitable header for the tables.
sub tablehead {
    local ($a, $b);

    print "table\t";
    foreach $a ( @values) { print ' 'x($maxvaluesize+1); };
    print "\t";
    foreach $a ( @values) {
	foreach $b (@values) { print $b; }
	print " ";
    }
    print "\n";

    print "_____\t";
    foreach $a ( @values) { print $a };
    print "\t";
    foreach $a ( @values) {
	foreach $b (@values) { print $a; } 
	print " ";
    }
    print "\n\n";
}
sub printtable {
    local ($a, $b);
    local ($nnum,$inum) = @_ if (@_);

    print "$nnum,$inum\t";
    foreach $a ( @values) { print n($a) };
    print "\t";
    foreach $a ( @values) {
	foreach $b (@values) { print im($b,$a); } 
	print " ";
    }
    print "  ";
}

#### the functions:
#  not (~a)
sub n{
    local ($a) = $_[0];
    $N{$a};
}
# implies (a => b)
sub im{
    local ($a, $b) = ($_[0], $_[1]);
    $I{$a.$b};
}
#
# the axioms
#
##### Modus Ponens
# A and A => B implies B.  Thus we must have im(T,T) = T and 
#                                            im(T,*) ne T  if * ne T.
sub MP {
    local ($a) = $_[0];
    if ($a eq $T) {
	return(im($a,$a));
    }
    if (im($T,$a) ne $T) {
	return($T);
    }
    return($values[$#values]);
}
##### the axioms
# A => (B=>A)
sub A1 {
    local ($a,$b) = ($_[0], $_[1]);
    im($a, im($b, $a));
}
# (A => (B=>C)) => ((A=>B) => (A=>C))
sub A2 {
    local ($a,$b,$c) = ($_[0], $_[1], $_[2]);
    im(im($a, im($b, $c)),
       im(im($a,$b), im($a,$c)));
}
# ((~B => ~A) => ((~B=>A)=>B)
sub A3 {
    local ($a,$b) = ($_[0], $_[1]);
    im(im(n($b), n($a)),
       im( im(n($b), $a), $b));
}

### some theorems, for debugging purposes.
# ~~A => A
sub T1 {
    local ($a) = ($_[0]);
    im(n(n($a)), $a);
}
# A => ~~A
sub T2 {
    local ($a) = ($_[0]);
    im(n(n($a)), $a);
}
# A => A
sub T3 {
    local ($a) = ($_[0]);
    im($a, $a);
}
# (~B => ~A) => (A => B)
sub S1 {
    local ($a, $b) = ($_[0], $_[1]);
    im(im(n($b), n($a)),  im($a,$b));
}