Deduksi Alami: Aturan Inferensi untuk Logika Proposisional

Natural Deduction adalah sistem pembuktian formal yang dikembangkan oleh Gerhard Gentzen (1934) dan secara independen oleh Stanisław Jaśkowski. Sistem ini meniru cara matematikawan melakukan pembuktian: menggunakan asumsi sementara dan mengeluarkannya ketika tidak lagi diperlukan.

Struktur Dasar

Dalam natural deduction, setiap connective logika memiliki dua jenis aturan:

1. Introduction rule - bagaimana membuktikan formula dengan connective tersebut
2. Elimination rule - bagaimana menggunakan formula dengan connective tersebut

Konjungsi ($\land$)

Introduction ($\land$I)

Dari $A$ dan $B$, kita dapat menyimpulkan $A \land B$.

Elimination ($\land$E)

Dari $A \land B$, kita dapat menyimpulkan $A$ atau $B$.

Implikasi ($\to$)

Introduction ($\to$I)

  [A]¹
   ⋮
   B
───── (→I)¹
A → B

Untuk membuktikan $A \to B$, asumsikan $A$ dan turunkan $B$.

Elimination (Modus Ponens, $\to$E)

Disjungsi ($\lor$)

Introduction ($\lor$I)

Elimination ($\lor$E)

  A ∨ B   [A]¹   [B]²
           ⋮      ⋮
           C      C
───────────────────── (∨E)¹,²
           C

Negasi dan $\bot$

Dalam logika intuitionistic:

• $\neg A$ didefinisikan sebagai $A \to \bot$
• Reductio ad absurdum (RAA): $\frac{[A] \quad \bot}{\neg A}$

Contoh Pembuktian

Buktikan $A \to A$:

1. [A]        Assumption
2. A          Reiteration (1)
────────────── (→I)1
3. A → A

Buktikan $A \land B \to B \land A$:

1. [A ∧ B]           Assumption
2. B                 (∧E) 1
3. A                 (∧E) 1
4. B ∧ A             (∧I) 2, 3
───────────────────── (→I)1
5. (A ∧ B) → (B ∧ A)

Catatan ini adalah bagian dari seri Logika dan Pembuktian oleh Intuisionistik ID.