高级数理逻辑第七章.pptVIP

存在性命题的两种解释证明 一个典型的存在性命题： 存在无理数a和b，使得ab是有理数。 证：若 是有理数，则a=b= 若 是无理数，则a= b= 对于存在性命题的构造性解释： 能找到无理数a和b，使得ab是有理数。 对应于构造性解释的证明为构造性证明。 构造性证明：必须证 是无理数。 构造性逻辑中自然推理系统 构造性逻辑不支持经典逻辑中的反证律，进而不支持排中律。 在构造性逻辑规则中，用以下两个规则替代反证律： (﹁+)若∑，A ├B， ∑ ，A ├﹁B， 则∑├ ﹁ A (﹁)若∑ ├A， ∑ ├﹁A， 则∑├B 构造性逻辑中公理推理系统 在公理推理系统中，用以下两个公理： (A→B) →((A→?B)→?A) ?A →(A→B) 替代 公理(?A→B) →((?A→?B)→A) ∑├cA A是在构造性逻辑中由∑C形式可推演（C形式可证明）的，记为∑├cA，当且仅当∑├cA能有限次使用构造性逻辑中形式推演规则生成。 一个有限序列∑1├cA1，∑2├cA2，…，∑n├cAn被称为∑n├cAn的C形式证明。其中， ∑k├cAk（1≤k≤n）由使用某一推演规则而生成。 证明? ? ?xA(x) ├c?x??A(x)。 证： (1) ?xA(x) ├ ?xA(x) (Ref) (2) ?xA(x) ├ A(u) u不在A(x)中出现 (?-)(1) (3) ﹁A(u) ，?xA(x) ├ A(u) (+)(2) (4) ﹁A(u) ，?xA(x) ├ ﹁A(u) (∈) (5) ﹁A(u) ├ ﹁?xA(x) (﹁+)(3)(4) (6) ?x(?A(x)) ├??xA(x) (?-)(5) (7) ???xA(x)，?x?A(x) ├??xA(x) (+)(5) (8) ???xA(x)，?x?A(x) ├???xA(x) (∈) (9) ???xA(x) ├ ??x?A(x) (﹁+)(7)(8) (10) ?A(u) ├ ?A(u) (Ref) (11) ?A(u) ├ ?x?A(x) (?+)(10) (12) ??x?A(x) ，?A(u) ├ ?x?A(x) (+)(11) (13) ??x?A(x) ，?A(u) ├ ??x?A(x) (∈) (14) ??x?A(x) ├ ? ?A(u) (﹁+)(12)(13) (15) ??x?A(x) ├ ?x??A(x) (?+)(14) (16) ? ? ?xA(x) ├ ?x??A(x) (Tr)(9)(15) ∑├zcA 定义：∑├zcA当且仅当存在序列A1，A2，…，An，使得A=An，且对于任何Ak，k=1，2，…，n，满足以下条件之一： Ak是公理 Ak∈∑ 存在i，jk，使得Ai= Aj→Ak 存在ik和B(u)，使得u不在∑中出现， Ai= B(u)，且Ak=?xB(x) A是在构造性逻辑中C形式可证明的 iff Ф├zcA 自然推理系统与公理推理系统的关系 设∑?Form(L )，A∈Form(L )，则 ∑├zcA 当且仅当 ∑├cA 构造性逻辑与经典逻辑的关系 设∑?Form(L )，A∈Form(L )。 若∑├cA，则∑├A 逆命题不成立。 Glivenko定理 设∑?Form(L p)，A∈Form(L p)。 ??∑├c??A 当且仅当 ∑├A 证明： 必要性。由??∑├c??A ，则??∑├??A 。进一步，可得∑├A。 充分性。对∑├A的结构进行归纳证明。 以证(?-)为例。 证明：若 ??∑， ???A ├c??B ??∑， ???A ├c???B