| rdfs:comment
| - Der Gentzensche Hauptsatz oder Schnittsatz ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in Gentzentypkalkülen zulässig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies. (de)
- The cut-elimination theorem (or Gentzen's Hauptsatz) is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. (en)
- El teorema de corte-eliminación (o Gentzen Hauptsatz) es un teorema que establece la importancia del cálculo de secuentes. Fue demostrado por Gerhard Gentzen en 1934 en su artículo Investigaciones sobre la deducción lógica para los sistemas LJ y LK formalizando la lógica intuicionista y la lógica clásica, respectivamente. El teorema de corte-eliminación establece que cualquier demostración que tenga una demostración en el cálculo de secuentes y use la regla de corte, también tiene una demostración sin corte, es decir que no haga uso de la regla de corte. (es)
- En logique mathématique, le théorème d'élimination des coupures (ou Hauptsatz de Gentzen) est le résultat central établissant l'importance du calcul des séquents. Il a été initialement prouvé par Gerhard Gentzen en 1934 dans son article historique « Recherches sur la déduction logique » pour les systèmes LJ et LK formalisant la logique intuitionniste et classique, respectivement. Le théorème d'élimination des coupures stipule que toute déclaration qui possède une preuve dans le calcul des séquents, faisant usage de la règle de coupure, possède aussi une preuve sans coupure, à savoir, une preuve qui ne fait pas usage de la règle de coupure. (fr)
- 자름-제거 정리 또는 컷-제거 정리(영어: cut-elimination theorem)는 시퀀트 계산의 중요성을 보여주는 증명론의 중요 정리이다. 이는 본래 게르하르트 겐첸이 1934년 논문 "논리적 연역에 관한 연구(Untersuchungen über das logische Schließen)"에서 고전 논리와 직관 논리를 각각 형식화하는 시퀀트 계산 체계인 LJ와 LK를 제시하면서 증명한 것이다. 컷-제거 정리의 핵심은, 시퀀트 연산에서 자름 규칙(cut rule)을 사용하여 증명 가능한 식은 자름 규칙을 사용하지 않고도 증명하는 것이 가능하다는 내용이다. (ko)
- Il Teorema di eliminazione del taglio (o Hauptsatz di Gentzen) è il principale risultato che mostra l'importanza del calcolo dei sequenti. Venne dimostrato originariamente da Gerhard Gentzen nel suo storico articolo "Investigations in Logical Deduction" per i sistemi LJ ed LK, in cui sono formalizzate rispettivamente la logica intuizionista e la logica classica. Il teorema di eliminazione del taglio stabilisce che ogni giudizio che possiede nel calcolo dei sequenti una dimostrazione facente uso della regola del taglio possiede anche una dimostrazione senza taglio cioè una dimostrazione che non fa uso della regola del taglio. (it)
- カット除去定理（カットじょきょていり、英: Cut-elimination theorem）は、シークエント計算の手法の重要性を示す、数理論理学の主要な結果のひとつである。（数理論理学の）基本定理と呼ぶこともある。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "Investigations into Logical Deduction" で、古典論理と直観論理の体系をそれぞれ形式化したシークエント計算の形式的体系 LK 及び LJ において、最初に証明が与えられた。カット除去定理は、シークエント計算の推論規則であるカット規則を用いて証明可能な式には、カット規則を用いない証明図もまた必ず存在することを示したものである。 (ja)
- O teorema da eliminação do corte (ou Hauptsatz de Gentzen) é o resultado central que estabelece a significância do cálculo de sequentes. Foi originalmente provado por Gerhard Gentzen em 1934, no seu definidor artigo "Investigations in Logical Deduction", para os sistemas LJ e LK, formalizando as lógicas intuicionista e clássica, respectivamente. O teorema da eliminação do corte diz que qualquer derivação que possui uma prova no cálculo de sequentes que utiliza a regra do corte também possui uma prova que não a utiliza. (1) e (2) pode-se inferir (3) (1) e (2) pode-se inferir (3) (pt)
- Устранимость сечений (теорема Генцена, элиминационная теорема) — свойство логических исчислений, согласно которому всякую секвенцию, выводимую в данном исчислении, можно вывести без применения правила сечений. Играет фундаментальную роль в теории доказательств и важную методологическую роль в математической логике в целом в связи с тем, что предоставляет конструктивный метод доказательства непротиворечивости, в частности, для классической и интуиционистской логик первого порядка. (ru)
- 切消定理（cut-elimination theorem (or Gentzen's Hauptsatz)）是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中，拥有利用了切规则的证明的任何判断，也拥有无切证明，就是说，不利用切规则的证明。 相继式是与多个句子有关的逻辑表达式，形式为""，它可以被读做"A, B, C, 证明N, O, P"，并且（按Gentzen的注释）应当被理解为等价于真值函数"如果（A & B & C ）那么（N or O or P）"。注意LHS（左手端）是合取（and）而RHS（右手端）是析取（or）。LHS可以有任意多个公式；在LHS为空的时候，RHS是重言式。在LK中，RHS也可以有任意数目的公式--如果没有，则LHS是个矛盾，而在LJ中，RHS只能没有或有一个公式：在右紧缩规则前面，允许RHS有多于一个公式，等价于容许排中律。注意，相继式演算是相当有表达力的框架，已经为直觉逻辑提议了允许RHS有多个公式的相继式演算，而来自的逻辑LC得到了RHS最多有一个公式的经典逻辑的更加自然的形式化；逻辑和结构规则的相互作用是它的关键。 "切"是在相继式演算的正规陈述中的一个规则，并等价于在其他证明论中的规则变体，给出 （1） 和 （2） 你可以推出 （3） (zh)
|
| has abstract
| - Der Gentzensche Hauptsatz oder Schnittsatz ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in Gentzentypkalkülen zulässig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies. (de)
- The cut-elimination theorem (or Gentzen's Hauptsatz) is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. (en)
- El teorema de corte-eliminación (o Gentzen Hauptsatz) es un teorema que establece la importancia del cálculo de secuentes. Fue demostrado por Gerhard Gentzen en 1934 en su artículo Investigaciones sobre la deducción lógica para los sistemas LJ y LK formalizando la lógica intuicionista y la lógica clásica, respectivamente. El teorema de corte-eliminación establece que cualquier demostración que tenga una demostración en el cálculo de secuentes y use la regla de corte, también tiene una demostración sin corte, es decir que no haga uso de la regla de corte. (es)
- En logique mathématique, le théorème d'élimination des coupures (ou Hauptsatz de Gentzen) est le résultat central établissant l'importance du calcul des séquents. Il a été initialement prouvé par Gerhard Gentzen en 1934 dans son article historique « Recherches sur la déduction logique » pour les systèmes LJ et LK formalisant la logique intuitionniste et classique, respectivement. Le théorème d'élimination des coupures stipule que toute déclaration qui possède une preuve dans le calcul des séquents, faisant usage de la règle de coupure, possède aussi une preuve sans coupure, à savoir, une preuve qui ne fait pas usage de la règle de coupure. (fr)
- 자름-제거 정리 또는 컷-제거 정리(영어: cut-elimination theorem)는 시퀀트 계산의 중요성을 보여주는 증명론의 중요 정리이다. 이는 본래 게르하르트 겐첸이 1934년 논문 "논리적 연역에 관한 연구(Untersuchungen über das logische Schließen)"에서 고전 논리와 직관 논리를 각각 형식화하는 시퀀트 계산 체계인 LJ와 LK를 제시하면서 증명한 것이다. 컷-제거 정리의 핵심은, 시퀀트 연산에서 자름 규칙(cut rule)을 사용하여 증명 가능한 식은 자름 규칙을 사용하지 않고도 증명하는 것이 가능하다는 내용이다. (ko)
- Il Teorema di eliminazione del taglio (o Hauptsatz di Gentzen) è il principale risultato che mostra l'importanza del calcolo dei sequenti. Venne dimostrato originariamente da Gerhard Gentzen nel suo storico articolo "Investigations in Logical Deduction" per i sistemi LJ ed LK, in cui sono formalizzate rispettivamente la logica intuizionista e la logica classica. Il teorema di eliminazione del taglio stabilisce che ogni giudizio che possiede nel calcolo dei sequenti una dimostrazione facente uso della regola del taglio possiede anche una dimostrazione senza taglio cioè una dimostrazione che non fa uso della regola del taglio. (it)
- カット除去定理（カットじょきょていり、英: Cut-elimination theorem）は、シークエント計算の手法の重要性を示す、数理論理学の主要な結果のひとつである。（数理論理学の）基本定理と呼ぶこともある。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "Investigations into Logical Deduction" で、古典論理と直観論理の体系をそれぞれ形式化したシークエント計算の形式的体系 LK 及び LJ において、最初に証明が与えられた。カット除去定理は、シークエント計算の推論規則であるカット規則を用いて証明可能な式には、カット規則を用いない証明図もまた必ず存在することを示したものである。 (ja)
- O teorema da eliminação do corte (ou Hauptsatz de Gentzen) é o resultado central que estabelece a significância do cálculo de sequentes. Foi originalmente provado por Gerhard Gentzen em 1934, no seu definidor artigo "Investigations in Logical Deduction", para os sistemas LJ e LK, formalizando as lógicas intuicionista e clássica, respectivamente. O teorema da eliminação do corte diz que qualquer derivação que possui uma prova no cálculo de sequentes que utiliza a regra do corte também possui uma prova que não a utiliza. Um sequente é uma expressão lógica que relaciona múltiplas sentenças, na forma "", que deve ser lida como "A1, A2, A3, prova B1, B2, B3, ", e (como comentado por Gentzen) deve ser entendida como equivalente à função verdade "Se (A1 e A2 e A3 ) então (B1 ou B2 ou B3 )." Note que o lado esquerdo do sequente (LE) é uma conjunção (e) e o lado direito (LD) é uma disjunção (ou). O LE pode ter uma quantidade arbitrária de fórmulas; quando o LE é vazio, o LD é uma tautologia. No sistema LK, o LD também pode ter qualquer número de fórmulas - se não possui alguma, o LE é uma contradição, enquanto que no sistema LJ o LD pode apenas possuir uma ou nenhuma fórmula: aqui nós vemos que permitir mais de uma fórmula no LD é equivalente, na presença da regra de contração correta, à admissibilidade da lei do terceiro excluído. No entanto, o cálculo de sequentes é uma ferramenta bastante expressiva, e existiram proposições de cálculos de sequente para a lógica intuicionista que permitem muitas fórmulas no LD. Da lógica LC de Jean-Yves Girard é fácil obter uma formalização bastante natural da lógica clássica onde o LD contém no máximo uma fórmula; o diálogo das regras lógicas e estruturais é a chave neste ponto. O "Corte" é uma regra na formulação normal do cálculo de sequentes, e é equivalente a uma variedade de regras em outras teorias de prova, em que, dados (1) e (2) pode-se inferir (3) Isto é, ela "corta" as ocorrências da fórmula "A" da relação inferencial. O teorema da eliminação do corte diz que (para um dado sistema) qualquer sequente provável utilizando a regra do corte pode ser provado sem o uso desta regra. Para os cálculos de sequentes que possuem apenas uma fórmula no LD, a regra do corte é: dados (1) e (2) pode-se inferir (3) Se é um teorema, então a eliminação do corte neste caso simplesmente diz que um lema utilizado na prova desse teorema pode ser englobado. Sempre que a prova do teorema menciona o lema , nós podemos substituir as ocorrências pela prova de . Consequentemente, a regra do corte é . Para sistemas formulados no cálculo de sequentes, são aquelas que não utilizam a regra do corte. Tipicamente, uma prova deste tipo será maior, claro, e não necessariamente de maneira trivial. No seu ensaio "Don't Eliminate Cut!", George Boolos demonstrou que existia uma derivação que podia ser completada em uma página usando a regra do corte, mas cuja prova analítica não poderia ser completada durante toda a existência do universo. O teorema possui muitas e ricas consequências:
* Um sistema é inconsistente se admite uma prova do absurdo. Se o sistema tem um teorema de eliminação do corte, então, se ele possui uma prova do absurdo, ou do sequente vazio, ele também deve ter uma prova do absurdo (ou do sequente vazio) sem cortes. É tipicamente muito fácil demonstrar que não existem tais provas. Então, uma vez que é provada a posse do teorema da eliminação do corte por um sistema, é geralmente imediato o fato de que o sistema é consistente.
* Normalmente o sistema também tem, ao menos na lógica de primeira ordem, a , uma propriedade importante em várias abordagens da . A eliminação do corte é uma das ferramentas mais poderosas para provar o . A possibilidade de conduzir busca de prova baseada na resolução, o insight essencial que levou a linguagem de programação Prolog, dependem da admissibilidade do corte no sistema apropriado. Para sistemas de provas baseados em através de um isomorfismo de Curry–Howard, algoritmos de eliminação do corte correspondem à propriedade de normalização forte (todo termo de prova é reduzido num número finito de passos em uma forma normal). (pt)
- Устранимость сечений (теорема Генцена, элиминационная теорема) — свойство логических исчислений, согласно которому всякую секвенцию, выводимую в данном исчислении, можно вывести без применения правила сечений. Играет фундаментальную роль в теории доказательств и важную методологическую роль в математической логике в целом в связи с тем, что предоставляет конструктивный метод доказательства непротиворечивости, в частности, для классической и интуиционистской логик первого порядка. Для классического и интуиционистского исчислений секвенций свойство доказано Генценом в 1934 году. В 1953 году высказана гипотеза Такеути, согласно которой устранимость сечений имеет место для простой теории типов и соответствующих ей логик высших порядков, впоследствии она нашла подтверждение — для классической логики второго порядка устранимость сечений доказал , для простой теории типов — и , вскоре найдены доказательства для серии неклассических теорий высших порядков (Драгалин) и развитых теорий типов ( для системы F). Символическая формулировка: пусть и — доказуемые секвенции исчисления ; если — секвенция исчисления , то она доказуема. (ru)
- 切消定理（cut-elimination theorem (or Gentzen's Hauptsatz)）是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中，拥有利用了切规则的证明的任何判断，也拥有无切证明，就是说，不利用切规则的证明。 相继式是与多个句子有关的逻辑表达式，形式为""，它可以被读做"A, B, C, 证明N, O, P"，并且（按Gentzen的注释）应当被理解为等价于真值函数"如果（A & B & C ）那么（N or O or P）"。注意LHS（左手端）是合取（and）而RHS（右手端）是析取（or）。LHS可以有任意多个公式；在LHS为空的时候，RHS是重言式。在LK中，RHS也可以有任意数目的公式--如果没有，则LHS是个矛盾，而在LJ中，RHS只能没有或有一个公式：在右紧缩规则前面，允许RHS有多于一个公式，等价于容许排中律。注意，相继式演算是相当有表达力的框架，已经为直觉逻辑提议了允许RHS有多个公式的相继式演算，而来自的逻辑LC得到了RHS最多有一个公式的经典逻辑的更加自然的形式化；逻辑和结构规则的相互作用是它的关键。 "切"是在相继式演算的正规陈述中的一个规则，并等价于在其他证明论中的规则变体，给出 （1） 和 （2） 你可以推出 （3） 就是说，在推论关系中"切掉"公式"C"的出现。 切消定理声称（对于一个给定的系统）使用切规则的任何相继式证明也可以不使用这个规则来证明。如果我们认为是一个定理，则切消简单的声称用来证明这个定理的引理可以被内嵌（inline）。在这个定理的证明提及引理的时候，我们可以把它代换为的证明。因此，切规则是可接纳的。 对于用相继式公式化的系统，是不使用切规则的证明。这种证明典型的会很长，当然没有必要这么做。在散文《不要消除切呀!》中，展示了可以使用切在一页中完成的推导，而它的分析性证明要耗尽宇宙的寿命来完成。 这个定理有很多丰富的推论。一旦一个系统被证明有切消定理，这个系统通常立即就是一致的。这个系统通常也有，这是达成证明论语义的重要性质。切削是证明的最强力工具。基于归结原理的完成证明查找的可能性，导致Prolog编程语言的本质洞察，依赖于在适当的系统中接纳切规则。 (zh)
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)