# 离散数学实战：用Python代码验证16个命题定律的真值表（附完整代码） 很多计算机专业的朋友在学习离散数学时，面对那一堆抽象的命题定律和等价式，常常感到头疼。书上列出的16个基本等价式，比如交换律、结合律、德摩根律，虽然逻辑清晰，但总感觉隔着一层纸，不够“实在”。有没有一种方法，能让我们亲手“触摸”到这些逻辑规律，直观地看到它们在任何情况下都恒为真？答案是肯定的，而且工具就在我们手边——Python。 这篇文章就是为你准备的，如果你是一名计算机系学生、编程爱好者，或者任何希望将形式逻辑与计算实践结合起来的探索者。我们将彻底抛弃纯理论的、黑板式的推导，转而打开代码编辑器，用Python构建一个灵活的真值表生成与验证系统。我们的目标不仅仅是“知道”这些定律，而是能够“写出”代码来证明它们，理解重言式替换规则背后的计算本质，并掌握验证公式有效性或可满足性的自动化方法。你会发现，当抽象的`p → q`变成屏幕上可运行的函数，当“等价”转化为两列完全相同的布尔值输出时，离散数学会变得前所未有的清晰和有力。 ## 1. 环境准备与核心思路 在开始敲代码之前，我们首先需要明确我们的“作战计划”。我们的核心任务是：给定一个命题逻辑公式（例如 `p ∧ q`）或两个公式（例如 `p → q` 和 `¬p ∨ q`），程序能够自动生成所有可能的真值指派组合，并计算出公式对应的真值结果，最终以表格形式呈现或进行比对。 ### 1.1 工具选择与安装 我们将使用纯Python的标准库，无需安装任何第三方包，确保环境的纯净和代码的可移植性。主要会用到`itertools`来生成真值指派组合，以及`eval()`函数或自定义解析器来计算表达式。为了更安全、更可控，我们倾向于自己编写表达式求值逻辑。 首先，确保你有一个Python环境（3.6及以上版本均可）。你可以通过以下命令快速检查： ```bash python --version ``` 如果尚未安装，请前往Python官网下载安装。接下来，创建一个新的Python脚本文件，例如 `truth_table_verifier.py`。 ### 1.2 设计我们的真值表引擎 一个健壮的真值表生成器需要几个核心组件： 1. **变量提取器**：从输入的公式字符串中，识别出所有独立的命题变元（如 `p`, `q`, `r`）。 2. **指派生成器**：为所有识别出的变元，生成所有可能的真值（True/False）组合。对于n个变元，将有2ⁿ种组合。 3. **表达式求值器**：对于每一种真值指派，将公式中的变元替换为具体的布尔值，并根据逻辑联结词（¬, ∧, ∨, →, ↔）的规则计算出整个公式的真值。 4. **结果展示器**：将变量、公式和计算结果以清晰易读的格式（如文本表格）输出。 > 注意：直接使用Python的`eval()`函数处理用户输入的字符串存在安全风险。我们将构建一个简单的、安全的递归下降解析器或使用字典替换的方式来求值，这不仅能保证安全，还能加深对表达式树结构的理解。 下面，我们先搭建一个基础框架。 ```python import itertools class TruthTable: def __init__(self, expression_str): self.expr = expression_str self.variables = self._extract_variables() self.truth_combos = list(itertools.product([False, True], repeat=len(self.variables))) self.results = [] def _extract_variables(self): """从表达式中提取所有字母变量（忽略逻辑运算符）""" vars_set = set() for char in self.expr: if char.isalpha() and char.islower(): # 假设变元为小写字母 vars_set.add(char) return sorted(list(vars_set)) # 排序以保证输出顺序一致 def evaluate(self, assignment): """ 核心求值函数。 assignment: 一个字典，如 {'p': True, 'q': False} 返回：公式在此指派下的布尔值。 """ # 这是一个占位符，我们将在下一节实现具体的逻辑 pass def generate(self): """生成完整的真值表""" table = [] for combo in self.truth_combos: # 创建变量名到真值的映射 assignment = dict(zip(self.variables, combo)) result = self.evaluate(assignment) table.append((*combo, result)) self.results = table return table def print_table(self): """以表格形式打印真值表""" header = self.variables + [self.expr] print(" | ".join(header)) print("-" * (len(" | ".join(header)))) for row in self.results: # 将布尔值转换为更直观的T/F row_display = ['T' if val else 'F' for val in row] print(" | ".join(row_display)) ``` 这个框架已经定义了核心结构。`_extract_variables`方法使用简单的规则识别变量。`generate`方法利用`itertools.product`生成所有真值组合，并准备调用求值函数。现在，最关键的挑战在于实现`evaluate`方法。 ## 2. 实现命题逻辑表达式求值器 为了让我们的引擎能够理解 `¬p ∧ (q ∨ r)` 这样的公式，我们需要定义逻辑联结词的语义。在Python中，我们可以用以下方式对应： | 逻辑联结词 | 符号 | Python 运算符 | 说明 | | :--- | :--- | :--- | :--- | | 否定 | ¬ | `not` | 真值取反 | | 合取 | ∧ | `and` | 逻辑与 | | 析取 | ∨ | `or` | 逻辑或 | | 蕴含 | → | `(not p) or q` | p为真且q为假时结果为假 | | 双条件 | ↔ | `p == q` | p和q真值相同时为真 | > 提示：蕴含 `p → q` 的逻辑等价于 `¬p ∨ q`，这是我们即将验证的定律之一。在代码实现中，我们可以直接使用这个等价式来简化计算。 实现求值器有两种主流思路： 1. **字符串替换与安全eval**：将公式中的逻辑符号替换为Python运算符，然后利用创建好的安全环境进行求值。 2. **构建语法树**：将公式解析成一棵抽象语法树（AST），然后递归求值。这种方法更复杂，但更强大、更灵活。 为了平衡安全性与实现的简洁性，我们采用第一种方法的增强版。我们将公式中的逻辑符号转换为Python可理解的函数调用或运算符，但**绝不直接`eval`原始字符串**，而是构建一个求值函数。 ```python def evaluate(self, assignment): """ 通过替换和安全的表达式构建来求值。 """ # 复制一份表达式字符串进行操作 expr_to_eval = self.expr # 第一步：替换变量为它们的布尔值 for var, val in assignment.items(): # 将 'p' 替换为 'True' 或 'False' expr_to_eval = expr_to_eval.replace(var, str(val)) # 第二步：替换逻辑运算符为Python表达式 # 注意替换顺序，避免干扰。例如，先替换双箭头，再替换单箭头，再替换其他。 expr_to_eval = expr_to_eval.replace('↔', '==') expr_to_eval = expr_to_eval.replace('→', '<=') # 使用'<='是因为 (not p) or q 在逻辑上等价于 p <= q (当p为True时，q必须为True) # 但更清晰的做法是显式替换为 `(not {0}) or {1}` 的格式。这里我们采用更直接的函数映射。 # 让我们换一种更稳健的方法：定义运算符函数。 # 实际上，更清晰的做法是定义一个内部函数来逐步计算。 # 我们重写这个evaluate方法，采用递归下降解析。 ``` 鉴于替换法的潜在缺陷（如变量名包含其他字母的子串），我们转向一个更鲁棒的、基于递归下降的简易解析器。我们假设公式使用标准符号且括号完备。 ```python def evaluate_recursive(self, expr, assignment): """递归地解析并求值一个表达式（假设表达式已去除空格）""" expr = expr.strip() # 基础情况：单个变量 if len(expr) == 1 and expr in assignment: return assignment[expr] # 处理括号 if expr[0] == '(' and expr[-1] == ')': # 找到匹配的右括号 count = 0 for i, ch in enumerate(expr): if ch == '(': count += 1 elif ch == ')': count -= 1 if count == 0 and i != len(expr) - 1: break # 括号不是最外层的 if i == len(expr) - 1: # 确实是外层括号，去掉括号递归求值 return self.evaluate_recursive(expr[1:-1], assignment) # 寻找主运算符（优先级最低的） # 优先级： ↔ (最低) → ∧, ∨ ¬ (最高) # 我们从左到右查找优先级最低的运算符 paren_count = 0 # 先找双条件 ↔ for i in range(len(expr)-1, -1, -1): # 从右向左找，实现左结合性 ch = expr[i] if ch == '(': paren_count += 1 elif ch == ')': paren_count -= 1 elif paren_count == 0 and ch == '↔': left_val = self.evaluate_recursive(expr[:i], assignment) right_val = self.evaluate_recursive(expr[i+1:], assignment) return left_val == right_val # 再找蕴含 → paren_count = 0 for i in range(len(expr)-1, -1, -1): ch = expr[i] if ch == '(': paren_count += 1 elif ch == ')': paren_count -= 1 elif paren_count == 0 and ch == '→': left_val = self.evaluate_recursive(expr[:i], assignment) right_val = self.evaluate_recursive(expr[i+1:], assignment) return (not left_val) or right_val # p → q 等价于 ¬p ∨ q # 再找析取 ∨ paren_count = 0 for i in range(len(expr)-1, -1, -1): ch = expr[i] if ch == '(': paren_count += 1 elif ch == ')': paren_count -= 1 elif paren_count == 0 and ch == '∨': left_val = self.evaluate_recursive(expr[:i], assignment) right_val = self.evaluate_recursive(expr[i+1:], assignment) return left_val or right_val # 再找合取 ∧ paren_count = 0 for i in range(len(expr)-1, -1, -1): ch = expr[i] if ch == '(': paren_count += 1 elif ch == ')': paren_count -= 1 elif paren_count == 0 and ch == '∧': left_val = self.evaluate_recursive(expr[:i], assignment) right_val = self.evaluate_recursive(expr[i+1:], assignment) return left_val and right_val # 最后处理否定 ¬ if expr[0] == '¬': val = self.evaluate_recursive(expr[1:], assignment) return not val # 如果以上都没匹配，理论上不应该发生 raise ValueError(f"无法解析表达式: {expr}") def evaluate(self, assignment): """包装递归求值函数，并预处理表达式（如去除空格）""" # 去除所有空格，简化解析 clean_expr = self.expr.replace(' ', '') return self.evaluate_recursive(clean_expr, assignment) ``` 现在，我们的`TruthTable`类拥有了一个能够解析常见命题逻辑公式的求值器。让我们用几个简单例子测试一下核心功能。 ```python if __name__ == "__main__": # 测试1：德摩根律的一部分 ¬(p ∧ q) tt1 = TruthTable("¬(p∧q)") tt1.generate() print("真值表 1: ¬(p ∧ q)") tt1.print_table() print() # 测试2：蕴含等价式 p → q tt2 = TruthTable("p→q") tt2.generate() print("真值表 2: p → q") tt2.print_table() ``` 运行这段代码，你应该能看到两个正确的真值表被打印出来。引擎已经就绪，接下来我们可以用它来验证那些重要的命题定律了。 ## 3. 验证16个基本等价式（命题定律） 现在进入最激动人心的部分：用我们亲手打造的代码，去验证离散数学课本中那16个基石般的等价式。我们不会一次性验证所有，而是挑选几个最具代表性、也最能体现代码价值的定律进行演示。完整的验证代码包可以在文章末尾找到。 首先，我们定义一个辅助函数，用来比较两个公式是否在所有真值指派下等价。 ```python def are_equivalent(expr1, expr2): """判断两个命题公式是否逻辑等价""" tt1 = TruthTable(expr1) tt2 = TruthTable(expr2) # 首先检查变量集是否相同（不考虑顺序） if set(tt1.variables) != set(tt2.variables): # 如果变量不同，可以尝试补充变量，但为了简单，我们先假设公式使用相同变量集 # 更严谨的做法是取变量并集，为缺失变量生成所有组合，但两个公式的变量集通常一致。 print(f"警告：公式变量集不同。{expr1}: {tt1.variables}, {expr2}: {tt2.variables}") # 我们暂时返回False，或实现更复杂的检查 return False tt1.generate() tt2.generate() # 比较每一行的结果 for row1, row2 in zip(tt1.results, tt2.results): if row1[-1] != row2[-1]: # 比较结果列 return False return True ``` 接下来，让我们用代码“证明”几个关键定律。 ### 3.1 结合律、交换律、分配律 这些定律和算术运算律非常相似，是逻辑演算的基础。 - **交换律**： `p ∧ q ≡ q ∧ p`， `p ∨ q ≡ q ∨ p` - **结合律**： `(p ∧ q) ∧ r ≡ p ∧ (q ∧ r)`， `(p ∨ q) ∨ r ≡ p ∨ (q ∨ r)` - **分配律**： `p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)`， `p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)` ```python print("=== 验证交换律、结合律、分配律 ===") laws_to_check = [ ("p∧q", "q∧p", "合取交换律"), ("p∨q", "q∨p", "析取交换律"), ("(p∧q)∧r", "p∧(q∧r)", "合取结合律"), ("(p∨q)∨r", "p∨(q∨r)", "析取结合律"), ("p∧(q∨r)", "(p∧q)∨(p∧r)", "合取对析取的分配律"), ("p∨(q∧r)", "(p∨q)∧(p∨r)", "析取对合取的分配律"), ] for expr1, expr2, name in laws_to_check: if are_equivalent(expr1, expr2): print(f"✅ {name} 成立: {expr1} ≡ {expr2}") else: print(f"❌ {name} 不成立") ``` 运行这段代码，你应该会看到一连串的“✅”，这是你的程序在向你确认这些千百年来被无数逻辑学家认可的规律。 ### 3.2 德摩根律与蕴含等价式 这两个定律在逻辑化简和电路设计中极其重要。 - **德摩根律**： `¬(p ∧ q) ≡ ¬p ∨ ¬q`， `¬(p ∨ q) ≡ ¬p ∧ ¬q` - **蕴含等价式**： `p → q ≡ ¬p ∨ q` ```python print("\n=== 验证德摩根律与蕴含等价式 ===") critical_laws = [ ("¬(p∧q)", "¬p∨¬q", "德摩根律 (合取)"), ("¬(p∨q)", "¬p∧¬q", "德摩根律 (析取)"), ("p→q", "¬p∨q", "蕴含等价式"), ] for expr1, expr2, name in critical_laws: if are_equivalent(expr1, expr2): print(f"✅ {name} 成立: {expr1} ≡ {expr2}") # 可以顺便打印一下真值表对比 print(f" 公式1真值表末尾结果: {[row[-1] for row in TruthTable(expr1).generate()]}") print(f" 公式2真值表末尾结果: {[row[-1] for row in TruthTable(expr2).generate()]}") else: print(f"❌ {name} 不成立") ``` 看到输出结果，你会发现`p→q`和`¬p∨q`的真值序列完全一致，这就是“逻辑等价”在计算上的直观体现。 ### 3.3 幂等律、同一律、零律、矛盾律与排中律 这些定律描述了命题与`True`、`False`常量相互作用的结果，以及命题自身的特性。 - **幂等律**： `p ∧ p ≡ p`， `p ∨ p ≡ p` - **同一律**： `p ∧ True ≡ p`， `p ∨ False ≡ p` - **零律**： `p ∧ False ≡ False`， `p ∨ True ≡ True` - **矛盾律**： `p ∧ ¬p ≡ False` - **排中律**： `p ∨ ¬p ≡ True` 要在代码中验证这些涉及常量(`True`/`False`)的定律，我们需要扩展我们的公式表示法。我们可以在`TruthTable`类中增加对`1`（代表True）和`0`（代表False）的支持，并修改求值器。为了简洁，我们换一种方式：直接通过逻辑推理和Python的布尔运算来验证，因为常量是固定的。但为了保持验证框架的一致性，我们可以将`True`视为一个永真变元，`False`视为一个永假变元。更简单的方法是，我们直接为这些定律编写特定的验证代码。 ```python print("\n=== 验证涉及常量的定律 ===") # 我们手动验证，因为我们的解析器暂不支持直接输入True/False。 # 思路：对于p的所有可能取值（True, False），检查等式是否成立。 import itertools def verify_constant_law(law_name, func1, func2): """func1和func2是接受一个布尔参数p的函数，返回布尔值""" for p in [True, False]: if func1(p) != func2(p): print(f"❌ {law_name} 在 p={p} 时不成立") return print(f"✅ {law_name} 成立") # 定义函数 verify_constant_law( "幂等律 (合取)", lambda p: p and p, lambda p: p ) verify_constant_law( "幂等律 (析取)", lambda p: p or p, lambda p: p ) verify_constant_law( "同一律 (p ∧ True ≡ p)", lambda p: p and True, lambda p: p ) verify_constant_law( "矛盾律 (p ∧ ¬p ≡ False)", lambda p: p and (not p), lambda p: False ) verify_constant_law( "排中律 (p ∨ ¬p ≡ True)", lambda p: p or (not p), lambda p: True ) ``` 通过这种方式，我们绕过了公式解析器对常量的支持，直接使用Python的布尔逻辑完成了验证。这实际上揭示了这些定律的另一个视角：它们就是布尔代数的基本运算性质。 ## 4. 探索重言式、可满足性与替换规则 掌握了等价式的验证，我们可以向更深处探索：重言式（永真式）、矛盾式（永假式）以及可满足式。 ### 4.1 自动检测公式类型 我们可以为`TruthTable`类增加一个方法，来分析生成的真值表属于哪种类型。 ```python def analyze_formula(self): """分析公式类型：重言式、矛盾式或可满足式""" if not self.results: self.generate() results_column = [row[-1] for row in self.results] all_true = all(results_column) all_false = not any(results_column) if all_true: return "Tautology (重言式)" elif all_false: return "Contradiction (矛盾式)" else: return "Satisfiable (可满足式)" ``` 让我们测试几个经典公式： ```python print("\n=== 公式类型分析 ===") test_formulas = [ ("p∨¬p", "排中律"), ("p∧¬p", "矛盾律"), ("p→p", "自蕴含"), ("p→q", "普通蕴含"), ("(p→q)∧p∧¬q", "逻辑推理中的谬误？"), ] for expr, desc in test_formulas: tt = TruthTable(expr) tt.generate() formula_type = tt.analyze_formula() print(f"{desc:20} {expr:15} -> {formula_type}") ``` 运行后，你会看到`p∨¬p`和`p→p`被识别为重言式，`p∧¬p`被识别为矛盾式，而`p→q`是一个可满足式（有时真，有时假）。最后一个`(p→q)∧p∧¬q`，如果你熟悉逻辑，会知道它正是“肯定前件”推理中，如果结论q为假会导致的矛盾式。我们的程序也正确地将其识别为矛盾式。 ### 4.2 实现重言式的替换规则 替换规则是逻辑推导中的强大工具：**如果一个公式是重言式，那么将其中的命题变元统一替换为任意复合命题，得到的新公式仍然是重言式。** 例如，已知 `A ∨ ¬A` 是重言式，将 `A` 替换为 `(p → q)`，则 `(p → q) ∨ ¬(p → q)` 也是重言式。 我们可以用代码模拟这个规则。思路是： 1. 确认原公式是重言式。 2. 定义一个替换映射（例如，`{'A': '(p→q)'}`）。 3. 对原公式字符串进行替换，得到新公式。 4. 验证新公式是否仍是重言式。 这里有一个技术点：我们的`TruthTable`类目前只接受小写字母作为变元。为了支持像`A`这样的“元变元”被替换为复合公式，我们需要一个更通用的替换和验证流程。我们可以构建一个函数，它接受一个重言式模板和一个替换字典，然后生成新公式并验证。 ```python def apply_substitution_rule(template_expr, substitution_map): """ 应用替换规则。 template_expr: 作为模板的重言式，其中包含可被替换的元变元（如'A', 'B'）。 substitution_map: 字典，将元变元映射为新的命题公式字符串。 返回：替换后的新公式字符串，以及它是否是重言式的验证结果。 """ # 进行替换 new_expr = template_expr for meta_var, sub_formula in substitution_map.items(): # 简单的字符串替换，注意避免部分匹配，这里假设元变元是独立的标识符 # 更安全的做法是使用正则表达式匹配单词边界 import re new_expr = re.sub(r'\b' + meta_var + r'\b', '(' + sub_formula + ')', new_expr) # 验证原模板是重言式 (应该由调用者保证，这里我们双重检查) tt_template = TruthTable(template_expr) if tt_template.analyze_formula() != "Tautology (重言式)": print(f"警告：模板 '{template_expr}' 不是重言式。") return new_expr, False # 验证新公式 tt_new = TruthTable(new_expr) is_tautology = tt_new.analyze_formula() == "Tautology (重言式)" return new_expr, is_tautology # 示例：用排中律模板 A ∨ ¬A template = "A∨¬A" sub_map = {'A': 'p→q'} new_formula, is_taut = apply_substitution_rule(template, sub_map) print(f"\n=== 替换规则演示 ===") print(f"模板重言式: {template}") print(f"替换映射: {sub_map}") print(f"生成的新公式: {new_formula}") print(f"新公式是重言式吗？ {is_taut}") # 再试一个复杂点的替换 sub_map2 = {'A': '(p∧q)→r'} new_formula2, is_taut2 = apply_substitution_rule(template, sub_map2) print(f"\n替换映射: {sub_map2}") print(f"生成的新公式: {new_formula2}") print(f"新公式是重言式吗？ {is_taut2}") ``` 这个演示生动地展现了替换规则的威力。无论你把`A`替换成多么复杂的命题公式，只要原式是重言式，替换后的新公式就像被施加了“永真魔法”一样，其真值表最后一列将全部是`True`。 ### 4.3 有效性(valid)与可满足性(satisfiable)的判定方法 在逻辑和计算机科学（特别是可满足性问题SAT）中，区分公式是“有效的”（即重言式）、“可满足的”（至少有一种成真指派）还是“不可满足的”（即矛盾式）至关重要。 我们的`analyze_formula`方法已经可以区分这三者。基于此，我们可以实现一个重要的逻辑关系：**一个公式是有效的（valid），当且仅当它的否定是不可满足的（unsatisfiable）。** 反之亦然。 ```python def is_valid(formula_expr): """通过检查其否定是否不可满足，来判断公式是否有效（重言式）""" tt = TruthTable(formula_expr) if tt.analyze_formula() == "Tautology (重言式)": return True # 方法二：检查其否定是否为矛盾式 negated_formula = "¬(" + formula_expr + ")" if len(formula_expr) > 1 else "¬" + formula_expr tt_neg = TruthTable(negated_formula) return tt_neg.analyze_formula() == "Contradiction (矛盾式)" def is_satisfiable(formula_expr): """判断公式是否可满足（至少有一个成真指派）""" tt = TruthTable(formula_expr) return tt.analyze_formula() != "Contradiction (矛盾式)" # 测试 print("\n=== 有效性与可满足性判定 ===") test_cases = ["p∨¬p", "p∧¬p", "p→q", "(p→q)∧¬q∧p"] for expr in test_cases: valid = is_valid(expr) sat = is_satisfiable(expr) print(f"公式: {expr:20} 有效(Valid)? {valid:5} 可满足(Satisfiable)? {sat:5}") ``` 你会发现，`p∨¬p`有效且可满足（重言式当然是可满足的），`p∧¬p`无效且不可满足，`p→q`无效但可满足。最后一个`(p→q)∧¬q∧p`，它试图描述“如果p则q，并且非q，并且p”的情况，这是一个逻辑矛盾（对应推理中的“否定后件”式），所以它无效且不可满足。 至此，我们已经构建了一个功能相对完整的命题逻辑真值表验证与实验平台。从验证基本等价式，到分析公式类型，再到应用替换规则和判定有效性，我们全部用代码走了一遍。这个过程不仅巩固了对离散数学概念的理解，更获得了一种将形式化理论转化为可执行检验的宝贵能力。 在最后的代码包里，我提供了一个整合所有功能的脚本，包含了文中提到的所有16个基本等价式的自动验证循环，以及一个简单的命令行交互界面，你可以直接输入公式进行探索。编程验证的一个巨大优势是，你可以轻易地测试书上没有的、你自己构想出来的复杂公式，立刻看到它的真值表，观察它是否是一个重言式，或者它和另一个公式是否等价。这种即时反馈的学习体验，是纸笔演算难以比拟的。