Catatan Kelas: Teori Pembuktian Minggu 4 - Eliminasi Cut

Dalam Teori Pembuktian, Eliminasi Cut (Cut-Elimination) adalah hasil fundamental oleh Gerhard Gentzen (1934). Teorema ini menyatakan bahwa setiap pembuktian dalam sequent calculus LK dapat ditransformasi menjadi pembuktian tanpa cut.

Apa itu Cut?

Cut adalah aturan inferensi yang memungkinkan kita "menghubungkan" dua sub-pembuktian:

Secara intuitif: jika $A$ dapat diturunkan dari $\Gamma$, dan dari $A$ kita dapat menurunkan konsekuen $\Lambda$, maka kita dapat "memotong" $A$.

Mengapa Eliminasi Cut Penting?

1. Subformula Property

Pembuktian tanpa cut memiliki subformula property: setiap formula dalam pembuktian adalah subformula dari formula-formula dalam end-sequent.

Ini memungkinkan pencarian pembuktian yang sistematis dan terbatas.

2. Konsistensi

Gentzen menggunakan eliminasi cut untuk membuktikan konsistensi aritmatika PA (Peano Arithmetic). Strateginya:

• Transforms setiap pembuktian PA ke sequent calculus
• Eliminasi semua cut
• Analisis "ordinal" dari pembuktian hasil
• Bukti bahwa tidak mungkin ada pembuktian untuk $\bot$

3. Analisis Pembuktian

Pembuktian tanpa cut lebih "analitik"—mereka menunjukkan bagaimana konklusi dibangun dari premis, bukan menggunakan "lem" (formula intermediate) yang arbitrer.

Proses Eliminasi Cut

Eliminasi cut dilakukan melalui serangkaian reduksi:

1. Cut Reduction pada Aturan Struktural: Kontraksi dan Weakening di dekat cut dapat dihilangkan

2. Cut Reduction pada Aturan Logis: Ketika cut bertemu aturan intro pada sisi kiri/kanan, kita "mendorong" cut ke atas

3. Grade Reduction: Untuk cut kompleks, kita kurangi kompleksitas formula cut

Contoh: Cut dengan $\land$-Left

Latihan

Soal: Transform pembuktian berikut menjadi bentuk tanpa cut:

Penyelesaian: Ini adalah contoh trivial—cut di sini menghubungkan pembuktian yang hanya menggunakan aturan struktural. Eliminasi cut pada kasus ini langsung menghilangkan cut karena formula yang dipotong ($A$) sudah ada di premis.

Hasil: $\frac{A \vdash A}{A, B \vdash A, B}$ melalui Weakening kiri dan kanan.

Catatan ini diperbarui mingguan di kelas Teori Pembuktian Intuisionistik ID.