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".^[1] Hal ini berbeda dengan sistem gaya Hilbert, yang sebaliknya menggunakan aksioma sebanyak mungkin untuk mengekspresikan hukum logika dari penalaran deduktif.

Deduksi natural muncul dari ketidakpuasan terhadap aksiomatisasi penalaran deduktif yang umum digunakan dalam sistem Hilbert, Frege, dan Russell (lihat, misalnya, sistem Hilbert). Aksiomatisasi semacam ini paling terkenal digunakan oleh Russell dan Whitehead dalam karya matematika mereka Principia Mathematica. 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.^[2] Usulannya menghasilkan berbagai notasi berbeda, seperti notasi Fitch atau metode Suppes, yang kemudian Lemmon kembangkan menjadi varian yang sekarang dikenal sebagai notasi Suppes–Lemmon.

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.^[3] Istilah natural deduction (atau dalam bahasa Jermannya natürliches Schließen) dicetuskan dalam makalah tersebut:

Ich wollte nun 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".

Terjemahan:

Pertama, saya ingin membangun sebuah formalisme yang sedekat mungkin dengan penalaran yang sebenarnya. Dengan demikian muncul sebuah "kalkulus deduksi natural".

Gentzen terdorong oleh keinginan untuk membuktikan konsistensi teori bilangan. 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. Karena itu ia memperkenalkan sistem alternatifnya, yaitu kalkulus sekuen, untuk mana ia membuktikan Hauptsatz baik untuk logika klasik maupun intuisionistik. Dalam serangkaian seminar pada tahun 1961 dan 1962, Prawitz memberikan ringkasan komprehensif mengenai kalkulus deduksi natural, dan memindahkan banyak pekerjaan Gentzen dengan kalkulus sekuen ke dalam kerangka deduksi natural. 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.

Dalam deduksi natural, sebuah proposisi diturunkan dari sekumpulan premis dengan menerapkan aturan inferensi secara berulang. 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.^[4]