Decidability algorithm for the implicational fragment of minimal logic

implicational.py

# Simple implementation of proving/disproving implicational statements

from collections import namedtuple

# String constants

lBOT = '⊥'
lNEG = '¬'
lIMP = ' → '
lMMP = ' ⇒ '
lVDA = ' ⊢ '
lNVD = ' ⊬ '

# Utils

compose = lambda f: lambda g: lambda *a, **k: f(g(*a, **k))

def csv(it):
    return '{' + ', '.join(map(str, sorted(it, key=str))) + '}'

def log(n, *args):
    print('\t' * n + str(args[0]), *args[1:])


# Formulae

class Prop:
    def is_atom(self):
        return isinstance(self, Atom)

    def is_arrow(self):
        return isinstance(self, Arrow)

    def is_simple(self):
        return self.is_arrow() and self.premise.is_atom()

    def is_left(self):
        return self.is_arrow() and self.premise.is_arrow()

    # Warning: not right-associative
    def __rshift__(self, shift):
        return Arrow(self, shift)

    def __invert__(self):
        return Arrow(self, bot)

    def __hash__(self):
        return hash(repr(self))


class Atom(Prop, namedtuple('Atom', 'name')):
    def paren_str(self):
        return str(self)

    def __eq__(self, other):
        return repr(self) == repr(other)

    def __hash__(self):
        return hash(repr(self))

    def __str__(self):
        return self.name


class Arrow(Prop, namedtuple('Arrow', 'premise conclusion')):
    def paren_str(self):
        if self.conclusion is bot:
            return str(self)
        else:
            return f'({self})'

    def __eq__(self, other):
        return repr(self) == repr(other)

    def __hash__(self):
        return hash(repr(self))

    def __str__(self):
        if self.conclusion is bot:
            return lNEG + self.premise.paren_str()
        else:
            return self.premise.paren_str() + lIMP + str(self.conclusion)


bot = Atom(lBOT)


# Deductions

class Deduction:
    def __str__(self):
        return csv(self.assumptions) + lVDA + str(self.prop)


class Assume(Deduction):
    def __init__(self, prop):
        self.assumptions = frozenset({prop})
        self.prop = prop
        self.parents = ()


class Intro(Deduction):
    def __init__(self, premise, d):
        self.assumptions = d.assumptions - {premise}
        self.prop = Arrow(premise, d.prop)
        self.parents = (d, )


class Elim(Deduction):
    def __init__(self, d1, d2):
        assert(d1.prop.premise == d2.prop)
        self.assumptions = d1.assumptions | d2.assumptions
        self.prop = d1.prop.conclusion
        self.parents = (d1, d2)


# Kripke trees

class Tree:
    def __init__(self, labels, branches=(), disproves=None):
        assert(all(x in b.labels for x in labels for b in branches))
        self.labels = labels
        self.branches = branches
        self.disproves = disproves
        print(self)
        assert(disproves is None or not self.forces(disproves))

    def forces(self, x):
        if x.is_atom():
            return x in self.labels
        else:
            return (self.forces(x.conclusion)
                    or (not self.forces(x.premise)
                        and all(b.forces(x) for b in self.branches)))

    def __repr__(self):
        return 'Tree({}, {}, {})'.format(repr(self.labels), repr(self.branches), repr(self.disproves))

    @compose('\n'.join)
    def _indent(self, n=0):
        for line in str(self).split('\n'):
            yield ' ' * n + line

    @compose('\n'.join)
    def __str__(self):
        yield '\- ' + csv(self.labels) + ' \t\t ' + str(self.disproves)
        for branch in self.branches:
            yield branch._indent(1)


# Algorithm

def reduced(partials, n=0):
    '''Combine partial proofs to get the simplest set of conclusions.'''
    log(n, "Simplifying", csv(partials))
    modified = True
    while modified:
        modified = False
        new_partials = set()
        for p in partials:
            if p.prop.is_arrow():
                for q in partials:
                    if p.prop.premise == q.prop:
                        r = Elim(p, q)
                        log(n, "From", p.prop, "and", q.prop, ", get", r.prop)
                        new_partials.add(r)
                        modified = True
                        break
                else:
                    new_partials.add(p)
            else:
                new_partials.add(p)
        partials = new_partials
    return partials


def examine(goal, partials=None, n=0):
    '''Get a proof or a countermodel of a formula.'''
    partials = partials or set()
    log(n, "Trying to prove", csv(x.prop for x in partials), lVDA, goal)
    original_goal = goal
    new_assumptions = []
    # First, restate the problem by simplifying the right side
    while goal.is_arrow():
        log(n, "Assume", goal.premise, "and prove", goal.conclusion)
        new_assumptions.append(Assume(goal.premise))
        goal = goal.conclusion
    partials |= set(new_assumptions)
    while True:
        partials = reduced(partials, n)
        log(n, "Now trying to prove", csv(x.prop for x in  partials), lVDA, goal)
        # Check if the goal is already proved by an assumption
        for p in partials:
            if goal == p.prop:
                log(n, "Which is trivial.")
                log(n, "We have", csv(p.assumptions), lVDA, p.prop)
                while new_assumptions:
                    p = Intro(new_assumptions.pop().prop, p)
                    log(n, "so", csv(p.assumptions), lVDA, p.prop)
                return p, None
        # Check if any of the left-nested premises can be proved
        models = []
        for d in (x for x in partials if x.prop.is_left()):
            log(n, "Perhaps", d.prop.premise,
                "can be proved from", csv(x.prop for x in partials - {d}), "?")
            proof, model = examine(d.prop.premise, partials - {d}, n + 1)
            if model:
                log(n, "Sadly not")
                models.append(model)
            else:
                # Proved a left-nested premise. Continue
                partials = (partials - {d}) | {Elim(d, proof)}
                break
        else:
            # No left-nested premises are provable.
            # Combine all countermodels together
            log(n, "No provable left-nested premises found.")
            model = Tree([x.prop for x in partials if x.prop.is_atom()],
                         models,
                         original_goal)
            assert(not model.forces(goal))
            return None, model

A = Atom('A')
B = Atom('B')
C = Atom('C')
D = Atom('D')
P = Atom('P')
Q = Atom('Q')
R = Atom('R')


#print(examine(A >> (B >> A)))
#print()
#print(examine(A >> (B >> ~(~~A >> ~~~B))))
#
#examine(~(A >> B) >> ~~(B >> A))                          #  1   IMPL
#print()
#examine(A >> (~A >> B))                                   #  2   IMPL
#print()
#examine(A >> (~B >> ~~~B))                                #  3   IMPL
#print()
#examine(~(A >> B) >> ~~~B)                                #  4   IMPL
#print()
#examine(~A >> (A >> B))                                   #  5
#print()
#examine((~A >> A) >> A)                                   #  6
#print()
#examine((A >> (B >> C)) >> (~(A >> C) >> ~~(B >> C)))     #  7   IMPL
#print()
#examine((A >> (B >> C)) >> ~~(~(A >> C) >> ~~~~(B >> C))) #  8   IMPL
#print()
#examine(~(A >> B) >> A)                                   #  9a  IMPL
#print()
#examine(~(A >> B) >> ~B)                                  #  9b  IMPL
#print()
#examine(((A >> B) >> A) >> A)                             # 10       (& 11 IMPL)
#print()
#examine((~~~A >> ~~A) >> A)                               # 12   IMPL
#print()
#examine(~A >> ~~(A >> B))                                 # 13   IMPL
#print()
#examine(~(~A >> ~B) >> ~~(~B >> ~A))                      # 14
#print()
examine((A >> (~B >> ~~C)) >> (~(A >> B) >> ~~(A >> C)))  # 15   IMPL
#print()
#examine((A >> ~B) >> (~~A >> ~~~B))                       # DM1  IMPL part a
#print()
#examine((~~A >> ~~~B) >> (A >> ~B))                       # DM1  IMPL part b
#print()
#examine(~(~A >> ~~B) >> ~A)                               # DM2  IMPL part a
#print()
#examine(~(~A >> ~~B) >> ~B)                               # DM2  IMPL part b
#print()
#examine(~A >> (~B >> ~(~A >> ~~B)))                       # DM2  IMPL part c
#print()
#examine((~A >> ~~B) >> (~A >> ~~B))                       # DM1' IMPL
#print()
#examine(~(~~A >> ~~~B) >> A)                              # DM2' IMPL part a
#print()
#examine(~(~~A >> ~~~B) >> B)                              # DM2' IMPL part b
#print()
#examine(A >> (B >> ~(~~A >> ~~~B)))                       # DM2' IMPL part c
#print()
#
#examine((A >> ~~B) >> ~~(A >> B))                         # 17
#print()
#examine(~~(A >> B) >> (A >> ~~B))                         # 17 converse
#print()
#examine(~~(A >> B) >> (~~A >> B))                         # 18
#print()
#examine((~~A >> B) >> ~~(A >> B))                         # 18 converse
#print()