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.
Dalam logika dan teori bukti, deduksi natural adalah sejenis kalkulus bukti di mana penalaran logis diekspresikan melalui aturan inferensi yang sangat terkait dengan cara penalaran yang "alami".
This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.
Hal ini berbeda dengan sistem gaya Hilbert, yang sebaliknya menggunakan aksioma sebanyak mungkin untuk mengekspresikan hukum logika dari penalaran deduktif.
Natural deduction grew out of a context of dissatisfaction with the axiomatizations of deductive reasoning common to the systems of Hilbert, Frege, and Russell (see, e.g., Hilbert system).
Deduksi natural muncul dari ketidakpuasan terhadap aksiomatisasi penalaran deduktif yang umum digunakan dalam sistem Hilbert, Frege, dan Russell (lihat, misalnya, sistem Hilbert).
Such axiomatizations were most famously used by Russell and Whitehead in their mathematical treatise Principia Mathematica.
Aksiomatisasi semacam ini paling terkenal digunakan oleh Russell dan Whitehead dalam karya matematika mereka Principia Mathematica.
Spurred on by a series of seminars in Poland in 1926 by Łukasiewicz that advocated a more natural treatment of logic, Jaśkowski made the earliest attempts at defining a more natural deduction, first in 1929 using a diagrammatic notation, and later updating his proposal in a sequence of papers in 1934 and 1935.
Terinspirasi oleh serangkaian seminar di Polandia pada tahun 1926 oleh Łukasiewicz yang menganjurkan pendekatan logika yang lebih “alami”, Jaśkowski melakukan upaya awal untuk mendefinisikan deduksi natural yang lebih alami, pertama pada tahun 1929 menggunakan notasi diagramatik, dan kemudian memperbarui usulannya dalam serangkaian makalah pada tahun 1934 dan 1935.
His proposals led to different notations such as Fitch notation or Suppes' method, for which Lemmon gave a variant now known as Suppes–Lemmon notation.
Usulannya menghasilkan berbagai notasi berbeda, seperti notasi Fitch atau metode Suppes, yang kemudian Lemmon kembangkan menjadi varian yang sekarang dikenal sebagai notasi Suppes–Lemmon.
Natural deduction in its modern form was independently proposed by the German mathematician Gerhard Gentzen in 1933, in a dissertation delivered to the faculty of mathematical sciences of the University of Göttingen.
Deduksi natural dalam bentuk modernnya diajukan secara independen oleh matematikawan Jerman Gerhard Gentzen pada tahun 1933, dalam sebuah disertasi yang disampaikan kepada fakultas ilmu matematika Universitas Göttingen.
Gentzen was motivated by a desire to establish the consistency of number theory.
Gentzen terdorong oleh keinginan untuk membuktikan konsistensi teori bilangan.
He was unable to prove the main result required for the consistency result, the cut elimination theorem—the Hauptsatz—directly for natural deduction.
Ia tidak mampu membuktikan hasil utama yang diperlukan untuk konsistensi tersebut, yaitu teorema eliminasi potong (cut elimination theorem atau Hauptsatz), secara langsung untuk deduksi natural.
For this reason he introduced his alternative system, the sequent calculus, for which he proved the Hauptsatz both for classical and intuitionistic logic.
Karena itu ia memperkenalkan sistem alternatifnya, yaitu kalkulus sekuen, untuk mana ia membuktikan Hauptsatz baik untuk logika klasik maupun intuisionistik.
His 1965 monograph Natural deduction: a proof-theoretical study was to become a reference work on natural deduction, and included applications for modal and second-order logic.
Monografnya tahun 1965, Natural deduction: a proof-theoretical study, menjadi karya referensi mengenai deduksi natural dan mencakup aplikasi untuk logika modal dan logika orde kedua.
In natural deduction, a proposition is deduced from a collection of premises by applying inference rules repeatedly.
Dalam deduksi natural, sebuah proposisi diturunkan dari sekumpulan premis dengan menerapkan aturan inferensi secara berulang.
The system presented in this article is a minor variation of Gentzen's or Prawitz's formulation, but with a closer adherence to Martin-Löf's description of logical judgments and connectives.
Sistem yang disajikan dalam artikel ini adalah variasi kecil dari formulasi Gentzen atau Prawitz, tetapi lebih dekat mengikuti deskripsi Martin-Löf mengenai penilaian logis dan konektor logika.