In logic, natural deduction is an approach to proof theory that attempts to provide a deductive system which is a formal model of logical reasoning as it "naturally" occurs. This approach is in contrast to axiomatic systems which use axioms.

PropertyValue
dbpprop:abstract
  • In logic, natural deduction is an approach to proof theory that attempts to provide a deductive system which is a formal model of logical reasoning as it "naturally" occurs. This approach is in contrast to axiomatic systems which use axioms.
  • Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen 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 Tableauxkalkül, Axiomatischer 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 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.
  • La déduction naturelle est un système formel proposé par Gerhard Gentzen en 1934 pour représenter les preuves en logique du premier ordre de manière aussi proche que possible des façons naturelles de raisonner. L'introduction de la déduction naturelle motivée par l'aspect peu canonique des systèmes à la Hilbert est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons : contrairement aux systèmes à la Hilbert basé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 : chaque connecteur est défini par 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, 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.
  • 自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。
  • 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 predikaatlogica.
  • Dedukcja naturalna to bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazowany 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 <math>\supset</math> 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. Oczywiście okna są wyłącznie graficzną reprezentacją tego co się dzieje.
  • Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Nos anos 30, foram introduzidos pela primeira vez, por Gentzen e Jaśkowski, os sistemas de Dedução Natural para a Lógica Clássica. As demonstrações realizadas no sistema de dedução natural seguem uma via sintática e utilizam árvores de derivação.
  • 在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。
dbpprop:hasPhotoCollection
dbpprop:portalProperty
  • Logic
  • Logical connectives Hasse diagram.svg
dbpprop:quoteProperty
  • Gentzen, Untersuchungen über das logische Schließen (Mathematische Zeitschrift 39, pp.176–210, 1935)
  • Ich wollte zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein „Kalkül des natürlichen Schließens“. (First I wished to construct a formalism that comes as close as possible to actual reasoning. Thus arose a "calculus of natural deduction".)
dbpprop:reference
dbpprop:wikiPageUsesTemplate
rdfs:comment
  • In logic, natural deduction is an approach to proof theory that attempts to provide a deductive system which is a formal model of logical reasoning as it "naturally" occurs. This approach is in contrast to axiomatic systems which use axioms.
  • Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen 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.
  • La déduction naturelle est un système formel proposé par Gerhard Gentzen en 1934 pour représenter les preuves en logique du premier ordre de manière aussi proche que possible des façons naturelles de raisonner.
  • 自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。
  • 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 predikaatlogica.
  • Dedukcja naturalna to bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazowany na systemach Hilberta. Dowód to lista formuł objętych oknami.
  • Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Nos anos 30, foram introduzidos pela primeira vez, por Gentzen e Jaśkowski, os sistemas de Dedução Natural para a Lógica Clássica. As demonstrações realizadas no sistema de dedução natural seguem uma via sintática e utilizam árvores de derivação.
  • 在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。
rdfs:label
  • Natural deduction
  • Systeme natürlichen Schließens
  • Déduction naturelle
  • 自然演繹
  • Natuurlijke deductie
  • Dedukcja naturalna
  • Dedução natural
  • 自然演绎
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of