牛津大学Alexander Paseau教授线上讲演“形式化是什么”
点击次数: 更新时间:2025-06-30
本网讯(通讯员 时尚)6月25日晚,牛津大学Alexander Paseau教授应邀做题为“形式化是什么”的线上讲座。Paseau教授主要研究逻辑和数学哲学、形而上学、知识论等领域。讲座由足球博彩app 程勇教授主持,通过线上平台直播,参与者达200人次。
Paseau教授以“如何描述有效性”出发,介绍了当下主流观点:一个论证有效当且仅其形式的所有实例保真。由这个观点我们可以得到一般的形式方法用来判断对于一个自然语言下的语句集S,它是否可以推导出一个论断s。首先是将语句集S和s形式化到我们选取的逻辑系统L中。而在一个逻辑形式系统中,我们通常以语义(逻辑蕴含)和语法(形式推演)的方式来判断一个推导是否是有效的。我们虽然可以很熟练地完成这一步形式化,但问题是从自然语言到一个逻辑系统的“形式化”究竟是什么?是否存在一个评判标准来界定某种形式化方法是否是良好的?从字面意思看,形式化(formalisation)是将自然语言(如英语)句子映射到形式逻辑语言(如命题逻辑 PL、一阶逻辑 FOL)的过程。接着,教授介绍了三个传统的评判标准。第一个是“保持蕴含关系”,即形式化应保留自然语言中的蕴含结构,如 “布鲁因是熊” 蕴含 “存在熊”;第二是“尊重语法结构”,形式化需贴近自然语言的语法结构,如合取式对应自然语言中的“且”。比如将“今天下雨”形式化到命题逻辑通常是一个命题变元” ”,而非”
”,虽然后者仍然可以满足“保持蕴含关系”,但并不满足“尊重语法结构”;第三个是“语义接近性”,指形式化句子的语义应与原句尽可能接近,通过解释使形式符号贴近原句含义。
然后教授以这三个标准来比较命题逻辑和一阶逻辑,得到了一个非平凡的结论——它们是一样好的。这与我们通常的看法不同。比如形式化“布鲁因是熊” 蕴含 “存在熊”这个论断时,命题逻辑的通常做法是将“布鲁因是熊”和“存在熊”分别用命题变元 和
表示,但
并不是有效的。而一阶逻辑就有所不同了,我们可以将“布鲁因是熊”形式化为
(谓词符号
表示“···是熊”,变元符号
表示“布鲁因”),将“存在熊”形式化为
,而
是在一阶逻辑上有效的。Paseau教授给了一个不同的方法,在命题逻辑中,我们可以将“存在熊”形式化为“
”,其中
仍表示“布鲁因是熊”,
表示“有除了布鲁因之外的熊”,那这样即使在命题逻辑里,
,也是逻辑有效的。这样的方法是否可以更一般化呢?Paseau教授在其论文《Capturing Consequence》中给了详细证明。利用可数无穷无原子布尔代数的同构定理,证明可数语言下的一阶逻辑与命题逻辑的林登鲍姆代数同构,存在后承同构映射
,使得两者在蕴含结构上严格等价。不过注意对于非紧致的系统如二阶逻辑,与命题逻辑是不等价的。如果使用另外两个标准比较PL与FOL,我们仍可以得到类似的结果。
但事实上,我们仍认为一阶逻辑是不可或缺的。比如弗雷格、希尔伯特的形式化工作,在命题逻辑中是很难完成的。教授认为我们还需要第四种评判标准——认识论标准。若逻辑语言 L1 的形式化能比 L2 更有效地帮助用户辨识论证的有效性,则 L1 的形式化优于 L2。该标准强调形式化不仅需保留逻辑结构,还需具备认知实用性,即让使用者更直观、高效地理解和判断逻辑关系。Paseau教授举了一个形象的例子:形式化就像是一个地图。逻辑之于逻辑后承就像是地图之于它描述的区域。一个好的地图应该准确描述两地在现实中的相对位置(就像是一个好的形式化应该保持后承关系),但我们认为这份地图也应该具备良好的可读性。
评论互动环节,国际著名逻辑学家Harvey Friedman教授,足球博彩app 陈波教授、程勇教授、谢凯博老师以及线上听众与Paseau教授围绕形式化的标准等问题展开深入讨论。从数学基础角度,命题逻辑显然不足以形式化数学概念(如定义、证明),但缺乏严格证明其 “不充分性” 的依据。传统逻辑教学中直接转向一阶逻辑,未深入探讨为何命题逻辑不足。以及一阶逻辑无法刻画 “不可数”( Löwenheim-Skolem 定理),但数学中仍认为其可形式化基数陈述。而若形式化不要求语义等价(如真值条件对应),则标准是否过低?此外二阶逻辑表达力强(如可定义 “可数”),但因不紧致、不完全,认知上可能更复杂。认识论标准是否支持二阶逻辑?教授回应,技术上,命题逻辑与一阶逻辑在 “蕴含结构同构” 意义上等价,但数学实践中还需考虑其他标准(如刻画定义、证明步骤的能力)。形式化的语义标准需区分 “模型类对应” 与 “直观意义对应”。比如一阶逻辑对 “不可数” 的形式化(如通过无穷公理)是结构上的对应,而非严格语义等价。认识论标准需平衡表达力与认知成本:二阶逻辑虽能刻画更多概念,但推理规则复杂,且模型论解释不直观。一阶逻辑的优势在于 “表达力 - 认知成本” 的平衡:既能处理大部分数学概念,又有完备的证明系统,便于用户验证有效性另外,教授承认一阶逻辑常为保持蕴含而牺牲表面语法,但认为 “保持蕴含关系” 优先于 “尊重语法结构”。尊重语法结构具有主观性。语法标准应注意 “布尔结构一致性”(如合取、析取的对应),而非表面词汇结构,这是不同逻辑可共识的最低语法要求。所以说,形式化的 “正确性” 与 “认知可及性” 需平衡,逻辑工具的选择应该兼具理论严谨性与实用便利性。
(编辑:邓莉萍 审稿:刘慧)