形式系统-tq系统

tq系统是在形式系统-pq系统的基础上，为形式化地表达“乘法”概念而设计的概念-形式系统。它在书中的主要作用是作为定义“合数”的工具，进而通过“衬底”的方式来反向定义“素数”，是阐释概念-图形与衬底思想的关键一步。

我们可以做一个与pq系统类似的系统，差别是这次我们表示的是乘法。我们称之为tq系统，“t”代表“乘”（英文是times）。

系统定义

符号

tq系统与pq系统类似，也使用 q 和 -（短杠），但用 t 代替了 p。

解释

系统的意向解释如下：

• t ↔ 乘 (times)
• q ↔ 等于 (equal)
• - (一串短杠) ↔ 其对应的自然数

根据这个解释，一个定理xqytz代表X = Y * Z，其中X, Y, Z分别是对应短杠串的长度。

公理模式

• 公理模式：xqxt-是一个公理，对任何一个短杠符号串x都是如此。

这个模式表达的是 X = X * 1。

推理规则

• 规则：设x、y、z都是短杠符号串。设xqytz是个已有的定理。那么，xyqytz-是个新的定理。

这条规则的本质是递归加法。如果已有X = Y * Z，那么下一步就是X + Y = Y * (Z + 1)。例如，从公理--q--t- (2=21)出发，应用一次规则可以得到----q--t-- (4=22)，再应用一次可以得到------q--t--- (6=2*3)。

tq系统的作用

tq系统本身只是一个简单的算术模型，但它为形式化地定义“合数”提供了基础。通过tq系统，可以建立一条新规则来生成所有代表合数的定理（C型定理），从而将合数定义为“图形”，而将素数定义为其“衬底”。

乘法是个比加法稍难对付的概念，现在已由印符操作“把握住”了……素数性质怎么样呢？这里有个看来聪明的计划：使用tq系统，定义一集形如Cx的新定理来刻划合数：

规则：设x、y、z是短杠符号串。如果xqy-tz-是定理，则Cx是定理。