Deduction theorem (original) (raw)
Unter dem Begriff Deduktionstheorem sind zwei eng verwandte Theoreme bekannt, die in der mathematischen Logik von Bedeutung sind. Eine Variante des Theorems, auch als Folgerungstheorem bekannt, zielt auf den Begriff der semantischen Folgerung ab. Die andere Variante, die innerhalb von Kalkülen Anwendung findet, macht statt der (semantischen) Folgerung die (syntaktische) Ableitung zum Ausgangspunkt. In beiden Fällen wird eine Beziehung zur materialen Implikation hergestellt.
| Property | Value |
|---|---|
| dbo:abstract | Unter dem Begriff Deduktionstheorem sind zwei eng verwandte Theoreme bekannt, die in der mathematischen Logik von Bedeutung sind. Eine Variante des Theorems, auch als Folgerungstheorem bekannt, zielt auf den Begriff der semantischen Folgerung ab. Die andere Variante, die innerhalb von Kalkülen Anwendung findet, macht statt der (semantischen) Folgerung die (syntaktische) Ableitung zum Ausgangspunkt. In beiden Fällen wird eine Beziehung zur materialen Implikation hergestellt. (de) In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication A → B, assume A as an hypothesis and then proceed to derive B—in systems that do not have an explicit inference rule for this. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction. In more detail, the propositional logic deduction theorem states that if a formula is deducible from a set of assumptions then the implication is deducible from ; in symbols, implies . In the special case where is the empty set, the deduction theorem claim can be more compactly written as: implies . The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if is a closed formula). In general a deduction theorem needs to take into account all logical details of the theory under consideration, so each logical system technically needs its own deduction theorem, although the differences are usually minor. The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However, there are first-order systems in which new inference rules are added for which the deduction theorem fails. Most notably, the deduction theorem fails to hold in Birkhoff–von Neumann quantum logic, because the linear subspaces of a Hilbert space form a non-distributive lattice. (en) El teorema de la deducción es un metateorema de la lógica proposicional, la lógica de primer orden y otros sistemas lógicos, que es bastante utilizado para demostrar otros metateoremas. Se trata de una formalización de la técnica de demostración ordinaria según la cual para demostrar que de A se sigue B, basta con suponer A y a partir de ello llegar a la conclusión de que B. Más formalmente, el teorema establece que si una fórmula B es deducible (en un sistema deductivo S) a partir del conjunto de fórmulas , entonces A → B es deducible a partir de solamente. En símbolos: implica O alternativamente, en la notación del cálculo de secuentes: implica En el caso especial donde es el conjunto vacío, el teorema de la deducción dice que: implica El teorema de la deducción parece haber sido demostrado por primera vez por Alfred Tarski en 1921, pero la primera demostración publicada es de Jacques Herbrand en 1930. (es) Nella logica matematica, il teorema di deduzione afferma che se una formula F è deducibile da un'altra formula E allora l'implicazione E → F è dimostrabile (ovvero è "deducibile" dall'insieme vuoto) e, viceversa, che se l'implicazione E → F è dimostrabile, allora la formula F è deducibile da E. In simboli, se e solo se . Più in generale, esso afferma che, se da un insieme di formule Γ è dimostrabile E → F, allora F è deducibile dall'insieme di premesse [Γ + (E)]. Il teorema di deduzione può essere generalizzato ad una sequenza numerabile di formule tali che da , si inferisce, e così via fino a . Il teorema di deduzione è un meta-teorema: è usato per dedurre dimostrazioni in una certa teoria sebbene non sia un teorema della stessa teoria. (it) 수리논리학에서 연역 정리(영어: deduction theorem)는 술어 논리 및 1차 논리의 (metatheorem)로, 전제된 논리식 E로부터 논리식 F를 연역가능하다면 함의 E → F가 증명가능(공집합으로부터 연역 가능)하다는 정리이다. 기호로 나타내면 이면 이라는 것이다. 연역 정리는 다음과 같이 임의의 개수의 유한한 전제 논리식들로 일반화할 수 있다: 로부터를 추론가능하며, 결국 로 된다. 연역 정리는 왜 수학에 있어서 조건절의 증명이 논리적으로 참이 되는가를 설명해준다. 이는 직관적으로 '자명하다'고 받아들여져 왔으나, 20세기 초에 에르브랑과 타르스키는 (제각각) 이것이 일반적인 경우에 논리적으로 올바르다는 것을 보였다. (ko) Twierdzenie o dedukcji – jeżeli jest zdaniem oraz to formuła zdaniowa należy do zbioru gdzie to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych (pl) 演繹定理（英: Deduction theorem）とは、数理論理学において、論理式 E から 論理式 F が演繹可能ならば、含意 E → F が証明可能である（すなわち、空集合から演繹可能）、というもの。記号的に表すと、 ならば、 である。 演繹定理は、以下のように任意個の有限な前提論理式群に一般化できる。 から が推論でき、最終的に となる。 演繹定理はである。つまり、理論自身の定理ではないが、その理論における演繹的証明に使われる。 演繹メタ定理は、メタ定理の中でも最も重要である。論理体系のなかには、これを推論規則（"→" の導入規則）として採用したもの（自然演繹）もある。そうでない体系でも、公理群から演繹定理を証明することでその論理体系が完全であることを示すのが一般的である。で何かを証明する場合、演繹メタ定理なしでは証明が困難となる。逆に演繹メタ定理を使えば、証明は非常に簡単になる。 (ja) Na lógica matemática, o teorema da dedução é um metateorema da lógica de primeira ordem. É a formalização da comum técnica de prova na qual uma implicação A → B é provada assumindo A e então derivando B a partir da premissa associada a resultados conhecidos. O teorema da dedução explica o porquê de provas de sentenças condicionais na matemática serem logicamente corretas. Embora isto tenha parecido por séculos "óbvio" para os matemáticos literalmente que provar B a partir de A, associado a um conjunto de teoremas era suficiente para provar a implicação A → B baseado nestes teoremas somente, foi deixado a Herbrand e Tarski mostrar (de forma independente entre os dois) que isto era logicamente correto no caso mais geral—outro exemplo,talvez, da lógica moderna "limpando" as práticas matemáticas. O teorema da dedução afirma que se uma fórmula B é dedutível a partir de um conjunto de premissas , onde A é uma fórmula fechada, então a implicação A → B é dedutível a partir de . Nos símbolos, implica . No caso especial, onde é um conjunto vazio, o teorema da dedução mostra que implica . O teorema da dedução é seguro para todas as teorias de primeira ordem com o sistema dedutivo para lógica de primeira ordem usual. No entanto, existem outros sistemas de primeira ordem nos quais novas regras de inferência são adicionadas e para o qual o teorema da dedução é falho. A regra de dedução é uma propriedade importante dos sistemas de Hilbert, pois o uso desde metateorema leva a mais provas curtas do que seria possível sem o mesmo. Embora o teorema da dedução pudesse ser escolhido como uma regra primitiva de inferência em alguns sistemas, essa aproximação não é sempre seguida; ao invés disso, o teorema da dedução é obtido como uma regra admissível usando outros axiomas lógicos e o modus ponens. Em outros sistemas de prova formal, o teorema da dedução é às vezes escolhido como uma primitiva regra de inferência. Por exemplo, na dedução natural, o teorema da dedução é relançado como uma regra de introdução para a "→". (pt) Deduktionsteoremet (även kallad "CP-regeln", från engelska: Conditional Proof) är ett metateorem inom satslogiken. Teoremet är en vid bevisföring effektiv slutledningsregel, som ofta används då en slutsats skall härledas, där huvudoperationen är en materiell implikation. Alfred Tarski bevisade teoremet 1931, men det tidigaste publicerade beviset var av Jacques Herbrand, 1930. Deduktionsteoremet: Om man från en premissmängd H = {P1,....Pn} jämte en formel F kan härleda slutsatsen G, så kan man från H härleda F→G. Deduktionsteoremet uttryckt med symboler: H ʌ F G implicerar H F→G, där symbolen, , betecknar syntaktisk konsekvens. I det fall då premissmängden H är tom följer av deduktionsteoremet, att F G implicerar F→G, vilket betyder att F→G är en tautologi. (sv) Теоре́ма про деду́кцію (ле́ма про деду́кцію, теоре́ма деду́кції) — один із фундаментальних результатів у теорії доведення, формалізує спосіб міркування, за якого для встановлення імплікації використовується як необхідна умова виведення. Використовується для встановлення існування висновків і доведень без їх побудови. Вперше явно сформулював і довів Ербран, а без доведення використовував її 1928 року. Незалежно цей принцип сформулював 1930 року Тарський. За повідомленням Тарського, він знав і застосовував цей принцип ще 1921 року. (uk) Теорема о дедукции (лемма о дедукции, теорема дедукции) — один из фундаментальных результатов в теории доказательств, формализует способ рассуждения, при котором для установления импликации используется в качестве необходимого условия вывода. Используется для установления существования выводов и доказательств, не используя их построения. Впервые была явно сформулирована и доказана в 1930 году Эрбраном, а без доказательств использовалась Эрбраном в 1928 году. Независимо этот принцип был сформулирован Тарским в 1930 году. По сообщению Тарского, он знал и применял этот принцип еще в 1921 году. (ru) 演绎定理是数理逻辑的一個核心規則，它清晰地描述元語言的純符號組合所做的演繹與逻辑语言裡的实质条件的聯繫。 (zh) |
| dbo:wikiPageExternalLink | http://www.ltn.lv/~podnieks/mlog/ml.htm https://www3.nd.edu/~cfranks/dt.pdf |
| dbo:wikiPageID | 480010 (xsd:integer) |
| dbo:wikiPageLength | 19090 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1115331898 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_calculus dbr:Quantum_logic dbr:Metatheorem dbr:John_von_Neumann dbr:Currying dbr:Cut-elimination_theorem dbr:Peirce's_law dbr:Combinatory_logic dbc:Proof_theory dbr:Mathematical_logic dbr:Garrett_Birkhoff dbr:Conditional_proof dbr:Empty_set dbr:Propositional_logic dbr:Distributive_lattice dbr:Linear_subspace dbr:A_K_Peters dbr:Curry–Howard_correspondence dbr:First-order_logic dbc:Theorems_in_the_foundations_of_mathematics dbr:Carl_Hewitt dbr:Natural_deduction dbr:Well-formed_formula dbr:Hilbert_space dbr:Tautology_(logic) dbc:Deductive_reasoning dbc:Metatheorems dbr:Lambda_calculus dbr:Theory_(mathematical_logic) dbr:Modus_ponens dbr:Dover_Publications dbr:Axiom_schema dbr:Springer_Science+Business_Media dbr:Meta-theorem dbr:New_York_City dbr:Generalization_(logic) dbr:Rule_of_inference dbr:Sentence_(mathematical_logic) dbr:Implication_introduction dbr:Springer-Verlag dbr:First_order_logic dbr:Lambda_elimination dbr:Inference_rule dbr:Hilbert-style_deduction_system |
| dbp:wikiPageUsesTemplate | dbt:Citation dbt:Short_description |
| dct:subject | dbc:Proof_theory dbc:Theorems_in_the_foundations_of_mathematics dbc:Deductive_reasoning dbc:Metatheorems |
| rdf:type | yago:WikicatMathematicalTheorems yago:WikicatTheoremsInTheFoundationsOfMathematics yago:Abstraction100002137 yago:Communication100033020 yago:Message106598915 yago:Proposition106750804 yago:Statement106722453 yago:Theorem106752293 |
| rdfs:comment | Unter dem Begriff Deduktionstheorem sind zwei eng verwandte Theoreme bekannt, die in der mathematischen Logik von Bedeutung sind. Eine Variante des Theorems, auch als Folgerungstheorem bekannt, zielt auf den Begriff der semantischen Folgerung ab. Die andere Variante, die innerhalb von Kalkülen Anwendung findet, macht statt der (semantischen) Folgerung die (syntaktische) Ableitung zum Ausgangspunkt. In beiden Fällen wird eine Beziehung zur materialen Implikation hergestellt. (de) 수리논리학에서 연역 정리(영어: deduction theorem)는 술어 논리 및 1차 논리의 (metatheorem)로, 전제된 논리식 E로부터 논리식 F를 연역가능하다면 함의 E → F가 증명가능(공집합으로부터 연역 가능)하다는 정리이다. 기호로 나타내면 이면 이라는 것이다. 연역 정리는 다음과 같이 임의의 개수의 유한한 전제 논리식들로 일반화할 수 있다: 로부터를 추론가능하며, 결국 로 된다. 연역 정리는 왜 수학에 있어서 조건절의 증명이 논리적으로 참이 되는가를 설명해준다. 이는 직관적으로 '자명하다'고 받아들여져 왔으나, 20세기 초에 에르브랑과 타르스키는 (제각각) 이것이 일반적인 경우에 논리적으로 올바르다는 것을 보였다. (ko) Twierdzenie o dedukcji – jeżeli jest zdaniem oraz to formuła zdaniowa należy do zbioru gdzie to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych (pl) 演繹定理（英: Deduction theorem）とは、数理論理学において、論理式 E から 論理式 F が演繹可能ならば、含意 E → F が証明可能である（すなわち、空集合から演繹可能）、というもの。記号的に表すと、 ならば、 である。 演繹定理は、以下のように任意個の有限な前提論理式群に一般化できる。 から が推論でき、最終的に となる。 演繹定理はである。つまり、理論自身の定理ではないが、その理論における演繹的証明に使われる。 演繹メタ定理は、メタ定理の中でも最も重要である。論理体系のなかには、これを推論規則（"→" の導入規則）として採用したもの（自然演繹）もある。そうでない体系でも、公理群から演繹定理を証明することでその論理体系が完全であることを示すのが一般的である。で何かを証明する場合、演繹メタ定理なしでは証明が困難となる。逆に演繹メタ定理を使えば、証明は非常に簡単になる。 (ja) Теоре́ма про деду́кцію (ле́ма про деду́кцію, теоре́ма деду́кції) — один із фундаментальних результатів у теорії доведення, формалізує спосіб міркування, за якого для встановлення імплікації використовується як необхідна умова виведення. Використовується для встановлення існування висновків і доведень без їх побудови. Вперше явно сформулював і довів Ербран, а без доведення використовував її 1928 року. Незалежно цей принцип сформулював 1930 року Тарський. За повідомленням Тарського, він знав і застосовував цей принцип ще 1921 року. (uk) Теорема о дедукции (лемма о дедукции, теорема дедукции) — один из фундаментальных результатов в теории доказательств, формализует способ рассуждения, при котором для установления импликации используется в качестве необходимого условия вывода. Используется для установления существования выводов и доказательств, не используя их построения. Впервые была явно сформулирована и доказана в 1930 году Эрбраном, а без доказательств использовалась Эрбраном в 1928 году. Независимо этот принцип был сформулирован Тарским в 1930 году. По сообщению Тарского, он знал и применял этот принцип еще в 1921 году. (ru) 演绎定理是数理逻辑的一個核心規則，它清晰地描述元語言的純符號組合所做的演繹與逻辑语言裡的实质条件的聯繫。 (zh) In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication A → B, assume A as an hypothesis and then proceed to derive B—in systems that do not have an explicit inference rule for this. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction. (en) El teorema de la deducción es un metateorema de la lógica proposicional, la lógica de primer orden y otros sistemas lógicos, que es bastante utilizado para demostrar otros metateoremas. Se trata de una formalización de la técnica de demostración ordinaria según la cual para demostrar que de A se sigue B, basta con suponer A y a partir de ello llegar a la conclusión de que B. Más formalmente, el teorema establece que si una fórmula B es deducible (en un sistema deductivo S) a partir del conjunto de fórmulas , entonces A → B es deducible a partir de solamente. En símbolos: implica implica (es) Nella logica matematica, il teorema di deduzione afferma che se una formula F è deducibile da un'altra formula E allora l'implicazione E → F è dimostrabile (ovvero è "deducibile" dall'insieme vuoto) e, viceversa, che se l'implicazione E → F è dimostrabile, allora la formula F è deducibile da E. In simboli, se e solo se . Più in generale, esso afferma che, se da un insieme di formule Γ è dimostrabile E → F, allora F è deducibile dall'insieme di premesse [Γ + (E)]. Il teorema di deduzione può essere generalizzato ad una sequenza numerabile di formule tali che da , si inferisce, e così via fino a (it) Deduktionsteoremet (även kallad "CP-regeln", från engelska: Conditional Proof) är ett metateorem inom satslogiken. Teoremet är en vid bevisföring effektiv slutledningsregel, som ofta används då en slutsats skall härledas, där huvudoperationen är en materiell implikation. Alfred Tarski bevisade teoremet 1931, men det tidigaste publicerade beviset var av Jacques Herbrand, 1930. Deduktionsteoremet: Om man från en premissmängd H = {P1,....Pn} jämte en formel F kan härleda slutsatsen G, så kan man från H härleda F→G. (sv) Na lógica matemática, o teorema da dedução é um metateorema da lógica de primeira ordem. É a formalização da comum técnica de prova na qual uma implicação A → B é provada assumindo A e então derivando B a partir da premissa associada a resultados conhecidos. O teorema da dedução explica o porquê de provas de sentenças condicionais na matemática serem logicamente corretas. Embora isto tenha parecido por séculos "óbvio" para os matemáticos literalmente que provar B a partir de A, associado a um conjunto de teoremas era suficiente para provar a implicação A → B baseado nestes teoremas somente, foi deixado a Herbrand e Tarski mostrar (de forma independente entre os dois) que isto era logicamente correto no caso mais geral—outro exemplo,talvez, da lógica moderna "limpando" as práticas matemátic (pt) |
| rdfs:label | Deduktionstheorem (de) Teorema de la deducción (es) Deduction theorem (en) Teorema di deduzione (it) 演繹定理 (ja) 연역 정리 (ko) Twierdzenie o dedukcji (pl) Teorema da dedução (pt) Deduktionsteoremet (sv) Теорема о дедукции (ru) 演绎定理 (zh) Теорема про дедукцію (uk) |
| owl:sameAs | freebase:Deduction theorem yago-res:Deduction theorem wikidata:Deduction theorem dbpedia-de:Deduction theorem dbpedia-es:Deduction theorem dbpedia-fa:Deduction theorem dbpedia-it:Deduction theorem dbpedia-ja:Deduction theorem dbpedia-ko:Deduction theorem dbpedia-pl:Deduction theorem dbpedia-pt:Deduction theorem dbpedia-ru:Deduction theorem dbpedia-sr:Deduction theorem dbpedia-sv:Deduction theorem dbpedia-uk:Deduction theorem dbpedia-zh:Deduction theorem https://global.dbpedia.org/id/DocV |
| prov:wasDerivedFrom | wikipedia-en:Deduction_theorem?oldid=1115331898&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Deduction_theorem |
| is dbo:wikiPageRedirects of | dbr:Deduction_Theorem dbr:Paraconsistent_deduction_theorem dbr:Resolution_theorem dbr:Virtual_rule_of_inference dbr:Deduction_meta-theorem dbr:Deduction_metatheorem dbr:Deductive_analysis |
| is dbo:wikiPageWikiLink of | dbr:Propositional_calculus dbr:Metatheorem dbr:Cut-elimination_theorem dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(D–H) dbr:List_of_mathematical_logic_topics dbr:List_of_rules_of_inference dbr:Peirce's_law dbr:Combinatory_logic dbr:Conditional_proof dbr:Deduction_Theorem dbr:What_the_Tortoise_Said_to_Achilles dbr:Paraconsistent_logic dbr:Curry–Howard_correspondence dbr:Judgment_(mathematical_logic) dbr:Universal_generalization dbr:Heyting_algebra dbr:Hilbert_system dbr:Abstract_algebraic_logic dbr:Theory_(mathematical_logic) dbr:Bunched_logic dbr:Implicational_propositional_calculus dbr:Sequent_calculus dbr:Rule_of_inference dbr:List_of_theorems dbr:T-norm_fuzzy_logics dbr:Paraconsistent_deduction_theorem dbr:Resolution_theorem dbr:Virtual_rule_of_inference dbr:Deduction_meta-theorem dbr:Deduction_metatheorem dbr:Deductive_analysis |
| is foaf:primaryTopic of | wikipedia-en:Deduction_theorem |