Prop

在Rust中使用类型表示的命题逻辑。

一个使用直觉主义命题逻辑进行定理证明的Rust库。支持在经典命题逻辑中进行定理证明。

• 用于路径语义的研究
• 由AdvancedResearch社区提供
• 在Discord上加入我们！

缩写

• IPL: 直觉主义/构造性命题逻辑
• EL: 存在逻辑（非存在的排中律）
• PL: 经典命题逻辑
• PSI: 路径语义直觉主义/构造性命题逻辑
• PSEL: 路径语义存在逻辑
• PSL: 路径语义经典命题逻辑
• PSQ: 路径语义量子命题逻辑
• HOOO EP: 高阶运算符重载指数命题
• MEL: 中指数逻辑

动机

路径语义通过正常路径扩展了依赖类型，并也用于通过多个命题级别扩展经典命题逻辑。它还用于探索高维数学。路径语义中的一个热门研究领域是Avatar扩展。

在研究过程中，在某些情况下，确定一个证明是否在经典逻辑中可证，但在构造逻辑中不可证，可能是有用的。这需要能够轻松地比较证明。

这个库使用提升机制，使得在经典逻辑中产生证明并将其与构造逻辑中的证明进行比较变得更加容易。

设计

这个库包含

• Prop: 可决定或不可决定的命题（构造逻辑）
• EProp: 存在命题（存在逻辑）
• DProp: 可决定的命题（经典逻辑）
• LProp: 与Prop类似，但具有路径语义（路径语义构造逻辑）
• ELProp: 与EProp类似，但具有路径语义（路径语义存在逻辑）
• DLProp：类似于DProp，但具有路径语义（路径语义经典逻辑）
• 自动将非存在排中律提升到存在命题
• 自动将排中律提升到可判定命题
• 对Prop的证明使用双重否定
• IPL中的路径语义质量/质量模型（参见“quality”模块）
• IPL中的路径语义量子比特模型（参见“qubit”模块）
• IPL中的路径语义反-质量模型（参见“con_qubit”模块）
• Seshatic皇后性模型（参见“queenity”模块）
• 路径语义的核心公理的形式化
• 用于重言式/悖论式定理证明的指数命题（HOOO）
• 由HOOO EP派生出的S5模态逻辑模型
• 由HOOO EP和Avatar扩展理论派生出的Avatar模态逻辑模型
• 使用EL和HOOO EP的中间指数逻辑模型
• 根据构造（例如and或imply）在模块中组织策略

示例

use prop::*;

fn proof<A: Prop, B: Prop>(f: Imply<A, B>, a: A) -> B {
    imply::modus_ponens(f, a)
}

请注意，这里没有使用DProp，这意味着它是一个归纳证明。

use prop::*;

fn proof<A: DProp, B: DProp>(f: Imply<Not<A>, Not<B>>) -> Imply<B, A> {
   imply::rev_modus_tollens(f)
}

在这里，需要使用DProp，因为rev_modus_tollens需要排中律。这限制了证明只能适用于可判定命题。

路径语义

路径语义是数学编程的极富表现力的语言。它使用一个核心公理，该公理模型了符号的语义。

基本上，数学语言由于符号的使用而包含一种隐藏的对称性。出人意料的是，符号本身并不“内在地”属于逻辑。

可以这样表达，即符号“本身”编码了数学定律。隐藏的对称性可以利用来证明语义，有时还可以提高自动定理证明器的性能。

有关更多信息，请参阅路径语义项目。