1. 素数判定的形式化系统，精彩！ 合数的判定系统比较容易构造，素数的判定当然不能简单的通过“不是合数”来解决。 首先构造一个不整除的概念(DND) 公理模式：xyDNDx，其中x和y是短横组成的符号串。（a>b，a自然不整除b） 生成规则：如果xDNDy是个定理，那么xDNDxy也是个定理。 接下来定义一个描述z在2到x的范围内没有因子的语言，zDFx (Divisor-Free) 规则1：如果–DNDz是个定理，那么zDF–也是个定理。 规则2：如果zDFx与x-DNDz都是定理，那么zDFx-也是个定理。 好了，到这里已经能检查一个数是否在给定范围内找出因子了，定义素数(Pz)就变得很简单。 规则：若z-DFz是个定理，那么Pz-是个定理。 再处理一个特例，为2制定一条公理 公理：P- -

本作品采用知识共享署名-非商业性使用 3.0 版本许可协议进行许可，欢迎转载，演绎，但是必须保留本文的署名 zellux（包含链接），且不得用于商业目的。