用Python代码玩转离散数学：命题逻辑的编程实践指南

离散数学中命题逻辑的概念常常让初学者感到抽象难懂。那些看似简单的命题、联结词和真值表，在实际应用中却可能让人摸不着头脑。但如果你是一名程序员，特别是Python开发者，其实可以用代码将这些抽象概念具象化——不仅能加深理解，还能让逻辑验证变得自动化。

1. 命题逻辑基础与Python表示

命题逻辑的核心是能够判断真假的陈述句。在Python中，我们可以用布尔值 True 和 False 直接表示命题的真值。让我们从最基本的逻辑联结词开始：

# 基本命题表示
p = True
q = False

# 逻辑联结词实现
not_p = not p          # 否定 ¬p
p_and_q = p and q      # 合取 p∧q
p_or_q = p or q        # 析取 p∨q
p_implies_q = not p or q  # 蕴含 p→q
p_iff_q = p_implies_q and (not q or p)  # 双条件 p↔q

四种基本命题在编程中的表达特别有趣。原命题"若p则q"可以直接用 p_implies_q 表示，而它的逆否命题"若非q则非p"则对应着 (not q) implies (not p) ——这两者在逻辑上是等价的：

# 验证逆否命题等价性
original = (not p) or q
contrapositive = (not (not q)) or (not p)  # 简化为 q or not p
print(original == contrapositive)  # 输出True，证明二者等价

真值表 是理解命题逻辑的重要工具。我们可以编写一个通用函数来生成任意命题表达式的真值表：

def print_truth_table(expr_func, variables):
    from itertools import product
    
    # 打印表头
    header = variables + ['Result']
    print(' | '.join(header))
    print('-' * (4 * len(header) - 1))
    
    # 遍历所有可能的真值组合
    for values in product([False, True], repeat=len(variables)):
        env = dict(zip(variables, values))
        result = expr_func(**env)
        row = ['T' if v else 'F' for v in values] + ['T' if result else 'F']
        print(' | '.join(row))

使用这个函数，我们可以轻松验证德摩根律等逻辑等价式：

# 验证德摩根律：¬(p∧q) ⇔ ¬p∨¬q
def demorgan_left(p, q):
    return not (p and q)

def demorgan_right(p, q):
    return (not p) or (not q)

print("德摩根律第一式真值表：")
print_truth_table(demorgan_left, ['p', 'q'])
print("\n德摩根律第二式真值表：")
print_truth_table(demorgan_right, ['p', 'q'])

2. 自动化真值表与逻辑验证

虽然我们实现了基础的真值表生成函数，但对于更复杂的逻辑表达式，使用SymPy库会更加高效。SymPy是一个符号计算Python库，内置了命题逻辑模块：

from sympy import symbols, And, Or, Not, Implies, Equivalent, truth_table

# 定义命题变量
p, q = symbols('p q')

# 构建逻辑表达式
expr = Implies(p, q)  # p→q

# 生成真值表
print("p→q的真值表：")
for valuation in truth_table(expr, [p, q]):
    print(valuation)

SymPy不仅能生成真值表，还能验证两个逻辑表达式是否等价：

from sympy.logic.boolalg import is_lattice_equal

# 验证分配律：p∨(q∧r) ⇔ (p∨q)∧(p∨r)
q, r = symbols('q r')
left_expr = Or(p, And(q, r))
right_expr = And(Or(p, q), Or(p, r))

print(f"分配律是否成立：{is_lattice_equal(left_expr, right_expr)}")  # 输出True

对于逻辑推理，我们可以实现一个简单的自然演绎系统。以下是一个检查前提是否能推出结论的函数：

def check_inference(premises, conclusion):
    # 将所有前提合取起来，然后蕴含结论
    combined_premises = premises[0]
    for premise in premises[1:]:
        combined_premises = And(combined_premises, premise)
    
    # 检查 (premise1 ∧ premise2 ∧ ...) → conclusion 是否为永真式
    return is_lattice_equal(Implies(combined_premises, conclusion), True)

# 示例：验证从p→q和p能否推出q
premises = [Implies(p, q), p]
conclusion = q
print(f"推理是否有效：{check_inference(premises, conclusion)}")  # 输出True

3. 范式转换与逻辑简化

范式（Normal Form）是命题逻辑中的重要概念，特别是主析取范式(PDNF)和主合取范式(PCNF)。我们可以用SymPy来自动化这些转换：

from sympy.logic.boolalg import to_cnf, to_dnf, simplify_logic

# 示例表达式：(p→q)∧(q→r)
expr = And(Implies(p, q), Implies(q, r))

# 转换为合取范式(CNF)
cnf_expr = to_cnf(expr)
print(f"合取范式：{cnf_expr}")

# 转换为析取范式(DNF)
dnf_expr = to_dnf(expr)
print(f"析取范式：{dnf_expr}")

# 逻辑简化
simplified = simplify_logic(expr)
print(f"简化形式：{simplified}")

理解极小项和极大项是掌握主范式的关键。我们可以编写函数来生成所有可能的极小项：

def generate_minterms(variables):
    from itertools import product
    
    minterms = []
    for values in product([0, 1], repeat=len(variables)):
        terms = []
        for var, val in zip(variables, values):
            terms.append(var if val else Not(var))
        minterms.append(And(*terms))
    return minterms

# 生成两个变量的所有极小项
minterms = generate_minterms([p, q])
for i, minterm in enumerate(minterms):
    print(f"极小项{i+1}: {minterm}")

基于真值表自动生成主范式是理解逻辑结构的有力工具。下面是一个实现这一功能的函数：

def get_canonical_forms(expr, variables):
    from sympy.logic import POSform, SOPform
    
    # 获取主析取范式(最小项之和)
    minterms = []
    for valuation in truth_table(expr, variables):
        if valuation[-1]:  # 如果表达式为真
            minterms.append(valuation[:-1])
    
    # 获取主合取范式(最大项之积)
    maxterms = []
    for valuation in truth_table(expr, variables):
        if not valuation[-1]:  # 如果表达式为假
            maxterms.append(valuation[:-1])
    
    # 使用SymPy的内置函数生成规范形式
    sop_form = SOPform(variables, minterms)
    pos_form = POSform(variables, maxterms)
    
    return sop_form, pos_form

# 示例：获取(p∧q)∨(¬p∧r)的主范式
expr = Or(And(p, q), And(Not(p), r))
variables = [p, q, r]
pdnf, pcnf = get_canonical_forms(expr, variables)
print(f"主析取范式：{pdnf}")
print(f"主合取范式：{pcnf}")

4. 实际应用：逻辑难题求解

命题逻辑不仅存在于课本中，还能解决现实生活中的逻辑难题。让我们用Python来解决经典的"骑士与无赖"谜题：

在一个岛上住着骑士和无赖，骑士总是说真话，无赖总是说谎。你遇到两个人A和B。A说："B是骑士。" B说："我们两个不是同类人。" 问A和B各是什么身份？

我们可以用命题逻辑来建模并求解这个问题：

from sympy import satisfiable

# 定义命题：A是骑士，B是骑士
A_knight, B_knight = symbols('A_knight B_knight')

# A的陈述：B是骑士
A_statement = B_knight

# B的陈述：A和B不是同类人
B_statement = Not(Equivalent(A_knight, B_knight))

# 骑士说真话，无赖说谎
constraints = [
    Equivalent(A_knight, A_statement),
    Equivalent(B_knight, B_statement)
]

# 寻找满足所有约束的真值赋值
solution = satisfiable(And(*constraints))
print("谜题的解：")
print(f"A是{'骑士' if solution[A_knight] else '无赖'}")
print(f"B是{'骑士' if solution[B_knight] else '无赖'}")

另一个实际应用是电路设计。逻辑门本质上就是命题逻辑的物理实现。我们可以模拟基本的逻辑门电路：

class LogicGate:
    def __init__(self, name):
        self.name = name
        self.output = None
    
    def get_output(self):
        self.output = self.perform_gate_logic()
        return self.output

class AndGate(LogicGate):
    def __init__(self, name):
        super().__init__(name)
        self.input1 = None
        self.input2 = None
    
    def perform_gate_logic(self):
        return self.input1 and self.input2

# 构建一个AND-OR电路
and1 = AndGate("AND1")
and1.input1, and1.input2 = True, False

and2 = AndGate("AND2")
and2.input1, and2.input2 = False, True

or_gate = OrGate("OR")
or_gate.input1, or_gate.input2 = and1.get_output(), and2.get_output()

print(f"电路输出：{or_gate.get_output()}")

对于更复杂的逻辑系统，我们可以实现一个简单的命题逻辑证明器：

def natural_deduction(premises, conclusion):
    known = set(premises)
    steps = []
    
    # 尝试直接推导
    if conclusion in known:
        return True, steps
    
    # 尝试使用蕴含消解规则
    for premise in known:
        if isinstance(premise, Implies):
            if premise.args[0] in known:
                known.add(premise.args[1])
                steps.append(f"使用→消解：从{premise}和{premise.args[0]}推出{premise.args[1]}")
                if premise.args[1] == conclusion:
                    return True, steps
    
    # 尝试使用德摩根律等逻辑等价
    # 这里可以添加更多推理规则...
    
    return False, steps

# 示例：验证从p→q和¬q能否推出¬p
premises = {Implies(p, q), Not(q)}
success, proof_steps = natural_deduction(premises, Not(p))
print(f"推导成功：{success}")
for step in proof_steps:
    print(step)

通过这些实际例子，我们可以看到命题逻辑不仅是理论概念，更是可以实际编程实现的工具。用代码来表达和验证逻辑命题，不仅能加深理解，还能解决实际问题。