Last active
April 8, 2019 21:07
-
-
Save Quuxplusone/6730d0e6b1d31f10c2832b0999ab6d2d to your computer and use it in GitHub Desktop.
Douglas Hofstadter's "Typographical Number Theory" exercises, in Python.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# -*- 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment