查看中间逻辑的源代码
←
中间逻辑
跳转至:
导航
、
搜索
因为以下原因,你没有权限编辑本页:
你刚才请求的操作只对属于该用户组的用户开放:
用户
您可以查看并复制此页面的源代码:
'''中间逻辑''',或'''中介[[逻辑]]''',是在[[直觉主义逻辑]]和[[经典逻辑]]之间的'''中介''',这是在它们包含在[[直觉主义逻辑]]中不可证明的[[定理]],而又不等于的[[经典逻辑]]的意义上说的。这种逻辑也叫做'''超直觉主义'''或'''次经典'''逻辑。 有[[连续统的势]]个不同的中介逻辑,通常是向[[直觉主义逻辑]]增加一个或多个公理而获得的。 这种逻辑的例子有: * 直觉主义逻辑('''IPC''', '''Int''', '''IL''', '''H''') * 经典逻辑('''CPC''', '''Cl''', '''CL'''):'''IPC''' + P ∨ ¬P * 弱[[排中律]]逻辑('''KC''', [[V. A. Jankov|Jankov]]逻辑,[[德·摩根定律]]逻辑): '''IPC''' + ¬¬P ∨ ¬P * [[哥德尔]]-[[Michael Dummett|Dummett]]逻辑('''LC'''):'''IPC''' + (P → Q) ∨ (Q → P) * [[Georg Kreisel|Kreisel]]-[[Hilary Putnam|Putnam]]逻辑:'''IPC''' +(¬P →(Q ∨ R))→((¬P → Q) ∨ (¬P → R)) * [[Yuri T. Medvedev|Medvedev]]有限问题的逻辑 * [[可实现性]]逻辑 * [[Dana Scott|Scott]]逻辑:'''IPC''' + ((¬¬P → P) → (P ∨ ¬P)) →(¬¬P ∨ ¬P) * Smetanich逻辑:'''IPC''' + (¬Q → P) →(((P → Q) → P)→ P) 研究中介逻辑的工具类似于直觉主义逻辑所使用的,比如[[Kripke语义]]。例如,Gödel-Dummett逻辑相对于线序的Kripke模型完全。 ===语义=== 给定一个[[Heyting代数]]γ,在γ上有效的命题公式是中介逻辑。反过来说,给定一个中介逻辑可以构造出是 Heyting代数的它的[[Lindenbaum代数]]。 一个直觉主义[[Kripke框架]]''F''是[[偏序集合]],而Kripke模型''M''是带有求值使得 { ''x'' ∣ ''M'' , ''x'' ⊩ ''p'' } 是''F''的[[上闭集合|上闭子集]]的Kripke框架。在''F''中有效的命题公式的集合是在中介逻辑中有效的。给定一个中介逻辑Σ有可能构造一个Kripke模型''M''使得''M''的逻辑是Σ(这种构造叫做“典范模型”)。带有这个性质的Kripke框架可能不存在,但是[[一般框架]]总是有。 ===与模态逻辑的关系=== 设''A''是命题公式。''A''的“哥德尔-塔斯基翻译”递归定义如下: * T ( p n ) = ◻ p n * T ( ¬ A ) = ◻ ¬ T ( A ) * T ( A ∧ B ) = T ( A ) ∧ T ( B ) * T ( A ∨ B ) = T ( A ) ∨ T ( B ) * T ( A → B ) = ◻ ( T ( A ) → T ( B ) ) 如果Λ是'''S4'''的扩充则 ρΛ = {''A'' | ''T''(''A'') ∈ Λ}是中介逻辑,而Λ叫做ρΛ的“模态对应”。特别是: *'''IPC''' = ρ'''S4''' *'''KC''' = ρ'''S4.2''' *'''LC''' = ρ'''S4.3''' *'''CPC''' = ρ'''S5''' 对于所有中介逻辑Σ都有很多模态逻辑Λ使得Σ = ρΛ。 ===参见=== * [[直觉主义]] * [[BHK释义]] * [[直觉类型论]] * [[经典逻辑]] * [[线性逻辑]] * [[构造性证明]] * [[Curry-Howard对应]] * [[可计算性逻辑]] * [[博弈语义]] [[Category:形式逻辑系统]] [[Category:模态逻辑]]
返回
中间逻辑
。
导航菜单
个人工具
创建账户
登录
名字空间
页面
讨论
变种
查看
阅读
查看源代码
查看历史
操作
搜索
导航
首页
最近更改
随机页面
工具箱
链入页面
相关更改
特殊页面
页面信息
扫描二维码可以用手机浏览词条