Proving the deduction theorem by induction, inside a Hilbert system with custom axioms. In particular, where the induction recurses over those custom axioms.
Introduction:
Note: This question is a more detailed elaboration to this older post on SO: https://stackoverflow.com/q/79947597/32395400.
Hello, I am reading Introduction to Mathematical Logic, 4th edition by Elliott Mendelson. Chapter 1, section 4.
I am striving to prove the deduction theorem by induction in my Hilbert system (written in python), but have been incapable of achieving this goal thus far.
I am having a few troubles in particular; specifically with representing sets where the number of elements is unknown (I will explain below), and representing proofs where the number of steps is unknown (again, this will make sense after I share the target proof).
The target proof:
"Let C1, ..., Cn be a proof of C from Γ ∪ B, where Cn is C. We will prove by induction on j that Γ ⊢ (B → Cj) for 1 ≤ j ≤ n. C1 must be either in Γ or an axiom of our system, or B itself. By axiom 1, C1 → (B → C1) is an axiom. Hence, in the first two cases, by MP, Γ ⊢ B → C1. For the third case, when C1 is B, we have ⊢ B → C1 by lemma 1.8, and therefore, Γ ⊢ B → C1. This takes care of the base case (j=1). Assume now that Γ ⊢ B → Ck for all k < j. Either Cj is an axiom, or Cj is in Γ, or Cj is B, or, Cj follows by modus ponens from some Cl and Cm, where l < j, m < j, and Cm has the form Cl → Cj. In the first three cases, Γ ⊢ B → Cj just as in the base case. In the last case, we have by inductive hypothesis that Γ ⊢ B → Cl and Γ ⊢ B → (Cl → Cj). But, by axiom 2, ⊢ (B → (Cl → Cj)) → ((B → Cl) → (B → Cj)). Hence, by MP, Γ ⊢ (B → Cl) → (B → Cj), and, again by MP, Γ ⊢ B → Cj. Thus, the proof by induction is complete." --- An almost verbatim copy of Mendelson.
Research:
I have seen the post https://proofassistants.stackexchange.com/a/4378/7947, but Coq does it in a way that is not consistent with the book I am reading. Just one example would be the use of quantifiers, which Mendelson does not introduce until later.
I would really much prefer a simpler-without sacrificing correctness!-solution that I could implement in my system without elaborate coding. Currently my code is less that 300 lines, and I would like to keep it short and powerful, and not have ad hoc code for everything.
The problems:
In a typical induction proof, we would prove the base case, then assume the inductive hypothesis and prove that the next step follows from that. I could do that in a CAS-like software, but I haven't been able to map those skills onto my Hilbert system. This is partly because they use different data structures.
My Hilbert system currently works for logical statements (a logical statement is a set of assumptions and a well formed statement which follows from them) with assumption sets that are finite and have known elements. The target proof however depends on a set whose elements are unknown, other than that they have the collective property of contributing to the proof's validity. It would therefore be wrong to have discrete elements in this set, and instead we must work with them abstractly.
Similarly, the Γ ∪ B → C proof has an unknown number of steps. It has at least one (the conclusion), but we don't know how many there are before that, so enummerating steps would feel wrong here. Instead we must work with them abstractly too. There might be one; there might be five; heck, there could be five hundred. That's why we should avoid using known elements, besides possibly the conclusion which at least we know exists. NOTE: The conclusion is an abstract conclusion here, not a typical (known) wfs. It could be substituted with any (known) wfs in this setup, so it would be bad to treatit as an individual wfs because it is meant to speak of them generally.
The final problem I see is how to account for the properties the step(s) of the "proof", without knowing what they are. This is especially complicated, because these properties would depend on axioms and theorems already present in the Hilbert system (which the user declares). This is worthy of more attention actually, so let me explain please.
What the solution would need to do:
It would need to prove the deduction theorem by induction, so that
it can be used later on without repeating the logic. Deduction
can be carried out recursively, and that is not the goal. We will
prove it recursively, but when we actually apply it, it should just
take an assumption and make it the antecedent of an implication.
The proof should be reproducible for other types of similar induction proofs too, even though I am not aware of any currently.
The current system:
from dataclasses import dataclass, field
from tabulate import tabulate
import textwrap
# see https://stackoverflow.com/a/79946254
@dataclass(frozen=True)
class Wfs:
def subs(self, mapping: dict["StatLett", "Wfs"]) -> "Wfs":
raise NotImplementedError
@dataclass(frozen=True)
class Symb(Wfs): pass
@dataclass(frozen=True)
class PrimConn(Symb): pass
@dataclass(frozen=True)
class Not(PrimConn):
arg: Wfs
def __repr__(self):
return f"¬({self.arg})"
def subs(self, mapping: dict[StatLett, Wfs]) -> Wfs:
return Not(self.arg.subs(mapping))
@dataclass(frozen=True)
class To(PrimConn):
arg1: Wfs
arg2: Wfs
def __repr__(self):
return f"({self.arg1} → {self.arg2})"
def subs(self, mapping: dict[StatLett, Wfs]) -> Wfs:
return To(self.arg1.subs(mapping), self.arg2.subs(mapping))
@dataclass(frozen=True)
class StatLett(Symb):
name: str
def __repr__(self):
return self.name
def subs(self, mapping: dict[StatLett, Wfs]) -> Wfs:
return mapping.get(self, self)
@dataclass(frozen=True)
class FiniteSet:
# see page 5 explanation
elements: list[Wfs]
def __contains__(self, other):
flag = False
for element in self.elements:
if element == other:
flag = True
break
return flag
def issubset(self, other):
assert isinstance(other, FiniteSet)
for element in self.elements:
if element not in other.elements:
return False
return True
def __eq__(self, other):
if not isinstance(other, FiniteSet):
return False
return self.issubset(other) and other.issubset(self)
def ispropersubset(self, other):
return self.issubset(other) and not self == other
def union(self, other):
assert isinstance(other, FiniteSet)
new_set = [element for element in self.elements]
for element in other.elements:
if element not in self:
new_set.append(element)
return FiniteSet(new_set)
def intersect(self, other):
assert isinstance(other, FiniteSet)
new_set = []
for element in self.elements:
if element in other:
new_set.append(element)
return FiniteSet(new_set)
def __sub__(self, other):
# in self, but not in other
assert isinstance(other, FiniteSet)
new_set = []
for element in self.elements:
if element not in other.elements:
new_set.append(element)
return FiniteSet(new_set)
def __repr__(self):
return ", ".join(repr(i) for i in self.elements)
@dataclass(frozen=True)
class LogiStat:
assu: FiniteSet
conc: Wfs
vdash: bool
def __repr__(self):
elems = self.assu.elements
lengt = len(elems)
if lengt == 0 and self.vdash == False:
return f"{self.conc}"
elif lengt == 0 and self.vdash == True:
return f"⊢ {self.conc}"
elif lengt > 0 and self.vdash == True:
return f"{self.assu} ⊢ {self.conc}"
def subs(self, mapping: dict[StatLett, Wfs]) -> LogiStat:
return LogiStat(
FiniteSet([i.subs(mapping) for i in self.assu.elements]),
self.conc.subs(mapping),
True
)
@dataclass
class ProofTable:
table: list[str] = field(
default_factory=lambda: [
[
"Line",
"Reasoning",
"Logic",
"Label"
]
]
)
def __repr__(self):
width = 25 # max line width per cell
wrapped_table = [
[textwrap.fill(str(cell), width=width) for cell in row]
for row in self.table
]
return tabulate(
wrapped_table,
headers="firstrow",
tablefmt="plain"
)
def axiom(self, stat: Wfs):
self.table.append(
[
len(self.table),
"Axiom",
LogiStat(
FiniteSet([]),
stat,
False
),
""
]
)
def index(self, location: int | str):
if isinstance(location, int):
return len(self.table) - location
for i, row in enumerate(self.table):
if row[3] == location:
return i
raise ValueError(f"Label '{location}' not found")
def label(self, label: str):
self.table[len(self.table) - 1][3] = label
def subs(self, prev: int | str, mapping: dict[StatLett, Wfs]) -> Wfs:
idx = self.index(prev)
old_logic = self.table[idx][2]
new_logic = old_logic.subs(mapping)
self.table.append(
[
len(self.table),
f"Subs({prev}, {mapping})",
new_logic,
""
]
)
def MP(self, line1: int | str, line2: int | str):
i1 = self.index(line1)
i2 = self.index(line2)
l1 = self.table[i1][2]
l2 = self.table[i2][2]
c1 = l1.conc
c2 = l2.conc
assert isinstance(c1, Wfs) and isinstance(c2, To)
assert c1 == c2.arg1
self.table.append(
[
len(self.table),
f"MP({line1}, {line2})",
LogiStat(
l1.assu.union(l2.assu),
c2.arg2,
True
),
""
]
)
def hypothesis(self, stat: Wfs):
self.table.append(
[
len(self.table),
"Hypothesis",
LogiStat(FiniteSet([stat]), stat, True),
""
]
)
def cut(self, assu_line, proved_line):
i1 = self.index(assu_line)
i2 = self.index(proved_line)
proved = self.table[i2][2].conc
assus = self.table[i1][2].assu
assert proved in assus
new_assus = (assus - FiniteSet([proved])).union(self.table[i2][2].assu)
self.table.append(
[
len(self.table),
f"Cut({assu_line}, {proved_line})",
LogiStat(new_assus, self.table[i1][2].conc, True),
""
]
)
def main():
p = ProofTable()
b = StatLett("B")
c = StatLett("C")
d = StatLett("D")
p.axiom(To(b, To(c, b)))
p.label("Axiom (A1)")
p.axiom(To(
To(b, To(c, d)),
To(To(b, c), To(b, d))
))
p.label("Axiom (A2)")
p.axiom(To(
To(Not(c), Not(b)),
To(To(Not(c), b), c)
))
p.label("Axiom (A3)")
p.subs("Axiom (A2)", {c: To(b, b), d: b})
p.subs("Axiom (A1)", {c: To(b, b)})
p.MP(1, 2)
p.subs("Axiom (A1)", {c: b})
p.MP(1, 2)
p.label("Lemma 1.8")
p.subs("Lemma 1.8", {b: Not(b)})
p.subs("Axiom (A3)", {c: b})
p.MP(2, 1)
p.label("Ex 1.47 (a)")
p.subs("Axiom (A1)", {b: To(c, d), c: b})
p.hypothesis(To(c, d))
p.MP(1, 2)
p.MP(1, "Axiom (A2)")
p.hypothesis(To(b, c))
p.MP(1, 2)
p.label("Ex 1.47 (b)")
p.hypothesis(To(b, To(c, d)))
p.MP(1, "Axiom (A2)")
p.subs("Axiom (A1)", {b: c, c: b})
p.subs("Ex 1.47 (b)", {b: c, c: To(b, c), d: To(b, d)})
p.cut(1, 2)
p.cut(1, 4)
p.label("Ex 1.47 (c)")
p.subs("Ex 1.47 (c)", {b: To(Not(c), Not(b)), c: To(Not(c), b), d: c})
p.cut(1, "Axiom (A3)")
p.subs("Axiom (A1)", {c: Not(c)})
p.subs("Ex 1.47 (b)", {c: To(Not(c), b), d: To(To(Not(c), Not(b)), c)})
p.cut(1, 3)
p.cut(1, 3)
p.subs("Ex 1.47 (c)", {c: To(Not(c), Not(b)), d: c})
p.cut(1, 2)
p.label("Ex 1.47 (d)")
print(p)
if __name__ == "__main__":
main()
The output
Line Reasoning Logic Label
1 Axiom (B → (C → B)) Axiom (A1)
2 Axiom ((B → (C → D)) → ((B → C) Axiom (A2)
→ (B → D)))
3 Axiom ((¬(C) → ¬(B)) → ((¬(C) → Axiom (A3)
B) → C))
4 Subs(Axiom (A2), {C: (B → ⊢ ((B → ((B → B) → B)) →
B), D: B}) ((B → (B → B)) → (B →
B)))
5 Subs(Axiom (A1), {C: (B → ⊢ (B → ((B → B) → B))
B)})
6 MP(1, 2) ⊢ ((B → (B → B)) → (B →
B))
7 Subs(Axiom (A1), {C: B}) ⊢ (B → (B → B))
8 MP(1, 2) ⊢ (B → B) Lemma 1.8
9 Subs(Lemma 1.8, {B: ⊢ (¬(B) → ¬(B))
¬(B)})
10 Subs(Axiom (A3), {C: B}) ⊢ ((¬(B) → ¬(B)) → ((¬(B)
→ B) → B))
11 MP(2, 1) ⊢ ((¬(B) → B) → B) Ex 1.47 (a)
12 Subs(Axiom (A1), {B: (C → ⊢ ((C → D) → (B → (C →
D), C: B}) D)))
13 Hypothesis (C → D) ⊢ (C → D)
14 MP(1, 2) (C → D) ⊢ (B → (C → D))
15 MP(1, Axiom (A2)) (C → D) ⊢ ((B → C) → (B →
D))
16 Hypothesis (B → C) ⊢ (B → C)
17 MP(1, 2) (B → C), (C → D) ⊢ (B → Ex 1.47 (b)
D)
18 Hypothesis (B → (C → D)) ⊢ (B → (C →
D))
19 MP(1, Axiom (A2)) (B → (C → D)) ⊢ ((B → C)
→ (B → D))
20 Subs(Axiom (A1), {B: C, ⊢ (C → (B → C))
C: B})
21 Subs(Ex 1.47 (b), {B: C, (C → (B → C)), ((B → C) →
C: (B → C), D: (B → D)}) (B → D)) ⊢ (C → (B → D))
22 Cut(1, 2) ((B → C) → (B → D)) ⊢ (C
→ (B → D))
23 Cut(1, 4) (B → (C → D)) ⊢ (C → (B → Ex 1.47 (c)
D))
24 Subs(Ex 1.47 (c), {B: ((¬(C) → ¬(B)) → ((¬(C) →
(¬(C) → ¬(B)), C: (¬(C) → B) → C)) ⊢ ((¬(C) → B) →
B), D: C}) ((¬(C) → ¬(B)) → C))
25 Cut(1, Axiom (A3)) ⊢ ((¬(C) → B) → ((¬(C) →
¬(B)) → C))
26 Subs(Axiom (A1), {C: ⊢ (B → (¬(C) → B))
¬(C)})
27 Subs(Ex 1.47 (b), {C: (B → (¬(C) → B)), ((¬(C)
(¬(C) → B), D: ((¬(C) → → B) → ((¬(C) → ¬(B)) →
¬(B)) → C)}) C)) ⊢ (B → ((¬(C) → ¬(B))
→ C))
28 Cut(1, 3) (B → (¬(C) → B)) ⊢ (B →
((¬(C) → ¬(B)) → C))
29 Cut(1, 3) ⊢ (B → ((¬(C) → ¬(B)) →
C))
30 Subs(Ex 1.47 (c), {C: (B → ((¬(C) → ¬(B)) → C))
(¬(C) → ¬(B)), D: C}) ⊢ ((¬(C) → ¬(B)) → (B →
C))
31 Cut(1, 2) ⊢ ((¬(C) → ¬(B)) → (B → Ex 1.47 (d)
C))
Why I didn't attempt a solution for you:
I have attempted solutions to this on my own, but they are all insufficient, and I believe that they would do more to distract from the goal than to help achieve it.