Deduksi alami (natural deduction) adalah salah satu metode formal dalam logika matematika yang dirancang untuk meniru cara manusia secara alami menyusun argumen logis. Tujuan dari deduksi alami adalah untuk menyediakan aturan-aturan inferensi yang memungkinkan kita menyimpulkan pernyataan logis baru dari pernyataan yang sudah diketahui dengan cara yang intuitif.

Deduksi alami dikembangkan pada awal abad ke-20 oleh logikawan Gerhard Gentzen dan Stanisław Jaśkowski. Metode ini terdiri dari aturan-aturan inferensi yang memandu bagaimana kita bisa menyimpulkan kebenaran suatu proposisi berdasarkan proposisi lain. Dua aturan inferensi utama dalam deduksi alami adalah:

1. Eliminasi (Elimination): Bagaimana kita bisa mengeliminasi konektor logika, seperti implikasi, disjungsi, atau konjungsi untuk menyimpulkan sesuatu.
2. Introduksi (Introduction): Bagaimana kita bisa memperkenalkan konektor logika ke dalam argumen (misalnya, mengintroduksi implikasi atau disjungsi).

Setiap aturan inferensi memperlakukan operator logika seperti dan (∧), atau (∨), tidak (¬), dan jika...maka... (→). Misalnya:

• Introduksi konjungsi (∧ Introduction): Jika kita tahu bahwa "A" benar dan "B" benar, maka kita dapat menyimpulkan "A ∧ B" (A dan B benar).
• Eliminasi implikasi (→ Elimination): Jika kita tahu "A → B" (jika A maka B) dan "A" benar, maka kita dapat menyimpulkan "B" benar.

Deduksi alami berbeda dari sistem lain seperti logika aksiomatik karena lebih fleksibel dan intuitif. Sistem ini banyak digunakan dalam berbagai cabang ilmu komputer, linguistik formal, dan logika filosofi karena menyerupai struktur argumentasi yang umum digunakan dalam penalaran manusia.

Sebelum mempelajari lebih jauh tentang deduksi alami, kita perlu menyimak Narasi Deduksi Alami dan mempelajari Aturan Dasar Deduksi Alami.