Natural deduction (original) (raw)
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.
| Property | Value |
|---|---|
| dbo:abstract | Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen und philosophischen Logik einen Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski – einem Vertreter der Lemberg-Warschau-Schule – entwickelt wurde. Der Begriff des Kalküls des natürlichen Schließens (KdnS) ist nicht streng definiert, stattdessen gibt es eine Reihe von Merkmalen, die auf KdnS in unterschiedlichem Maße zutreffen und dabei bestimmen, wie typisch das Exemplar für die Gattung ist. * Anders als bei den allermeisten anderen Kalkültypen wie Tableaukalkül, Axiomatischem Kalkül, Dialogkalkül etc. gibt es im KdnS die Möglichkeit, Aussagen anzunehmen, die für eine Weile innerhalb der Ableitung ihre Gültigkeit haben. Diese Annahmen können später wieder getilgt werden (siehe dazu auch unten). Dieses Merkmal macht einen großen Anteil an der „Natürlichkeit“ des Schließens im KdnS aus, denn es entspricht der gängigen Praxis in mathematischen Beweisen. * Im Gegensatz zu axiomatischen Kalkülen enthält ein System natürlichen Schließens keine bzw. kaum Axiome, sondern hauptsächlich eine größere Zahl von Schlussregeln. Zusammen mit den gleichfalls von Gentzen entwickelten Sequenzenkalkülen gehören Systeme des natürlichen Schließens deshalb zur Familie der Regellogiken oder Regelkalküle. * Die Schlussregeln in einem KdnS sollten intuitiv zu rechtfertigen sein, am besten prätheoretisch akzeptierten Beweistechniken entsprechen. Auch dieses Merkmal trägt zur „Natürlichkeit“ des Schließens bei. * Üblicherweise werden die Schlussregeln so systematisiert, dass für jeden logischen Operator (Junktor bzw. Quantor) eine Einführungs- und eine Beseitigungsregel angegeben ist. Die Einführungsregel für einen Operator O erlaubt es, zu einer Aussage mit O als Hauptoperator überzugehen; die Beseitigungsregel führt von einer Aussage mit O als Hauptoperator zu einer anderen Aussage. Aufgrund der Natürlichkeit des Schließens und der Systematisierung in Einführungs- und Beseitigungsregeln lässt sich mit einem KdnS der Anspruch einer „beweistheoretischen Semantik“ verbinden, welche die Bedeutung der logischen Operatoren durch die Angabe von Schlussregeln festlegen will. (de) La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostraciones matemáticas. En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas de inferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla. Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada.Sirve para demostrar la validez de un argumento. La deducción natural fue introducida por Gerhard Gentzen en su trabajo Investigaciones sobre la inferencia lógica (Untersuchungen über das logische Schliessen), publicado en 1934-1935. (es) En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons : * contrairement aux systèmes à la Hilbert fondés sur des listes d'axiomes logiques plus ou moins ad hoc, la déduction naturelle repose sur un principe systématique de symétrie : pour chaque connecteur, on donne une paire de règles duales (introduction/élimination) ; * elle a conduit Gentzen à inventer un autre formalisme très important en théorie de la démonstration, encore plus « symétrique » : le calcul des séquents ; * elle a permis dans les années 1960 d'identifier la première instance de l'isomorphisme de Curry-Howard. La terminologie « déduction naturelle » a été suggérée, par Gentzen, eu égard à l'aspect peu intuitif des systèmes à la Hilbert. (fr) In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning. (en) 自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。 (ja) 논리학 및 증명이론에서 자연 연역(自然演繹, natural deduction)이란 자연스러운 논리적 추론을 나타내는 증명 연산의 일종으로, 최대한 공리를 배제하고 오직 구문적인 추론 규칙만을 사용한 증명이 이루어지는 것이 특징이다. 이는, 추론규칙의 논리적 법칙을 표현하기 위해 많은 공리들을 이용하는 힐베르트 체계와는 대조된다. (ko) Natuurlijke deductie is een methode om via deductie met noodzakelijkheid de geldigheid van een redenering conform vastgestelde regels te bewijzen in de logica. Het model zou gebaseerd zijn op een "natuurlijke" vorm van redeneren. Systemen van natuurlijke deductie zijn ontwikkeld voor verschillende vormen van logica, waaronder de propositielogica en de predicaatlogica. (nl) Dedukcja naturalna – bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazujący na systemach Hilberta. Dowód to lista formuł objętych oknami. Operacje w bardzo prostej wersji to: * dodanie założenia, otwiera to okno, * przepisanie dowolnego aktywnego założenia, * zamknięcie okna, dodaje się za oknem formułę „pierwsza formuła okna ostatnia formuła okna”, wszystkie formuły w oknie są dezaktywowane, * użycie jednej z reguł dowodzenia (w szczególności modus ponens na dowolnych aktywnych) na dowolnych aktywnych formułach. Każda formuła leżąca poza oknem, zwykle powstała w wyniku zamknięcia ostatniego okna, jest twierdzeniem. Okna są wyłącznie graficzną reprezentacją tego co się dzieje. (pl) La deduzione naturale è, nel campo della logica, un sistema deduttivo. Un sistema deduttivo è una relazione che può sussistere tra un insieme di formule e una formula: se la relazione vale, diciamo che la formula viene dedotta dall'insieme. La deduzione naturale si propone quindi come un metodo per dimostrare che un'affermazione è conseguenza di certe ipotesi. A differenza dei sistemi assiomatici è un sistema senza assiomi, basato su una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi. (it) Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen.Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma linguística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais económica, a lógica. Na notação formal utilizamos conectivos lógicos, operadores que realizam a ligação entre os átomos (os menores objetos). São eles: * - Negação (não é um conectivo, simplesmente nega a fórmula ou átomo ligado) * - Conjunção * - Disjunção * - Implicação * - Bi-implicação No caso da lógica clássica de primeira ordem, temos ainda os quantificadores: * - Universal * - Existencial Também utilizamos alguns símbolos extras para auxiliar: * - Derivação * - Consequência semântica * - Top (Verdade) * - Bottom (Absurdo, falsidade) (pt) 在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。 (zh) |
| dbo:thumbnail | wiki-commons:Special:FilePath/First_order_natural_deduction.png?width=300 |
| dbo:wikiPageExternalLink | https://web.archive.org/web/20160704202340/http:/www.cs.man.ac.uk/~pt/stable/Proofs+Types.html http://teachinglogic.univ-grenoble-alpes.fr/DN1/ http://www.danielclemente.com/logica/dn.en.pdf http://www.winterdrache.de/freeware/domino/ http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html https://archive.org/details/naturaldeduction0000praw%7Curl-access=registration%7Cseries=Acta http://www-2.cs.cmu.edu/~fp/papers/mscs00.pdf https://www.era.lib.ed.ac.uk/bitstream/handle/1842/407/ECS-LFCS-94-308.PDF%3Fsequence=2&isAllowed=y http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf https://www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf http://gdz.sub.uni-goettingen.de/dms/resolveppn/%3FPPN=GDZPPN002375508 http://gdz.sub.uni-goettingen.de/dms/resolveppn/%3FPPN=GDZPPN002375605%7Cdoi=10.1007/bf01201363%7Cs2cid=186239837 |
| dbo:wikiPageID | 51072 (xsd:integer) |
| dbo:wikiPageLength | 53209 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1110260943 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Predicate_logic dbr:Principia_Mathematica dbr:Modal_logic dbr:Model_theory dbr:Bertrand_Russell dbr:David_Hilbert dbr:Deductive_reasoning dbr:Argument_map dbr:Patrick_Suppes dbr:Per_Martin-Löf dbr:Dag_Prawitz dbr:University_of_Göttingen dbr:Decidability_(logic) dbr:Intensional_type_theory dbr:Intuitionistic_logic dbr:Analytic_tableau dbr:Universal_quantifier dbr:Jan_Lukasiewicz dbr:Computer-assisted_proof dbc:Methods_of_proof dbc:Proof_theory dbr:Mathematical_induction dbr:Mathematical_logic dbr:Normal_form_(abstract_rewriting) dbr:Normalization_property_(abstract_rewriting) dbr:Structural_rule dbr:Gerhard_Gentzen dbr:Gottlob_Frege dbr:Linear_logic dbr:Logic dbr:Calculus_of_constructions dbc:Logical_calculi dbr:Stephen_Cole_Kleene dbr:Function_type dbr:Henk_Barendregt dbr:John_Lemmon dbr:Parametric_polymorphism dbr:Proposition dbr:Type_theory dbr:Disjunction_elimination dbr:Countable dbr:Lambda-mu_calculus dbr:Lambda_cube dbr:Logical_reasoning dbr:System_L dbr:Alfred_North_Whitehead dbr:First-order_logic dbr:Number_theory dbr:Judgment_(mathematical_logic) dbr:Logical_connective dbr:Logical_framework dbr:Predicate_(mathematical_logic) dbr:Proof_theory dbr:Quantifier_(logic) dbr:Hilbert_system dbr:Atomic_formula dbr:Temporal_logic dbr:Term_(logic) dbr:Hybrid_logic dbr:Hypersequent dbr:Fitch-style_calculus dbr:Arend_Heyting dbc:Deductive_reasoning dbr:LF_(logical_framework) dbr:LISP dbr:Lambda_calculus dbr:Higher-order_logic dbr:Term_algebra dbr:Theory_(mathematical_logic) dbr:Axiom dbr:Classical_logic dbr:Meta-theorem dbr:Second-order_logic dbr:Proof_calculus dbr:Sequent_calculus dbr:Sequent dbr:Turnstile_(symbol) dbr:Implication_introduction dbr:Extensional_type_theory dbr:Impredicative_polymorphism dbr:Programming_language dbr:S5_(modal_logic) dbr:Stanisław_Jaśkowski dbr:Nordic_Journal_of_Philosophical_Logic dbr:Product_type dbr:S4_(modal_logic) dbr:Substructural_logic dbr:Display_logic dbr:Callcc dbr:Inference_rule dbr:Inference_rules dbr:Curry–Howard_isomorphism dbr:Cut_elimination dbr:Cut_elimination_theorem dbr:Dependent_type_theory dbr:Excluded_middle dbr:Existential_quantifier dbr:Hilbert-style_system dbr:Predicative_polymorphism dbr:File:First_order_natural_deduction.png dbr:First_class_control dbr:Labelled_deduction dbr:Michel_Parigot |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Cite_journal dbt:Cite_web dbt:Columns-list dbt:Harvtxt dbt:Main dbt:Portal dbt:Quote dbt:Reflist dbt:Mathematical_logic dbt:Foundations-footer |
| dcterms:subject | dbc:Methods_of_proof dbc:Proof_theory dbc:Logical_calculi dbc:Deductive_reasoning |
| gold:hypernym | dbr:Kind |
| rdf:type | yago:WikicatMethodsOfProof yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:Method105660268 yago:PsychologicalFeature100023100 |
| rdfs:comment | In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning. (en) 自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。 (ja) 논리학 및 증명이론에서 자연 연역(自然演繹, natural deduction)이란 자연스러운 논리적 추론을 나타내는 증명 연산의 일종으로, 최대한 공리를 배제하고 오직 구문적인 추론 규칙만을 사용한 증명이 이루어지는 것이 특징이다. 이는, 추론규칙의 논리적 법칙을 표현하기 위해 많은 공리들을 이용하는 힐베르트 체계와는 대조된다. (ko) Natuurlijke deductie is een methode om via deductie met noodzakelijkheid de geldigheid van een redenering conform vastgestelde regels te bewijzen in de logica. Het model zou gebaseerd zijn op een "natuurlijke" vorm van redeneren. Systemen van natuurlijke deductie zijn ontwikkeld voor verschillende vormen van logica, waaronder de propositielogica en de predicaatlogica. (nl) La deduzione naturale è, nel campo della logica, un sistema deduttivo. Un sistema deduttivo è una relazione che può sussistere tra un insieme di formule e una formula: se la relazione vale, diciamo che la formula viene dedotta dall'insieme. La deduzione naturale si propone quindi come un metodo per dimostrare che un'affermazione è conseguenza di certe ipotesi. A differenza dei sistemi assiomatici è un sistema senza assiomi, basato su una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi. (it) 在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。 (zh) Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen und philosophischen Logik einen Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski – einem Vertreter der Lemberg-Warschau-Schule – entwickelt wurde. Der Begriff des Kalküls des natürlichen Schließens (KdnS) ist nicht streng definiert, stattdessen gibt es eine Reihe von Merkmalen, die auf KdnS in unterschiedlichem Maße zutreffen und dabei bestimmen, wie typisch das Exemplar für die Gattung ist. (de) La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostraciones matemáticas. En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas de inferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla. Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada.Sirve para demostrar la validez de un argumento. (es) En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons : La terminologie « déduction naturelle » a été suggérée, par Gentzen, eu égard à l'aspect peu intuitif des systèmes à la Hilbert. (fr) Dedukcja naturalna – bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazujący na systemach Hilberta. Dowód to lista formuł objętych oknami. Operacje w bardzo prostej wersji to: * dodanie założenia, otwiera to okno, * przepisanie dowolnego aktywnego założenia, * zamknięcie okna, dodaje się za oknem formułę „pierwsza formuła okna ostatnia formuła okna”, wszystkie formuły w oknie są dezaktywowane, * użycie jednej z reguł dowodzenia (w szczególności modus ponens na dowolnych aktywnych) na dowolnych aktywnych formułach. (pl) Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen.Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma linguística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais económica, a lógica. * - Universal * - Existencial (pt) |
| rdfs:label | Systeme natürlichen Schließens (de) Deducción natural (es) Déduction naturelle (fr) Deduzione naturale (it) 자연 연역 (ko) Natural deduction (en) Natuurlijke deductie (nl) 自然演繹 (ja) Dedukcja naturalna (pl) Dedução natural (pt) 自然演绎 (zh) |
| owl:sameAs | freebase:Natural deduction wikidata:Natural deduction dbpedia-de:Natural deduction dbpedia-es:Natural deduction dbpedia-fi:Natural deduction dbpedia-fr:Natural deduction dbpedia-it:Natural deduction dbpedia-ja:Natural deduction dbpedia-ko:Natural deduction dbpedia-nl:Natural deduction dbpedia-no:Natural deduction dbpedia-pl:Natural deduction dbpedia-pt:Natural deduction dbpedia-simple:Natural deduction dbpedia-zh:Natural deduction https://global.dbpedia.org/id/Z2sV yago-res:Natural deduction |
| prov:wasDerivedFrom | wikipedia-en:Natural_deduction?oldid=1110260943&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/First_order_natural_deduction.png |
| foaf:isPrimaryTopicOf | wikipedia-en:Natural_deduction |
| is dbo:wikiPageDisambiguates of | dbr:Deduction |
| is dbo:wikiPageRedirects of | dbr:Elimination_rule dbr:Introduction_rule dbr:Natural_deduction_calculus dbr:Natural_deduction_logic dbr:Natural_deduction_system dbr:Natural_deductive_logic |
| is dbo:wikiPageWikiLink of | dbr:Proof_assistant dbr:Proof_net dbr:Propositional_calculus dbr:Quantum_logic dbr:List_of_functional_programming_topics dbr:MINLOG dbr:Monotonicity_of_entailment dbr:Deductive_reasoning dbr:Argument_map dbr:Richard_Sylvan dbr:Curry's_paradox dbr:Dag_Prawitz dbr:Deduction_theorem dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(I–Q) dbr:Inductivism dbr:Intuition dbr:Ivan_Orlov_(philosopher) dbr:Elimination_rule dbr:List_of_multiple_discoveries dbr:Minority_influence dbr:Universal_instantiation dbr:Propositional_proof_system dbr:Structural_proof_theory dbr:Timeline_of_Polish_science_and_technology dbr:Mathematical_logic dbr:Geometric_logic dbr:Negation dbr:Normal_form_(natural_deduction) dbr:Epigram_(programming_language) dbr:Gerhard_Gentzen dbr:Proof-theoretic_semantics dbr:Andrzej_Trybulec dbr:Logic dbr:Simply_typed_lambda_calculus dbr:Combinatory_categorial_grammar dbr:Computability_logic dbr:Deduction dbr:Programming_language_theory dbr:Type_theory dbr:Gödel's_completeness_theorem dbr:Jape_(software) dbr:Lambda-mu_calculus dbr:Laws_of_Form dbr:Logic:_The_Laws_of_Truth dbr:Logic_alphabet dbr:Minimal_logic dbr:System_L dbr:Paraconsistent_logic dbr:Curry–Howard_correspondence dbr:First-order_logic dbr:Diagrammatic_reasoning dbr:Formal_proof dbr:Grammatical_Framework dbr:History_of_logic dbr:History_of_type_theory dbr:Judgment_(mathematical_logic) dbr:Proof_by_contradiction dbr:Predicate_functor_logic dbr:Proof_procedure dbr:Proof_theory dbr:Relevance_logic dbr:Hilbert_system dbr:Lambda_calculus dbr:Lance_Rips dbr:Theory_(mathematical_logic) dbr:Planner_(programming_language) dbr:Frege_system dbr:Typing_rule dbr:Inductive_type dbr:Mercedes_Richards dbr:Metamath dbr:New_Math dbr:Second-order_logic dbr:Proof_calculus dbr:Sequent_calculus dbr:Rule_of_inference dbr:Sequent dbr:Stanisław_Jaśkowski dbr:Evert_Willem_Beth dbr:Fitch_notation dbr:Set-theoretic_definition_of_natural_numbers dbr:Introduction_rule dbr:Outline_of_software_engineering dbr:The_Poisoned_Chocolates_Case dbr:Natural_deduction_calculus dbr:Natural_deduction_logic dbr:Natural_deduction_system dbr:Natural_deductive_logic |
| is foaf:primaryTopic of | wikipedia-en:Natural_deduction |
