Logic Playground

Mathematics ought to embody absolute rigor and crystalline clarity. Yet traditional mathematical notation often falls short: its chaotic symbols and inconsistent structures force proofs to lean heavily on verbose natural language, creating barriers to both understanding and verification. This results in an enormous obstacle to the effective communication of mathematical ideas.

Traditional mathematical language suffers from two key shortcomings. First, it lacks a unified format for reasoning, making natural language indispensable for clarifying logical steps. Second, it offers no convenient and consistent way to express functions. For example, one can write $f(x) = \dots$ to define a function, but cannot simply write $f = \dots$, limiting elegant function abstraction.

Many axiomatic systems have addressed the first problem, but most are unfriendly to computer processing. The Lambda Calculus offers a compelling solution to the second problem with strikingly simple notation. However, it behaves more like a programming language and lacks the necessary components to serve mathematical proof.

My project, Logic Playground, combines the strengths of axiomatic systems and the Lambda Calculus. It removes the Lambda Calculus’s restriction of direct computability, adds expressive symbols for relations such as “for all”, and introduces a set of inference rules for proofs. This novel language is concise and uniform, with only eight operators and three keywords.

For more information, please refer to the wiki.

逻辑游乐场

数学应当体现绝对的严谨与清晰，然而传统数学符号往往力不从心：其混乱的符号与不一致的结构迫使证明严重依赖冗长的自然语言，为理解和验证设置了障碍，严重阻碍数学思想的高效传播。

传统数学语言存在两大缺陷：其一，缺乏统一的推理格式，必须依赖自然语言阐明逻辑步骤；其二，没有便捷统一的函数表达方式。例如可用 $f(x) = \dots$ 定义函数，却无法直接书写 $f = \dots$，限制了优雅的函数抽象。

众多公理系统已解决第一个问题，但大多难以适配计算机处理。λ演算（Lambda Calculus）以惊世骇俗的简洁符号为第二个问题提供了优雅解法，但其行为更接近编程语言，缺乏支撑数学证明的必要成分。

我的项目 Logic Playground 融合了公理系统与λ演算的优势：解除λ演算对直接可计算性的限制，添加"任意"等关系表达符号，并引入一套用于证明的推理规则。这种新型语言仅用八个运算符和三个关键词，兼具简洁性与统一性。

更多信息详见文档。