公理化中的EQPL必须定义的递归可枚举算术公式

在公理化中，蕴涵是EQPL 必须定义的。如果Γ 蕴涵δ，写作Γ∣∣-δ。对于任意w 和ρ 满足Γ 中的任意元素，则wρ∣∣-η。给定一个量子系统的有限集合F，如果F∈∪S，则称量子结构w=（V，S，∣ψ〉，v）是F 可分解的。给定一个F 上的量子公式集合Γ 和一个F 上的量子公式η，对于任意F 分解w和ρ满足Γ 的任意元素，如果wρ╟η，则说在F 上Γ 蕴涵η，写作Γ╟Fη。明显地，对于任意F，Γ ╟η 蕴含Γ ∣∣-Fη，此外，对于F1 上的任意Γ 和η，如果F1⊆F2，并且Γ╟F2η，那么Γ╟F1η。

对于量子位符号中的任意有限集F，其公理和推理规则如下：

公理包括：

推理规则：

两条推理规则分别是经典蕴涵CMP 的模态和量子蕴涵QMP 的模态。事实上，CMP 可以从QMP 和Lift⇒衍生出来。

作为公理，经典重言式[CTaut]和量子重言式[QTaut]的集合都是递归的。

公理[Oracle]是有争议的，不过我们可以接受任何有效的算术公式。值得注意的是，这组有效的算术公式是递归可枚举的，因此选择了这一公理。使用该公理的原因包括：首先，希望在不丢失数学细节的前提下实现量子方面的推理；其次，为了保持完备性，提出一种基于代数闭域理论的递归公理化的替代方法需要我们放松相应的语义，这可能是朝着远离量子力学假设的直觉根源的方向。

公理[Lift⇒]，[Eqv⊥]和[Ref⊓]可以将（局部）经典推理和（全局）量子重言式推理联系起来，这些是在全局逻辑中联系经典连接词和全局连接词的公理。

公理[If ㅜ]和[If⊥]在完整性证明中用于删除替代项。

公理[NEtgF]，[NEtg∣]，[NEtg∪]和[NEtg\]足以实现对子系统进行推理，这些公理共同规定了子系统在集合论操作下是封闭的。

公理[Empty]，[NAdm]和[Unit]规范了逻辑振幅。每一个公理都密切反映了语义结构的一个属性。公理Empty 指出，逻辑振幅∣⊤〉øø 总是为1。公理Unit 表明每个子系统的状态是一个单位向量。公理NAdm 表明，不允许经典赋值的振幅为0。

公理[Prob]将概率和振幅联系起来。(www.xing528.com)

如果能建立起从公理和以公式集合F 中的公式为假设的推理规则中建立一个η 的推导，则认为，F 上的一个公式η 是一个F-定理，写作├Fη。

作为公理化的说明，考虑任意有限的F，建立如下公理：

证明：PUnit 的推导：

下面的定理是非纠缠公理的直接推论，实现了集合论运算下非纠缠闭合的场景。

下面的定理对逻辑振幅的主要性质给出了一些见解。

以下关于测量后的概率的定理中，第一个说明了有限可加性，第二个将逻辑推理与概率推理（单调性）联系起来。第三个说明了有限量子位的可测量性。

下列公理表明，量子模态和概率模态的行为类似。

引理：假言三段论。设γ1，γ2，γ3 为量子式。则：

证明：通过QTaut 可知：

该命题是通过使用两个QMP 实例得出的。