Web Analytics

See also ebooksgratis.com: no banners, no cookies, totally FREE.

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
Privacy Policy Cookie Policy Terms and Conditions
相继式 - Wikipedia

相继式

维基百科,自由的百科全书

证明论中,相继式是对在规定演绎演算的时候经常用到的可证明性的形式陈述。

目录

[编辑] 解释

相继式有如下形式

\Gamma\vdash\Sigma

这里的 Γ 和 Σ 二者是逻辑公式的序列(就是说公式的数目和出现次序都是重要的)。符号 \vdash 通常被称为十字转门(turnstile)或 T 型符号(tee),并经常被读做"产生"或"证明"。它不是语言中的符号,而用来讨论证明的元语言中的符号。在相继式中,Γ 叫做相继式的前件(antecedent)而 Σ 叫做相继式的后继(succedent)。

[编辑] 直觉意义

上面给出的那种相继式的直觉意义是在假定了 Γ 推出 Σ 是可证明的之下的。在经典的情形下,在十字转门左面的公式按合取解释,而右面的公式按析取解释。这意味着当在 Γ 中的所有公式成立的时候,在 Σ 中至少有一个公式必定是真的。如果后继为空,则按虚假解释,就是说 \Gamma\vdash 意味着 Γ 证明了虚假,并且因此是矛盾的。在另一方面,空前件被假定为真,就是说 \vdash\Sigma 意味着 Σ 没有任何假定就成立,也就是说,它总是真(作为一个析取式),而且因此是一个断言

但是上述解释只用于教学目的。因为在证明论中的形式证明是纯粹的语法上的,相继式的语义只由提供实际的推理规则的演算的性质给出。

剥离在上面的技术性精确定义中的任何矛盾,我们可以按它们的介绍性的逻辑形式来描述相继式。Γ 表示我们开始逻辑处理时做的假定的集合,例如 "苏格拉底是人" 和 "所有人都是必死的"。Σ 表示从这些前提得到的逻辑结论。例如,我们希望在十字转门的 Σ 端见到 "苏格拉底是必死的"。在这个意义上,\vdash 意味着推理过程,或者英语中的"所以"。

我们对这些符号指派的意思是有所助益的。规则自身按机械性本质来运做而不承载潜在的意义。这个主题的详情请参见哥德尔不完备定理

[编辑] 例子

一个典型的相继式:

\phi,\psi\vdash\alpha,\beta

它声称要么 α 要么 β 可以推导自 φψ

[编辑] 性质

因为在(左边的)的前件中的所有公式都必须为真来获得在(右边的)后继中至少一个公式为真,向任何一端增加公式都导致一个更弱的相继式,而从任何一端去除公式都得到更强的相继式。

[编辑] 规则

多数证明系统都提供从一个相继式到另一个相继式的演绎方式。这些规则都写成在横线上下的相继式列表。这些规则指示如果在横线上的所有相继式都为真,则在横线之下的也都为真。

一个典型的规则是:

\frac{\Gamma\vdash\Sigma}{\begin{matrix} \Gamma,\alpha\vdash\Sigma & \alpha,\Gamma\vdash\Sigma \end{matrix}}

这指示了如果我们可以演绎 ΣΓ,则我们也可以演绎它自 Γα 一起。

注意我们通常使用大写的希腊字母来指称(可能为空)公式的列表。[Γ,Σ] 被用来指示 ΓΣ 的紧缩,就是说,这些出现在要么 Γ 要么 Σ 中但不重复的那些公式的列表。

[编辑] 变体

这里介绍的相继式的一般概念能以各种方式特殊化。一个相继式被称为是直觉相继式,如果在后继中有最多一个公式。这种形式是获得直觉逻辑的演算是需要的。类似的,你可以通过要求相继式在前件中只有一个公式来获得双直觉逻辑(某种次协调逻辑)的演算。

在很多情况下,相继式还假定由多集或集合组成。所以你可以漠视公式的次序甚至数目。对于经典命题逻辑这不导致问题,因为你能从一组前提中得出的结论不依赖于这些数据。但是在亚结构逻辑中这就变得很重要了。

一些系统只允许在右边有一个公式。

[编辑] 历史

历史上,相继式是 Gerhard Gentzen 介入用来规定他著名的相继式演算。在他的德语出版物中他使用了单词 "Sequenz"。但是,在英语中,单词"序列" 已经用来翻译德语的 "Folge" 并在数学中经常出现。术语"相继式"被建立用做这个德语表达的替代翻译。

本文含有从PlanetMath上的Sequent来的材料,版权遵守GNU自由文档许可证

其他语言

Static Wikipedia (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2007 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2006 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Static Wikipedia February 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu