博文
双重形式化框架连接人类语言与机器计算：走向符号系统的统一理论
||
作者：邹晓辉1,2∗[0000-0002-5577-8245]
1 人类语言与机器计算人机互助新时代双重形式化方法实验室（北京大学跨学科知识建模课题组），1008712 融智学应用场景领军人才实训实操实践示范活动示范基地研究所(珠海横琴塞尔科技有限公司)，广东，519000
*通讯作者： zouxiaohui@pku.org.cn 949309225@qq.com
摘要：20世纪的形式语言传统，从塔斯基的真理语义论到卡尔纳普的逻辑句法，奠定了对象语言与元语言的基础性区分。然而，这一传统主要停留在哲学领域，留下了一个关键空白：形式语言如何同时服务于人类概念化和机器计算？本文引入了一个双重形式化框架，通过两个相互关联的系统填补这一空白：ge（言）所承载的是一种虚拟的符号对象语言，编码了人类表达的基本单元。术语“ge”源自单音节的汉字“言”导入的容器，记录言语行为、词语形式或语言体系在其具体表达元子对象的维度。在我们的框架中，ge所承载的元子对象包含八种模态，每种代表一种不同的符号表示模式；以及ip（语），一种元语言，通过范畴论态射控制ge对象的组合、变换和计算。这个id+ge/id+ip架构，根植于范畴论和类型论，同时支持人类可解释的符号表示和机器可执行的计算。ge和ip均有狭义与广义之分：狭义ge指单音节字（具体符号实例），广义ge指八大模态元子对象集合；狭义ip指多音节字组（具体组合规则），广义ip指元组态射，记录“哲逻数自社工文心”各领域的“三基一例”本体。该框架利用了一个关键事实：每种模态的元子对象构成有限的子全域（例如汉字部首约200个，数字0-9共10个）；复杂结构通过规则组合动态生成并由唯一标识符定位，从而无需暴力存储数十亿原子对象。核心方程包括：id+ge = pair（原子知识单元），ip = 一系列的 id+ge（规则构成），id+ip = pairs（规则知识图谱）。(id+ge双列表)与(id+ip多列表)共同构成了人机互助的机助人范例，它不仅处理“字式图表音像立活”八大模态的元子对象及其元组态射，形成多模态广义语言与广义文本；同时也处理“哲逻数自社工文心”多学科领域的“三基一例”术语本体、知识本体与常识本体，最终整合为软件本体信息处理。该框架的核心特征在于双重形式化与双重计算的并驾齐驱。通过人助机（human-assisted machine）机制，我们将id+ge双列表的左列表ge导入不同层次的对象，建构出三种双重形式化理解模型（A、B、C），分别对应直接形式化理解、基于多模态的间接形式化理解、以及基于汉语特例的间接形式化理解。这些模型共同构成了“双重形式化中文屋”与“孪生图灵机”，实现了计算机全自动批处理与人机互助的深度融合。我们展示了该框架如何将不同知识领域统一在共同的形式本体论下，以及它如何将塔斯基-卡尔纳普的遗产延伸到人机协作时代。该框架自2000年以来通过一系列专利和出版物逐步发展，最终形成了2011-2013年提出的间接形式化方法和双重计算模型。我们认为，这种双重形式化为人类语义丰富性与机器计算效率之间长期缺失的桥梁提供了解决方案，对人工智能、知识表示和科学的统一具有深远意义。关键词：双重形式化，对象语言，元语言，范畴论，类型论，人机协作，知识表示，融智学，中文屋，孪生图灵机，软件本体
1. 引言：形式语言的百年探索1.1 从莱布尼茨之梦到弗雷格的《概念文字》语言的形式化是二十世纪最深刻的知识成就之一。然而，这一探索的根源可以追溯到哲学史的深处。17世纪德国哲学家戈特弗里德·威廉·莱布尼茨设想了两大宏伟计划：第一，一个理性演算——一种理性的演算，将使“所有推理错误都仅仅是计算错误”[1]；第二，一个普遍字符——一种通用的人工语言，以取代自然语言的歧义[1]。莱布尼茨的愿景在两个世纪内仍未实现，等待着戈特洛布·弗雷格的非凡才华。
正是弗雷格在1879年发表了被许多逻辑学家视为现代逻辑诞生之作的著作：《概念文字：一种模仿算术的纯思维公式语言》[1]。在这部开创性著作中，弗雷格实现了莱布尼茨仅能想象的东西——他构建了第一个完全实现的形式系统，一个能够表示数学推理逻辑结构的“谓词演算”[1,2]。
弗雷格的成就是双重的。首先，他构建了一种人工语言，具有自己的词汇、形成规则和变换规则——一种摆脱了自然语言歧义和不规则性的语言[1]。其次，他公理化地组织了这种语言，遵循欧几里得为几何学开创的方法。在《概念文字》中，弗雷格提出了九条公理和四条推理规则，并由此推导出许多定理[1,2]。正如zbMATH对2018年批判性版本的评论所指出的：“弗雷格创造了150年后仍然有效的逻辑标准，特别是在命题逻辑的逻辑形式、逻辑理论中的演算概念、命题逻辑的演算、谓词逻辑的逻辑形式以及谓词理论方面”[2]。
弗雷格的工作启发了Łukasiewicz[3]、Russell与Whitehead[4]、Lewis[5]以及Kripke[6]等人的后续发展，使形式逻辑成为一门严谨的学科。
1.2 塔斯基的语义革命：对象语言与元语言虽然弗雷格给了我们第一个形式化的对象语言，但正是阿尔弗雷德·塔斯基在1930年代提供了用于谈论这些语言的概念工具。塔斯基的计划首先于1933年以波兰文发表，然后于1935年以德文“Der Wahrheitsbegriff in den formalisierten Sprachen”（形式化语言中的真理概念）发表，其动机是一个紧迫的问题：说谎者悖论[7,8]。
正如塔斯基所观察到的，说谎者悖论产生于一种语言是“语义封闭的”——即它包含自己的真理谓词并且可以指称自己的句子时。悖论可以简单地表述为：
句子1：句子1不是真的。
如果句子1是真的，那么它所说的必须成立，所以它不是真的。如果它不是真的，那么它所说的成立，所以它是真的。我们得到了一个矛盾[7,8]。
塔斯基的解决方案是坚持严格的语言层次结构[7,8]：
对象语言：我们谈论的语言，不包含像“真”或“假”这样的语义术语
元语言：我们用来谈论对象语言的语言，它包含对象语言作为一部分，加上语义谓词和研究对象语言的手段
塔斯基认为，真理只能在元语言中为对象语言的句子定义。著名的T-模式捕捉了这一洞见：
(T) “雪是白的”在英语中为真当且仅当雪是白的。[7]
这里，左边属于元语言（引用的句子作为对象语言句子的名称），而右边属于对象语言。正如索姆斯在其对塔斯基著作的阐述中所指出的，“塔斯基展示了如何在M中构造一个谓词T的定义，该谓词适用于L的所有且仅有的真句子。由于T是M的一部分而不是L的一部分，没有包含它的句子是它所适用的，因此无论在M还是L中都无法构造说谎者句子”[8]。
1.3 卡尔纳普的逻辑句法：作为演算的元语言鲁道夫·卡尔纳普在弗雷格和塔斯基的基础上，将语言的形式分析扩展到涵盖其句法结构。在他的代表作《语言的逻辑句法》中，该书于1934年首次以德文出版，1937年以英文出版，卡尔纳普发展了一种系统的理论，即他所谓的“逻辑句法”——独立于解释而考虑的语言形式结构[9]。
正如2022年中文译本记录所指出的，“语言的逻辑句法是指一种语言的语言形式的形式理论——即对支配一种语言的形式规则以及这些规则所产生的后果的系统阐述”[9]。卡尔纳普的目标是提供“一个概念系统，即提供一种语言，在其中可以精确表达逻辑分析的结果”[9]。
至关重要的是，卡尔纳普认识到逻辑句法必须在一个谈论对象语言的元语言中表述。这个元语言本身也可以形式化，导致语言的层次结构——这一主题后来将在我们的双重形式化框架中引起共鸣。
1.4 未解决的问题：从哲学形式化到机器计算从弗雷格经塔斯基到卡尔纳普的传统确立了形式语言理论的基本概念：对象语言、元语言、句法、语义以及语言的层次结构。然而，这一传统主要停留在哲学层面，而非操作层面。元语言虽然形式规范，但仍然是一种供人类推理的语言，而不是供机器计算的语言。
随后编程语言的发展——从Fortran到Python——创造了为机器设计的语言，但这些语言缺乏塔斯基-卡尔纳普框架的语义丰富性和跨领域通用性。编程语言是为计算而设计的，而不是为了表示人类知识在数学、自然语言、图表、声音和图像等方面的全部谱系。
近一个世纪以来一直未回答的问题是：我们能否构建一个形式语言系统，同时服务于人类概念化和机器计算，既保留语义丰富性又支持算法操作？
随着我们进入人机交互协作互助协同的新时代，这个问题变得越来越紧迫。最近关于人工通用智能数学基础的工作，如巴拉克里希南2025年的论文“基于同伦类型论和范畴论的通用智能数学”，认为“AGI需要一种预先存在的‘理解’机制，基于强大的抽象，使所有学习成为可能”[12]。巴拉克里希南提出范畴论和同伦类型论可以提供这样的抽象，并进一步认为——与普遍观点相反——“语义只能通过精心构建的句法结构产生”[12]。
本文介绍一个经过二十多年研究发展出的解决方案：融智学的双重形式化框架。该框架基于言（ge）作为对象语言和语（ip）作为元语言的区分，提供了一个统一的表示和计算符号的形式体系，涵盖所有人类知识领域——从数学、自然语言到图表、声音、图像甚至生命过程。
1.5 本文结构本文其余部分组织如下。第2节介绍核心理论框架，详细阐述id+ge / id+ip架构、狭义与广义的区分及其在范畴论和类型论中的数学基础，并引入人助机机制与三种理解模型。第3节追溯该框架从2000年到2013年的历史发展，借鉴了专利和出版物。第4节展示了在不同知识领域——数学、自然语言、中文书写以及跨学科整合中的应用。第5节考察该框架的理论意义，展示它如何扩展和操作化了塔斯基-卡尔纳普的遗产。第6节探讨了对人工智能和人机协作的启示，并进一步阐述三种理解模型的哲学与工程意涵。第7节概述了未来研究方向。第8节总结。
https://blog.sciencenet.cn/blog-94143-1525650.html
上一篇：为通用人工智能奠基的融智学新范式
