У меня возникли проблемы с доказательством утверждения, в котором говорится, что 3 — натуральное число.
Аксиома 2.1 утверждает, что 0 — натуральное число, а аксиома 2.2 утверждает, что последователи натуральных чисел являются натуральными.
Что я делаю хочу — это способ объединить теоремы путем подстановки в цепочку, так что я могу получать результаты на основе этих цепочек, не назначая уникальную строку для каждого отдельного шага.
Я думал о том, чтобы сделать мой пример более минимальным, не включая следующие три аксиомы (их 5), но я подумал, что если бы я это сделал, то был бы упущен важный контекст. Это также дает мне возможность получать отзывы о моем коде.
В настоящее время функция modus_ponens работает только для одношаговых теорем, а не для многошаговых.
Я искренне надеюсь, что смогу добиться этого в рамках моей текущей архитектуры. Я не пытаюсь копировать бережливое производство и т. д., а скорее пытаюсь синтезировать собственное понимание основ математики.
"""
The goal of this file is to emulate the framework described in
Terrence Tao's Analysis 1, 3rd edition. The book is freely available
on the internet.
Specifically, instead of using Lean, I wanted to do it from scratch
so I could learn about foundational math.
Goal of the question:
I want to implement a substitution method on theorems
that allows me to string them together in proofs, without
needing to assign a unique label to each step
"""
class ZeroNumber:
"""
This is the symbol 0.
"""
def __repr__(self):
return "0"
def __eq__(self, other):
return isinstance(other, ZeroNumber)
def __hash__(self):
return hash((ZeroNumber))
def substitute(self, substitution, var_name):
return self
class NaturalNumbers:
"""
This is the symbol ℕ.
"""
def __repr__(self):
return "ℕ"
class IncrementOperation:
"""
This is the symbol S()
"""
def __init__(self, operand):
self.operand = operand
def __repr__(self):
return f"S({self.operand})"
def __eq__(self, other):
if not isinstance(other, IncrementOperation):
return False
return self.operand == other.operand
def __hash__(self):
return hash((IncrementOperation, self.operand))
def substitute(self, substitution, var_name):
return IncrementOperation(self.operand.substitute(substitution, var_name))
class SymbolicVariable:
"""
A variable letter. No value.
Values are imposed by propositions.
"""
def __init__(self, name):
self.name = name
def __repr__(self):
return self.name
def __eq__(self, other):
if not isinstance(other, SymbolicVariable):
return False
return self.name == other.name
def __hash__(self):
return hash((SymbolicVariable, self.name))
def substitute(self, substitution, var_name):
if self.name == var_name:
return substitution
return self
class Proposition:
pass
class Predicate(Proposition):
def __init__(self, operand):
self.operand = operand
def __repr__(self):
return f"P({self.operand})"
def __eq__(self, other):
if not isinstance(other, Predicate):
return False
return self.operand == other.operand
def __hash__(self):
return hash((Predicate, self.operand))
def substitute(self, substitution, var_name):
return Predicate(self.operand.substitute(substitution, var_name))
class Contains(Proposition):
"""
The statement x∈S.
x is an element of the set S.
"""
def __init__(self, element, SET):
self.element = element
self.set = SET
def __repr__(self):
return "(" + str(self.element) + "∈" + str(self.set) + ")"
def __eq__(self, other):
if not isinstance(other, Contains):
return False
return self.element == other.element and self.set == other.set
def __hash__(self):
return hash((Contains, self.element, self.set))
def substitute(self, substitution, var_name):
return Contains(self.element.substitute(substitution, var_name), self.set)
class Implication(Proposition):
"""
The statement x→y.
x implicates y.
"""
def __init__(self, antecedent, consequent):
self.antecedent = antecedent
self.consequent = consequent
def __repr__(self):
return "(" + str(self.antecedent) + "→" + str(self.consequent) + ")"
def __eq__(self, other):
if not isinstance(other, Implication):
return False
return self.antecedent == other.antecedent and self.consequent == other.consequent
def __hash__(self):
return hash((Implication, self.antecedent, self.consequent))
def substitute(self, substitution, var_name):
return Implication(
self.antecedent.substitute(substitution, var_name),
self.consequent.substitute(substitution, var_name)
)
class UnEqual(Proposition):
"""
The statement a≠b
a is unequal to b.
"""
def __init__(self, left, right):
self.left = left
self.right = right
def __repr__(self):
return "(" + str(self.left) + "≠" + str(self.right) + ")"
def __eq__(self, other):
if not isinstance(other, UnEqual):
return False
return self.left == other.left and self.right == other.right
def __hash__(self):
return hash((UnEqual, self.left, self.right))
def substitute(self, substitution, var_name):
return UnEqual(
self.left.substitute(substitution, var_name),
self.right.substitute(substitution, var_name)
)
class LogicalAnd(Proposition):
"""
The statement A∧B.
True is both are true else false
"""
def __init__(self, left, right):
self.left = left
self.right = right
def __repr__(self):
return f"({self.left} ∧ {self.right})"
def __eq__(self, other):
if not isinstance(other, LogicalAnd):
return False
return self.left == other.left and self.right == other.right
def __hash__(self):
return hash((LogicalAnd, self.left, self.right))
def substitute(self, substitution, var_name):
return LogicalAnd(
self.left.substitute(substitution, var_name),
self.right.substitute(substitution, var_name)
)
class Theorem:
def __init__(self, proposition, name, dependencies, assumptions):
assert isinstance(proposition, Proposition)
assert isinstance(name, str)
assert isinstance(dependencies, list)
self.proposition = proposition
self.name = name
self.dependencies = dependencies
self.assumptions = frozenset(assumptions) if assumptions is not None else frozenset()
def __repr__(self):
return "\nTheorem " + self.name + ": " + str(self.proposition) \
+ "; " + str(self.dependencies) + "; " + str(self.assumptions)
def axiom(proposition, name):
return Theorem(proposition, name, [], None)
def modus_ponens(implication_theorem, hypothesis_theorem, name):
"""
Rule: From P → Q and P, derive Q
"""
assert isinstance(implication_theorem.proposition, Implication)
assert isinstance(hypothesis_theorem.proposition, Proposition)
assert implication_theorem.proposition.antecedent == hypothesis_theorem.proposition
return Theorem(
implication_theorem.proposition.consequent,
name,
[implication_theorem, hypothesis_theorem],
None
)
# 0 is a natural number.
AXIOM_2_1 = axiom(
Contains(ZeroNumber(), NaturalNumbers()),
"AXIOM_2_1"
)
# successors of naturals are naturals
AXIOM_2_2 = axiom(
Implication(
Contains(SymbolicVariable("n"), NaturalNumbers()),
Contains(IncrementOperation(SymbolicVariable("n")), NaturalNumbers())
),
"AXIOM_2_2"
)
# 3 is a natural number.
# PROPOSITION_2_1_4 = modus_ponens(...)
# should return something like
# Theorem(
# Contains(
# IncrementOperation(
# IncrementOperation(
# IncrementOperation(
# ZeroNumber()
# )
# )
# ),
# NaturalNumbers()
# ),
# "PROPOSITION_2_1_4",
# [AXIOM_2_1, AXIOM_2_2],
# None
# )
# 0 is not the successor of any natural number
AXIOM_2_3 = axiom(
Implication(
Contains(SymbolicVariable("n"), NaturalNumbers()),
UnEqual(IncrementOperation(SymbolicVariable("n")), ZeroNumber())
),
"AXIOM_2_3"
)
# different natural numbers have different successors
AXIOM_2_4 = axiom(
Implication(
LogicalAnd(
Contains(SymbolicVariable("n"), NaturalNumbers()),
Contains(SymbolicVariable("m"), NaturalNumbers())
),
Implication(
UnEqual(
SymbolicVariable("n"),
SymbolicVariable("m")
),
UnEqual(
IncrementOperation(SymbolicVariable("n")),
IncrementOperation(SymbolicVariable("m"))
)
)
),
"AXIOM_2_4"
)
# Principle of mathematical induction
# P(0) ∧ (∀n∈ℕ
(n) → P(S(n))) → ∀n∈ℕ:P(n)AXIOM_2_5 = axiom(
Implication(
LogicalAnd(
Predicate(ZeroNumber()),
LogicalAnd(
Contains(SymbolicVariable("n"), NaturalNumbers()),
Implication(
Predicate(SymbolicVariable("n")),
Predicate(IncrementOperation(SymbolicVariable("n")))
)
)
),
Predicate(SymbolicVariable("n"))
),
"AXIOM_2_5"
)
def main():
print(str(AXIOM_2_1))
print(str(AXIOM_2_2))
# print(str(PROPOSITION_2_1_4))
print(str(AXIOM_2_3))
print(str(AXIOM_2_4))
print(str(AXIOM_2_5))
if __name__ == "__main__":
main()
