#!/usr/bin/perl
#
eval 'exec /usr/bin/perl -S $0 ${1+"$@"}' if $running_under_some_shell;

#
# $Id: mally.pl,v 1.7 2002/06/16 19:43:58 lokhorst Exp $
#
# Supplement to G.J.C. Lokhorst, "Mally's Deontic Logic",
# in Edward N. Zalta, ed., Stanford Encyclopedia of Philosophy.
# The Metaphysics Research Lab at the Center for the Study of
# Language and Information, Stanford University, Stanford, CA,
# 2002.
#
############################################################
# BASIC SETUP
# The matrices were discovered by MaGIC version 2.1.4:
# see the output of MaGIC at the end of this program.
############################################################
@n = ( 0, 1, 2, 3, 4, 5 );
$max       = 6;
@matrixCon = (
    ( 0, 0, 0, 0, 0, 0 ), ( 0, 1, 0, 1, 0, 1 ),
    ( 0, 0, 2, 2, 2, 2 ), ( 0, 1, 2, 3, 2, 3 ),
    ( 0, 0, 2, 2, 4, 4 ), ( 0, 1, 2, 3, 4, 5 ),
);
@matrixArrow = (
    ( 5, 5, 5, 5, 5, 5 ), ( 0, 1, 2, 3, 4, 5 ),
    ( 0, 0, 1, 1, 3, 5 ), ( 0, 0, 0, 1, 2, 5 ),
    ( 0, 0, 0, 0, 1, 5 ), ( 0, 0, 0, 0, 0, 5 ),
);
$truth   = 1;
$u       = 2;
@meaning = ( 'ok', 'INVALID' );

############################################################
# CONNECTIVES
############################################################
sub impl {
    return @matrixArrow[ ( $max * $_[0] ) + $_[1] ];
}

sub neg {
    return ( $max - 1 ) - $_[0];
}

sub dot {
    return neg( impl( $_[0], neg( $_[1] ) ) );
}

sub con {
    return @matrixCon[ ( $max * $_[0] ) + $_[1] ];
}

sub dis {
    return neg( con( neg( $_[0] ), neg( $_[1] ) ) );
}

sub equiv {
    return con( impl( $_[0], $_[1] ), impl( $_[1], $_[0] ) );
}

sub obl {
    return impl( $u, $_[0] );
}

sub req {
    return impl( $_[0], obl( $_[1] ) );
}

sub oquiv {
    return con( req( $_[0], $_[1] ), req( $_[1], $_[0] ) );
}

############################################################
# SUBROUTINES
############################################################
sub designated {
    return ( $_[0] % 2 != 0 );
}

sub notdesignated {
    return ( $_[0] % 2 == 0 );
}

sub check0 {
    $ret = 0;
    $ret = 1 if ( notdesignated $_[1]->() );
    print "\t$_[0]: $meaning[$ret]\n";
}

sub check1 {
    $ret = 0;
    CHECK1:
    foreach $a (@n) {
        if ( notdesignated $_[1]->($a) ) {
            $ret = 1;
            last CHECK1;
        }
    }
    print "\t$_[0]: $meaning[$ret]\n";
}

sub check2 {
    $ret = 0;
    CHECK2:
    foreach $a (@n) {
        foreach $b (@n) {
            if ( notdesignated $_[1]->( $a, $b ) ) {
                $ret = 1;
                last CHECK2;
            }
        }
    }
    print "\t$_[0]: $meaning[$ret]\n";
}

sub check3 {
    $ret = 0;
    CHECK3:
    foreach $a (@n) {
        foreach $b (@n) {
            foreach $c (@n) {

                if ( notdesignated $_[1]->( $a, $b, $c ) ) {
                    $ret = 1;
                    last CHECK3;
                }
            }
        }
    }
    print "\t$_[0]: $meaning[$ret]\n";
}

sub check4 {
    $ret = 0;
    CHECK4:
    foreach $a (@n) {
        foreach $b (@n) {
            foreach $c (@n) {

                foreach $d (@n) {
                    if ( notdesignated $_[1]->( $a, $b, $c, $d ) ) {
                        $ret = 1;
                        last CHECK4;
                    }
                }
            }
        }
    }
    print "\t$_[0]: $meaning[$ret]\n";
}

sub checkrule2 {
    $ret = 0;
    CheckRule2:
    foreach $a (@n) {
        if ( designated $a ) {
            foreach $b (@n) {

                if ( designated $_[1]->( $a, $b ) ) {
                    if ( notdesignated $_[2]->( $a, $b ) ) {
                        $ret = 1;
                        last CheckRule2;
                    }
                }
            }
        }
    }
    print "\t$_[0]: $meaning[$ret]\n";
}

############################################################
# Output starts here
############################################################
printf "Read %s for information on this program.\n", $0;
print "Matrices\n";
print "\t- |\n";
print "\t--+--\n";

foreach $a (@n) {
    printf "\t%d | %d\n", $a, neg($a);
}
print "\n";
print "\t-> | 0 1 2 3 4 5\n";
print "\t---+------------\n";

foreach $a (@n) {
    printf "\t %d |", $a;
    foreach $b (@n) {
        printf " %d", impl( $a, $b );
    }
    print "\n";
}
print "\n";
print "\t& | 0 1 2 3 4 5\n";
print "\t--+------------\n";

foreach $a (@n) {
    printf "\t%d |", $a;
    foreach $b (@n) {
        printf " %d", con( $a, $b );
    }
    print "\n";
}
print "\n";
print "\tv | 0 1 2 3 4 5\n";
print "\t--+------------\n";

foreach $a (@n) {
    printf "\t%d |", $a;
    foreach $b (@n) {
        printf " %d", dis( $a, $b );
    }
    print "\n";
}
print "Designated Values:";

foreach $a (@n) {
    if ( designated $a ) { printf " %d", $a }
}
print "\n";

############################################################
print "Alethic Axioms\n";
check1( 'Self-implication', sub { return impl( $_[0], $_[0] ) } );
check3(
  'Prefixing', sub {
      return impl( impl( $_[0], $_[1] ),
        impl( impl( $_[2], $_[0] ), impl( $_[2], $_[1] ) ) );
} );
check2(
  'Contraction', sub {
      return impl( impl( $_[0], impl( $_[0], $_[1] ) ), impl( $_[0], $_[1] ) );
} );
check3(
  'Permutation', sub {
      return impl(
        impl( $_[0], impl( $_[1], $_[2] ) ),
        impl( $_[1], impl( $_[0], $_[2] ) )
      );
} );
check1(
  'A <-> (t -> A)', sub {
      return equiv( $_[0], impl( $truth, $_[0] ) );
} );
check1(
  'Double Negation', sub {
      return impl( neg( neg( $_[0] ) ), $_[0] );
} );
check2(
  'Contraposition', sub {
      return impl( impl( $_[0], neg( $_[1] ) ), impl( $_[1], neg( $_[0] ) ) );
} );
check2( '& Elimination', sub { return impl( con( $_[0], $_[1] ), $_[0] ) } );
check2( '& Elimination', sub { return impl( con( $_[0], $_[1] ), $_[1] ) } );
check3(
  '& Introduction', sub {
      return impl( con( impl( $_[0], $_[1] ), impl( $_[0], $_[2] ) ),
        impl( $_[0], con( $_[1], $_[2] ) ) );
} );
check2( 'v Introduction', sub { return impl( $_[0], dis( $_[0], $_[1] ) ) } );
check2( 'v Introduction', sub { return impl( $_[1], dis( $_[0], $_[1] ) ) } );
check3(
  'v Elimination', sub {
      return impl( con( impl( $_[0], $_[2] ), impl( $_[1], $_[2] ) ),
        impl( dis( $_[0], $_[1] ), $_[2] ) );
} );
check3(
  'Distribution', sub {
      return impl(
        con( $_[0], ( dis( $_[1], $_[2] ) ) ),
        dis( con( $_[0], $_[1] ), $_[2] )
      );
} );

############################################################
print "Rules of Inference\n";
checkrule2(
  "MP", sub { return impl( $_[0], $_[1] ) }, sub {
      return $_[1];
} );
checkrule2( "Adj", sub { return $_[1] }, sub { return con( $_[0], $_[1] ) } );

############################################################
print "Deontic Axioms\n";
check3(
  'I.', sub {
      return impl( con( req( $_[0], $_[1] ), impl( $_[1], $_[2] ) ),
        req( $_[0], $_[2] ) );
} );
check3(
  'II.', sub {
      return impl( con( req( $_[0], $_[1] ), req( $_[0], $_[2] ) ),
        req( $_[0], con( $_[1], $_[2] ) ) );
} );
check2(
  'III.', sub {
      return equiv( req( $_[0], $_[1] ), obl( impl( $_[0], $_[1] ) ) );
} );
check0( 'IV', sub { return obl($u) } );
check0( 'V', sub { return neg( req( $u, neg($u) ) ) } );

############################################################
print "Mally's Formulas\n";
check2(
  '(1)', sub {
      return impl( impl( $_[0], obl( $_[1] ) ), impl( $_[0], obl($truth) ) );
} );
check2(
  '(2)', sub {
      return impl( impl( $_[0], obl( neg($truth) ) ),
        impl( $_[0], obl( $_[1] ) ) );
} );
check3(
  '(3)', sub {
      return impl( dis( req( $_[2], $_[0] ), req( $_[2], $_[1] ) ),
        req( $_[2], dis( $_[0], $_[1] ) ) );
} );
check4(
  '(4)', sub {
      return impl(
        con( req( $_[3], $_[0] ), req( $_[2], $_[1] ) ),
        req( con( $_[3], $_[2] ), con( $_[0], $_[1] ) )
      );
} );
check2(
  '(5)', sub {
      return con(
        impl( obl( $_[0] ), impl( $_[1], obl( $_[0] ) ) ),
        impl( impl( $truth, obl( $_[0] ) ), obl( $_[0] ) )
      );
} );
check2(
  '(6)', sub {
      return req( con( obl( $_[0] ), impl( $_[0], $_[1] ) ), $_[1] );
} );
check1( '(7)', sub { return impl( obl( $_[0] ), obl($truth) ) } );
check3(
  '(8)', sub {
      return impl( con( req( $_[0], $_[1] ), req( $_[1], $_[2] ) ),
        req( $_[0], $_[2] ) );
} );
check2(
  '(9)', sub {
      return req( con( obl( $_[0] ), req( $_[0], $_[1] ) ), $_[1] );
} );
check2(
  '(10)', sub {
      return equiv( con( obl( $_[0] ), obl( $_[1] ) ),
        obl( con( $_[0], $_[1] ) ) );
} );
check2(
  '(11)', sub {
      return equiv( oquiv( $_[0], $_[1] ), obl( equiv( $_[0], $_[1] ) ) );
} );
check2(
  '(12)', sub {
      return equiv( obl( impl( $_[0], $_[1] ) ),
        obl( neg( con( $_[0], neg( $_[1] ) ) ) ) );
} );
check2(
  '(13)', sub {
      return equiv( req( $_[0], $_[1] ),
        neg( con( $_[0], neg( obl( $_[1] ) ) ) ) );
} );
check2(
  '(14)', sub {
      return equiv( req( $_[0], $_[1] ), req( neg( $_[1] ), neg( $_[0] ) ) );
} );
check1( '(15)', sub { return impl( $_[0], obl($u) ) } );
check1( '(16)', sub { return req( impl( $u, $_[0] ), $_[0] ) } );
check1( '(17)', sub { return req( req( $u, $_[0] ), $_[0] ) } );
check1( '(18)', sub { return req( obl( obl( $_[0] ) ),   $_[0] ) } );
check1( '(19)', sub { return equiv( obl( obl( $_[0] ) ), obl( $_[0] ) ) } );
check1(
  '(20)', sub {
      return equiv( impl( $u, obl( $_[0] ) ), oquiv( $_[0], $u ) );
} );
check1( '(21)', sub { return equiv( obl( $_[0] ), oquiv( $_[0], $u ) ) } );
check0( '(22)', sub { return obl($truth) } );
check0( '(23)',  sub { return oquiv( $truth, $u ) } );
check0( "(23')", sub { return req( $truth,   $u ) } );
check1( '(24)', sub { return impl( $_[0], obl( $_[0] ) ) } );
check2(
  '(25)', sub {
      return impl( impl( $_[0], $_[1] ), impl( $_[0], obl( $_[1] ) ) );
} );
check2(
  '(26)', sub {
      return impl( equiv( $_[0], $_[1] ), oquiv( $_[0], obl( $_[1] ) ) );
} );
check1( '(27)', sub { return impl( neg($u),  obl( $_[0] ) ) } );
check0( '(28)', sub { return impl( neg($u),  obl( neg($u) ) ) } );
check0( '(29)', sub { return impl( neg($u),  obl($u) ) } );
check0( '(30)', sub { return req( neg($u),   neg($truth) ) } );
check0( '(31)', sub { return oquiv( neg($u), neg($truth) ) } );
check0( '(32)', sub { return neg( impl( $u, obl( neg($truth) ) ) ) } );
check0( '(33)', sub { return neg( impl( $u, neg($truth) ) ) } );
check0( '(34)', sub { return equiv( $u, $truth ) } );
check0( '(35)', sub { return equiv( neg($u), neg($truth) ) } );
print "Done\n";

############################################################
# Output from MaGIC. NB: u o u = ~(u -> ~u).
############################################################
# Logic: R
# Extra: (u o u) o u
# Fragment: ->, &, v, ~, o, t, f, T, F
# Definition: u Primitive (cut)
# Fail: u o u
# Search concludes when 1 matrix found
# or when size 14 finished.
#
# Size: 6
#
# Negation table 6.1
# a | 0 1 2 3 4 5
# ---+------------
# ~a | 5 4 3 2 1 0
#
# Order 6.1.1
# < | 0 1 2 3 4 5
# --+------------
# 0 | + + + + + +
# 1 | - + - + - +
# 2 | - - + + + +
# 3 | - - - + - +
# 4 | - - - - + +
# 5 | - - - - - +
#
# Choice 6.1.1.1 of t: 1
#
# Implication matrix 6.1.1.1.1
# -> | 0 1 2 3 4 5
# ---+------------
# 0 | 5 5 5 5 5 5
# 1 | 0 1 2 3 4 5
# 2 | 0 0 1 1 3 5
# 3 | 0 0 0 1 2 5
# 4 | 0 0 0 0 1 5
# 5 | 0 0 0 0 0 5
# Choice 6.1.1.1.1.1 of u: 2
# Failure: u o u
#
############################################################
# That's all for now.
############################################################