手写Python Hilbert prover：演绎定理证明中元层次证明对象的数据结构选型

1. 先锚定元证明的核心逻辑 #

演绎定理的归纳证明本质是将「Γ∪{A}⊢B」的对象层次证明，转换为「Γ⊢A→B」的对象层次证明，归纳过程分三类情况：

• 基例1：原证明步骤是公理或Γ中的前提
• 基例2：原证明步骤是假设A
• 归纳步：原证明步骤由分离规则（MP）推导得出

数据结构的核心需求是：能追踪原证明的每一步依据，同时对应生成元证明转换后的证明片段。

2. 核心数据结构设计 #

2.1 基础对象层次结构（复用你已实现的逻辑，补充必要细节） #

先明确底层公式与证明步骤的表示：

class Formula:
    def __init__(self, formula_type, left=None, right=None, symbol=None):
        self.type = formula_type  # "atom", "implies", "neg"
        self.left = left  # 蕴含式的左子公式
        self.right = right  # 蕴含式/否定的右子公式
        self.symbol = symbol  # 原子公式的符号（如"P", "Q"）
    
    def __eq__(self, other):
        # 实现公式相等判断逻辑，用于匹配公理实例和MP前提
        if not isinstance(other, Formula):
            return False
        if self.type != other.type:
            return False
        if self.type == "atom":
            return self.symbol == other.symbol
        elif self.type == "implies":
            return self.left == other.left and self.right == other.right
        elif self.type == "neg":
            return self.right == other.right
    
    def __repr__(self):
        # 友好的公式打印格式，方便调试
        if self.type == "atom":
            return self.symbol
        elif self.type == "implies":
            return f"({self.left} → {self.right})"
        elif self.type == "neg":
            return f"¬{self.right}"

class ProofStep:
    def __init__(self, formula, justification):
        self.formula = formula  # 当前步骤的Formula实例
        self.justification = justification  # 依据：("axiom", 公理编号) / ("premise", 前提索引) / ("mp", 步骤i, 步骤j)

2.2 元层次证明的递归节点结构 #

用递归类表示元证明的归纳步骤，每个节点对应原证明一步的转换逻辑：

class MetaProofNode:
    def __init__(self, case_type, original_step, children=None):
        self.case_type = case_type  # "base_axiom", "base_premise", "base_hyp_A", "inductive_mp"
        self.original_step = original_step  # 原证明中的ProofStep实例
        self.children = children or []  # 归纳步需要的子元证明节点（MP的两个前提对应节点）
        self.constructed_steps = None  # 存储转换后的Γ⊢A→B的证明片段（ProofStep列表）

    def construct(self, A):
        # 根据不同case生成对应的证明片段
        if self.case_type in ["base_axiom", "base_premise"]:
            # 原公式φ，构造A→φ：用公理1 + MP
            phi = self.original_step.formula
            # 公理1实例：φ→(A→φ)
            axiom1_inst = Formula("implies", phi, Formula("implies", A, phi))
            step1 = ProofStep(axiom1_inst, ("axiom", 1))
            # MP步骤：从φ和φ→(A→φ)得到A→φ
            step2 = ProofStep(Formula("implies", A, phi), ("mp", len(self.constructed_steps)-1, 0))
            self.constructed_steps = [step1, self.original_step, step2]
        
        elif self.case_type == "base_hyp_A":
            # 构造Γ⊢A→A的标准证明（用公理1和公理2推导）
            # 公理1实例：A→((A→A)→A)
            axiom1_inst = Formula("implies", A, Formula("implies", Formula("implies", A, A), A))
            # 公理2实例：(A→((A→A)→A))→((A→(A→A))→(A→A))
            axiom2_inst = Formula("implies",
                Formula("implies", A, Formula("implies", Formula("implies", A, A), A)),
                Formula("implies", Formula("implies", A, Formula("implies", A, A)), Formula("implies", A, A))
            )
            # 公理1实例：A→(A→A)
            axiom1_inst2 = Formula("implies", A, Formula("implies", A, A))
            step1 = ProofStep(axiom1_inst, ("axiom", 1))
            step2 = ProofStep(axiom2_inst, ("axiom", 2))
            step3 = ProofStep(Formula("implies", Formula("implies", A, Formula("implies", A, A)), Formula("implies", A, A)), ("mp", 1, 0))
            step4 = ProofStep(axiom1_inst2, ("axiom", 1))
            step5 = ProofStep(Formula("implies", A, A), ("mp", 3, 2))
            self.constructed_steps = [step1, step2, step3, step4, step5]
        
        elif self.case_type == "inductive_mp":
            # 原步骤由MP从C和C→B得到B，先构造子节点的证明片段
            child_c, child_c_implies_b = self.children
            child_c.construct(A)
            child_c_implies_b.construct(A)
            # 拼接子节点的证明步骤
            combined = child_c.constructed_steps + child_c_implies_b.constructed_steps
            # 公理2实例：(A→(C→B))→((A→C)→(A→B))
            C = child_c.original_step.formula
            B = self.original_step.formula
            axiom2_inst = Formula("implies",
                Formula("implies", A, Formula("implies", C, B)),
                Formula("implies", Formula("implies", A, C), Formula("implies", A, B))
            )
            step_axiom2 = ProofStep(axiom2_inst, ("axiom", 2))
            combined.append(step_axiom2)
            # 第一次MP：从A→(C→B)和公理2得到(A→C)→(A→B)
            mp1_idx = len(child_c.constructed_steps) + len(child_c_implies_b.constructed_steps) - 1
            step_mp1 = ProofStep(Formula("implies", Formula("implies", A, C), Formula("implies", A, B)), ("mp", len(combined)-1, mp1_idx))
            combined.append(step_mp1)
            # 第二次MP：从A→C和(A→C)→(A→B)得到A→B
            mp2_idx = len(child_c.constructed_steps) - 1
            step_mp2 = ProofStep(Formula("implies", A, B), ("mp", len(combined)-1, mp2_idx))
            combined.append(step_mp2)
            self.constructed_steps = combined

3. 整体执行流程 #

1. 输入处理：接收「Γ∪{A}⊢B」的完整证明（ProofStep列表）
2. 生成元证明树：遍历原证明的每一步，为每个ProofStep创建对应的MetaProofNode：
   • 若步骤依据是公理或Γ中的前提：创建case_type="base_axiom"或"base_premise"的节点
   • 若步骤是假设A：创建case_type="base_hyp_A"的节点
   • 若步骤是MP推导：找到对应前提步骤的MetaProofNode作为子节点，创建case_type="inductive_mp"的节点
3. 构造目标证明：对最后一个MetaProofNode调用construct(A)，得到「Γ⊢A→B」的完整ProofStep列表
4. 验证（可选）：遍历构造出的证明，检查每一步的依据是否符合Hilbert系统规则，确保转换正确

4. 调试与优化建议 #

• 给Formula和ProofStep实现清晰的__repr__，方便打印证明步骤排查问题
• 先测试小规模原证明（3-5步），验证元证明的转换逻辑，再扩展到复杂场景
• 可预存常见内定理的证明片段（如A→A），避免重复构造

内容的提问来源于stack exchange，提问作者Jasper