Douglas Hofstadter's "Typographical Number Theory" exercises, in Python.

tnt.py

# -*- coding: utf-8 -*-

import re
from contextlib import contextmanager

assert u'\u2283' == u'⊃'
assert u'\u2227' == u'∧'
assert u'\u2228' == u'∨'
assert u'\u2200' == u'∀'
assert u'\u2203' == u'∃'
assert u'\u22c5' == u'⋅'
assert u'\u2032' == u'′'

def U(s):
    if type(s) is unicode:
        return s
    return s.decode('utf8')

def is_alphabetically_correct(s):
    return set(s) <= set(u'0Sabcdefghijklmnopqrstuwxyz′(+⋅)=~<∧∨⊃>∀∃:')

def is_numeral(s):
    return bool(re.match('S*0$', U(s)))

assert all(is_numeral(x) for x in ['0', 'S0', 'SS0', 'SSS0', 'SSSS0', 'SSSSS0'])

def is_variable(s):
    return bool(re.match(u'[abcdefghijklmnopqrstuwxyz]′*$', U(s)))

assert all(is_variable(x) for x in ['a', 'b′', 'c′′', 'd′′′', 'e′′′′'])

def is_term(s):
    s = U(s)
    while s and s[0] == 'S':
        s = s[1:]
    if not s:
        return False
    if s[0] == '(' and s[-1] == ')':
        for i in range(len(s)):
            if s[i] in u'+⋅' and is_term(s[1:i]) and is_term(s[i+1:-1]):
                return True
    if is_numeral(s) or is_variable(s):
        return True
    return False

def get_free_variables_in_term(s):
    return set(re.findall(u'[abcdefghijklmnopqrstuwxyz]′*?', U(s)))

def is_definite_term(s):
    return is_term(s) and not get_free_variables_in_term(s)

def is_indefinite_term(s):
    return is_term(s) and get_free_variables_in_term(s)

assert all(is_definite_term(x) for x in ['0', '(S0+S0)', 'SS((SS0⋅SS0)+(S0⋅S0))'])
assert all(is_indefinite_term(x) for x in ['b', 'Sa', '(b′+S0)', '(((S0+S0)⋅S0)+e)'])

class FormulaInfo:
    def __init__(self, wf, fv, qv):
        assert type(qv) in [type(set()), type(None)]
        assert type(fv) in [type(set()), type(None)]
        self.is_well_formed = wf
        self.free_variables = fv
        self.quantified_variables = qv
    def __nonzero__(self):
        assert False  # you shouldn't be calling this

def check_atom(s):
    s = U(s)
    for i in range(len(s)):
        if s[i] == '=':
            t1, t2 = s[:i], s[i+1:]
            if is_term(t1) and is_term(t2):
                return FormulaInfo(True, get_free_variables_in_term(t1) | get_free_variables_in_term(t2), set())
    return FormulaInfo(False, None, None)

assert all(check_atom(x).is_well_formed for x in ['S0=0', '(SS0+SS0)=SSSS0', 'S(b+c)=((c⋅d)⋅e)'])

def check_negation(s):
    s = U(s)
    if s and s[0] == '~':
        return check_well_formed_formula(s[1:])
    return FormulaInfo(False, None, None)

def check_compound(s):
    s = U(s)
    if s and s[0] == '<' and s[-1] == '>':
        for i in range(len(s)):
            if s[i] in u'∧∨⊃':
                f1 = check_well_formed_formula(s[1:i])
                f2 = check_well_formed_formula(s[i+1:-1])
                if f1.is_well_formed and f2.is_well_formed:
                    fv = (f1.free_variables | f2.free_variables)
                    qv = (f1.quantified_variables | f2.quantified_variables)
                    if not (fv & qv):
                        return FormulaInfo(True, fv, qv)
                    break
    return FormulaInfo(False, None, None)

def check_quantification(s):
    s = U(s)
    if s and s[0] in u'∀∃':
        colon = s.find(':')
        if colon >= 0:
            v = s[1:colon]
            f = check_well_formed_formula(s[colon+1:])
            if is_variable(v) and f.is_well_formed and (v in f.free_variables):
                return FormulaInfo(True, f.free_variables - set([v]), f.quantified_variables | set([v]))
    return FormulaInfo(False, None, None)

def check_well_formed_formula(s):
    s = U(s)
    for check in [check_atom, check_negation, check_compound, check_quantification]:
        f = check(s)
        if f.is_well_formed:
            return f
    return FormulaInfo(False, None, None)

assert all(check_negation(x).is_well_formed for x in ['~S0=0', '~∃b:(b+b)=S0', '~<0=0⊃S0=0>', '~b=S0', '~∃c:Sc=d'])
assert all(check_compound(x).is_well_formed for x in ['<0=0∧~0=0>', '<b=b∨~∃c:c=b>', '<S0=0⊃∀c:~∃b:(b+b)=c>'])
assert all(check_quantification(x).is_well_formed for x in ['∀b:<b=b∨~∃c:c=b>', '∀c:~∃b:(b+b)=c'])

def is_well_formed_formula(s):
    return check_well_formed_formula(s).is_well_formed

def get_free_variables(s):
    return check_well_formed_formula(s).free_variables

def get_quantified_variables(s):
    return check_well_formed_formula(s).quantified_variables

assert is_well_formed_formula('∀a:a=SSSS0')  # "All natural numbers are equal to 2."
assert is_well_formed_formula('~∃a:(a⋅a)=a')  # "There is no natural number which equals its own square."
assert is_well_formed_formula('∀a:∀b:<~a=b⊃~Sa=Sb>')  # "Different natural numbers have different successors."
assert is_well_formed_formula('<S0=0⊃∀a:~∃b:(b⋅SS0)=a>')  # "If 1 equals 0, then every number is odd."
assert is_well_formed_formula('∀c:<∃d:(c⋅d)=b⊃∃d:(d⋅SS0)=c>')  # "b is a power of 2."
assert is_well_formed_formula('∃a:∃x:∃y:<<∃d:∃e:<x=(d⋅SSy)∧y=Se>∧∃d:∃e:<x=((d⋅S(Sa⋅y))+b)∧(Sa⋅y)=(b+e)>>∧∀k:∀z:<<∃n:(k+Sn)=a∧∃d:∃e:<x=((d⋅S(Sk⋅y))+z)∧(Sk⋅y)=(z+e)>>⊃∃d:∃e:<x=((d⋅S(SSk⋅y))+(SSSSSSSSSS0⋅z))∧S(SSk⋅y)=(S(SSSSSSSSSS0⋅z)+e)>>>')  # "b is a power of 10."

def WF(s):
    assert is_well_formed_formula(s)

class InvalidStep:
    pass

class Derivation:
    def __init__(self, fantasy_setup=None):
        if fantasy_setup is None:
            self.premise = None
            self.theorems = set([
                u'∀a:~Sa=0',
                u'∀a:(a+0)=a',
                u'∀a:∀b:(a+Sb)=S(a+b)',
                u'∀a:(a⋅0)=0',
                u'∀a:∀b:(a⋅Sb)=((a⋅b)+a)',
            ])
            self.conclusion = None
        else:
            self.premise, self.theorems = fantasy_setup
            self.theorems.add(self.premise)
            self.conclusion = self.premise

    def has_been_derived(self, s):
        return s in self.theorems

    def is_valid_by_joining(self, s):
        s = U(s)
        if s[0] == '<' and s[-1] == '>':
            for i in range(len(s)):
                if s[i] == u'∧':
                    first, second = s[1:i], s[i+1:-1]
                    if set([first, second]) <= self.theorems:
                        return True
        return False

    def is_valid_by_separation(self, s):
        s = U(s)
        if not is_well_formed_formula(s):
            return False
        for theorem in self.theorems:
            if theorem[0] == '<' and theorem[-1] == '>':
                if theorem.startswith(u'<%s∧' % s):
                    return True
                if theorem.endswith(u'∧%s>' % s):
                    return True
        return False

    def is_removal_of_double_tilde(self, shorter, longer):
        if len(shorter)+2 == len(longer):
            if sorted(shorter + u'~~') == sorted(longer):
                for i in range(len(shorter)):
                    if longer == shorter[:i] + '~~' + shorter[i:]:
                        return True
        return False

    def is_valid_by_double_tilde(self, s):
        s = U(s)
        if not is_well_formed_formula(s):
            return False

        for theorem in self.theorems:
            if self.is_removal_of_double_tilde(s, theorem) or self.is_removal_of_double_tilde(theorem, s):
                return True
        return False

    def is_valid_by_detachment(self, s):
        s = U(s)
        for theorem in self.theorems:
            implication = u'<%s⊃%s>' % (theorem, s)
            if implication in self.theorems:
                return True  # because of the implication
        return False

    def _is_valid_by_substituting(self, s, a, b):
        s = U(s)
        for xi in range(0, len(s)):
            for xj in range(xi+1, len(s)):
                x = s[xi:xj]
                if is_well_formed_formula(x):
                    for yi in range(0, len(s)):
                        for yj in range(yi+1, len(s)):
                            y = s[yi:yj]
                            if is_well_formed_formula(y):
                                first = a.replace('X', x).replace('Y', y)
                                if len(first) > len(s):
                                    continue
                                second = b.replace('X', x).replace('Y', y)
                                i = s.find(first)
                                while i != -1:
                                    substituted_s = s[:i] + second + s[i+len(first):]
                                    if substituted_s in self.theorems:
                                        return True
                                    i = s.find(first, i+1)
        return False

    def _is_valid_by_interchanging(self, s, a, b):
        return self._is_valid_by_substituting(s, a, b) or self._is_valid_by_substituting(s, b, a)

    def is_valid_by_contrapositive(self, s):
        return self._is_valid_by_interchanging(s, u'<X⊃Y>', u'<~Y⊃~X>')

    def is_valid_by_de_morgans(self, s):
        return self._is_valid_by_interchanging(s, u'<~X∧~Y>', u'~<X∨Y>')

    def is_valid_by_switcheroo(self, s):
        return self._is_valid_by_interchanging(s, u'<X∨Y>', u'<~X⊃Y>')

    def _is_substitution_of_some_term_for_variable(self, u, a, b):
        if a == b:
            return True
        us_in_a = a.count(u)
        length_of_a_without_us = len(a) - (us_in_a * len(u))
        if len(b) < length_of_a_without_us:
            return False
        if (len(b) - length_of_a_without_us) % us_in_a != 0:
            return False
        length_of_replacement = (len(b) - length_of_a_without_us) / us_in_a
        first_u_in_a = a.find(u)
        if not b.startswith(a[:first_u_in_a]):
            return False
        replacement = b[first_u_in_a:first_u_in_a + length_of_replacement]
        if not is_term(replacement):
            return False
        if get_free_variables_in_term(replacement) & get_quantified_variables(a):
            return False
        return (b == a.replace(u, replacement))

    def is_valid_by_specification(self, s):
        s = U(s)
        for theorem in self.theorems:
            if theorem.startswith(u'∀'):
                colon = theorem.find(':')
                if colon >= 0:
                    u, x = theorem[1:colon], theorem[colon+1:]
                    assert is_variable(u)
                    if self._is_substitution_of_some_term_for_variable(u, x, s):
                        return True
        return False

    def is_valid_by_generalization(self, s):
        s = U(s)
        if s.startswith(u'∀'):
            colon = s.find(':')
            if colon >= 0:
                u, x = s[1:colon], s[colon+1:]
                if is_variable(u) and u in get_free_variables(x):
                    if self.premise is not None and u in get_free_variables(self.premise):
                        return False
                    if x in self.theorems:
                        return True
        return False

    def is_valid_by_interchange(self, s):
        s = U(s)
        for theorem in self.theorems:
            if len(theorem) == len(s):
                a = theorem.find(u'∀')
                while a >= 0 and s[:a] == theorem[:a]:
                    if s[a:a+2] == u'~∃':
                        colon = theorem.find(':', a+1)
                        u = theorem[a+1:colon]
                        assert is_variable(u)
                        if theorem[colon+1] == '~':
                            if s == theorem[:a] + u'~∃' + u + ':' + theorem[colon+2:]:
                                return True
                    a = theorem.find(u'∀', a+1)
                ne = theorem.find(u'~∃')
                while ne >= 0 and s[:ne] == theorem[:ne]:
                    if s[ne] == u'∀':
                        colon = theorem.find(':', ne+2)
                        u = theorem[ne+2:colon]
                        assert is_variable(u)
                        if s == theorem[:ne] + u'∀' + u + ':~' + theorem[colon+1:]:
                            return True
                    ne = theorem.find(u'~∃', ne+2)
        return False

    def is_valid_by_existence(self, s):
        s = U(s)
        if s.startswith(u'∃'):
            colon = s.find(':')
            if colon >= 0:
                u, x = s[1:colon], s[colon+1:]
                if is_variable(u) and u in get_free_variables(x):
                    for theorem in self.theorems:
                        if self._is_substitution_of_some_term_for_variable(u, x, theorem):
                            return True
        return False

    def is_valid_by_equality(self, s):
        s = U(s)
        equals = s.find('=')
        if equals > 0:
            first, second = s[:equals], s[equals+1:]
            if is_term(first) and is_term(second):
                symmetrical_s = u'%s=%s' % (second, first)
                if symmetrical_s in self.theorems:
                    return True
            for theorem in self.theorems:
                if theorem.startswith(first + '='):
                    middle = theorem[len(first)+1:]
                    transitive_s = u'%s=%s' % (middle, second)
                    if transitive_s in self.theorems:
                        return True
        return False

    def is_valid_by_successorship(self, s):
        s = U(s)
        equals = s.find('=')
        if equals > 0:
            first, second = s[:equals], s[equals+1:]
            if is_term(first) and is_term(second):
                add_s = u'S%s=S%s' % (first, second)
                if add_s in self.theorems:
                    return True
                if first[0] == 'S' and second[0] == 'S':
                    drop_s = u'%s=%s' % (first[1:], second[1:])
                    if drop_s in self.theorems:
                        return True
        return False

    def is_valid_by_induction(self, s):
        s = U(s)
        if is_well_formed_formula(s) and s[0] == u'∀':
            colon = s.find(':')
            assert colon >= 0
            u, x = s[1:colon], s[colon+1:]
            assert is_variable(u)
            base_case = x.replace(u, '0')
            if base_case in self.theorems:
                inductive_case = u'∀%s:<%s⊃%s>' % (u, x, x.replace(u, 'S' + u))
                if inductive_case in self.theorems:
                    return True
        return False

    def is_valid_new_theorem(self, s):
        s = U(s)
        return (
            (s in self.theorems) or
            self.is_valid_by_joining(s) or
            self.is_valid_by_separation(s) or
            self.is_valid_by_double_tilde(s) or
            self.is_valid_by_detachment(s) or
            self.is_valid_by_contrapositive(s) or
            self.is_valid_by_de_morgans(s) or
            self.is_valid_by_switcheroo(s) or
            self.is_valid_by_specification(s) or
            self.is_valid_by_generalization(s) or
            self.is_valid_by_interchange(s) or
            self.is_valid_by_existence(s) or
            self.is_valid_by_equality(s) or
            self.is_valid_by_successorship(s) or
            self.is_valid_by_induction(s) or
            False
        )

    def step(self, s):
        s = U(s)
        if not self.is_valid_new_theorem(s):
            raise InvalidStep()
        self.theorems.add(s)
        self.conclusion = s

    @contextmanager
    def fantasy(self, premise):
        f = Derivation([U(premise), self.theorems.copy()])
        yield f
        s = u'<%s⊃%s>' % (f.premise, f.conclusion)
        self.theorems.add(s)
        self.conclusion = s

    def print_all_theorems(self):
        for theorem in self.theorems:
            print theorem

# Page 188:
d = Derivation()
with d.fantasy('<p=0⊃~~p=0>') as f:
    f.step('<~~~p=0⊃~p=0>')  # contrapositive
    f.step('<~p=0⊃~p=0>')    # double-tilde
    f.step('<p=0∨~p=0>')     # switcheroo

# Pages 189–190:
d = Derivation()
with d.fantasy('<<p=0⊃q=0>∧<~p=0⊃q=0>>') as f:
    f.step('<p=0⊃q=0>')     # separation
    f.step('<~q=0⊃~p=0>')   # contrapositive
    f.step('<~p=0⊃q=0>')    # separation
    f.step('<~q=0⊃~~p=0>')  # contrapositive
    with f.fantasy('~q=0') as g:  # push again
        g.step('~q=0')            # premise
        g.step('<~q=0⊃~p=0>')     # carry-over of line 4
        g.step('~p=0')            # detachment
        g.step('<~q=0⊃~~p=0>')    # carry-over of line 6
        g.step('~~p=0')           # detachment
        g.step('<~p=0∧~~p=0>')    # joining
        g.step('~<p=0∨~p=0>')     # De Morgan
    f.step('<~q=0⊃~<p=0∨~p=0>>')  # fantasy rule
    f.step('<<p=0∨~p=0>⊃q=0>')  # contrapositive
    with f.fantasy('~p=0') as g:
        pass
    f.step('<~p=0⊃~p=0>')   # fantasy rule
    f.step('<p=0∨~p=0>')    # switcheroo
    f.step('q=0')           # detachment

# Page 196:
d = Derivation()
with d.fantasy('<p=0∧~p=0>') as f:
    f.step('p=0')           # separation
    f.step('~p=0')          # separation
    with f.fantasy('~q=0') as g:
        g.step('p=0')       # carry-over line 3
        g.step('~~p=0')     # double-tilde
    f.step('<~q=0⊃~~p=0>')  # fantasy
    f.step('<~p=0⊃q=0>')    # contrapositive
    f.step('q=0')           # detachment
d.step('<<p=0∧~p=0>⊃q=0>')

# Page 219: 1 plus 1 equals 2.
d = Derivation()
d.step('∀a:∀b:(a+Sb)=S(a+b)')
d.step('∀b:(S0+Sb)=S(S0+b)')
d.step('(S0+S0)=S(S0+0)')
d.step('∀a:(a+0)=a')
d.step('(S0+0)=S0')
d.step('S(S0+0)=SS0')
d.step('(S0+S0)=SS0')

# Page 219: 1 times 1 equals 1.
d = Derivation()
d.step('∀a:∀b:(a⋅Sb)=((a⋅b)+a)')
d.step('∀b:(S0⋅Sb)=((S0⋅b)+S0)')
d.step('(S0⋅S0)=((S0⋅0)+S0)')
d.step('∀a:∀b:(a+Sb)=S(a+b)')
d.step('∀b:((S0⋅0)+Sb)=S((S0⋅0)+b)')
d.step('((S0⋅0)+S0)=S((S0⋅0)+0)')
d.step('∀a:(a+0)=a')
d.step('((S0⋅0)+0)=(S0⋅0)')
d.step('∀a:(a⋅0)=0')  # axiom 4
d.step('(S0⋅0)=0')  # specification
d.step('((S0⋅0)+0)=0')  # transitivity
d.step('S((S0⋅0)+0)=S0')  # add S
d.step('((S0⋅0)+S0)=S0')  # transitivity
d.step('(S0⋅S0)=S0')  # transitivity

# Page 220. Illegal Shortcuts.
d = Derivation()
d.step('∀a:(a+0)=a')  # axiom 2
try:
    d.step('∀a:a=(a+0)')  # symmetry (Wrong!)
    assert False
    d.step('∀a:a=a')  # transitivity
except InvalidStep:
    pass

d = Derivation()
with d.fantasy('a=0') as f:
    try:
        f.step('∀a:a=0')  # generalization (Wrong!)
        assert False
    except InvalidStep:
        pass

d = Derivation()
with d.fantasy('∀a:a=a') as f:
    f.step('Sa=Sa')       # specification
    f.step('∃b:b=Sa')     # existence
    f.step('∀a:∃b:b=Sa')  # generalization
    try:
        f.step('∃b:b=Sb')     # specification (Wrong!)
        assert False
    except InvalidStep:
        pass

# Exercise, page 220: Derive "Different numbers have different successors" as a theorem of TNT.
d = Derivation()
with d.fantasy('Sa=Sb') as f:
    f.step('a=b')
d.step('<Sa=Sb⊃a=b>')
d.step('<~a=b⊃~Sa=Sb>')
d.step('∀b:<~a=b⊃~Sa=Sb>')
d.step('∀a:∀b:<~a=b⊃~Sa=Sb>')

# Page 221: Something Is Missing
assert is_well_formed_formula('∀a:(0+a)=a')
assert is_well_formed_formula('~∀a:(0+a)=a')

# Page 224: Induction
d = Derivation()
d.step('∀a:∀b:(a+Sb)=S(a+b)')     # axiom 3
d.step('∀b:(0+Sb)=S(0+b)')        # specification
d.step('(0+Sb)=S(0+b)')           # specification
with d.fantasy('(0+b)=b') as f:
    f.step('S(0+b)=Sb')           # add S
    f.step('(0+Sb)=S(0+b)')       # carry over line 3
    f.step('(0+Sb)=Sb')           # transitivity
d.step('<(0+b)=b⊃(0+Sb)=Sb>')     # fantasy rule
d.step('∀b:<(0+b)=b⊃(0+Sb)=Sb>')  # generalization
d.step('(0+0)=0')                 # specialization of axiom 2
d.step('∀b:(0+b)=b')              # induction
d.step('(0+a)=a')                 # specialization
d.step('∀a:(0+a)=a')              # generalization