Eliminasi-Potong (Cut-Elimination)

Eliminasi-potong adalah teorema Gentzen bahwa aturan potong (cut rule), yang memformalkan penggunaan lemma, dapat dihilangkan dari setiap bukti kalkulus sekuen, menyisakan bukti yang hanya dibangun dari formula-formula yang relevan.

Definition

Eliminasi-potong adalah teorema dan prosedur konstruktif yang menunjukkan bahwa setiap penurunan kalkulus sekuen yang menggunakan aturan potong dapat diubah menjadi penurunan yang tidak menggunakannya, sehingga setiap sekuen yang dapat dibuktikan memiliki bukti di mana hanya subformula dari sekuen akhir yang muncul.

Scope

Topik ini mencakup aturan potong dan perannya dalam kalkulus sekuen, prosedur eliminasi-potong dan terminasinya, sifat subformula dari bukti bebas-potong, konsekuensi konsistensi dan keterdecidabilitas yang dihasilkan, serta batasan ukuran bukti yang dapat ditimbulkan oleh eliminasi.

Core questions

• Apa yang diungkapkan oleh aturan potong dan mengapa penghapusannya signifikan?
• Bagaimana prosedur eliminasi-potong berakhir (terminate)?
• Apa itu sifat subformula dan apa implikasinya untuk pencarian bukti?
• Berapa biaya komputasi untuk mengeliminasi potongan?

Key theories

Gentzen Hauptsatz

Teorema utama Gentzen menyatakan bahwa aturan potong dapat diterima dalam kalkulus sekuen, sehingga setiap bukti yang menggunakan potongan dapat diubah menjadi bukti bebas-potong dari sekuen akhir yang sama.

Sifat subformula

Setiap formula yang muncul dalam bukti bebas-potong adalah subformula dari sekuen akhir, yang membatasi bentuk bukti dan mendasari prosedur keputusan serta argumen konsistensi.

Konsistensi melalui eliminasi-potong

Karena bukti bebas-potong dari sekuen kosong tidak mungkin, eliminasi-potong menghasilkan bukti langsung bahwa kalkulus, dan karenanya teori yang diformalkannya, adalah konsisten.

Clinical relevance

Eliminasi-potong adalah hasil fundamental dengan konsekuensi luas: menghasilkan bukti konsistensi, sifat subformula yang esensial untuk pembuktian teorema otomatis dan metode tableau, teorema interpolasi, dan, melalui korespondensi bukti-sebagai-program, normalisasi program berjenis (typed programs).

History

Gentzen membuktikan eliminasi-potong, Hauptsatz-nya, pada tahun 1934 untuk logika orde pertama, dan metode ini menjadi landasan teori bukti struktural. Tait dan Girard memperluas teknik ini ke sistem yang lebih kuat dan logika orde tinggi, dan batasan pertumbuhan ukuran bukti di bawah eliminasi-potong menjadi subjek studi tersendiri.

Key figures

• Gerhard Gentzen
• William Tait
• Jean-Yves Girard
• Gaisi Takeuti

Seminal works

• takeuti1987
• troelstra2000
• negri2001

Frequently asked questions

Apa itu potongan (cut) dalam sebuah bukti?

Aturan potong memungkinkan seseorang untuk membuktikan sebuah lemma dan kemudian menggunakannya: dari penurunan yang menetapkan sebuah formula dan penurunan lain yang menggunakan formula tersebut sebagai premis, aturan ini menyimpulkan hasil gabungan. Eliminasi-potong menunjukkan bahwa lemma perantara semacam itu pada prinsipnya selalu dapat dihilangkan.

Mengapa eliminasi potongan dapat membuat bukti menjadi jauh lebih panjang?

Menghilangkan sebuah potongan mungkin memerlukan duplikasi bagian besar dari penurunan, dan pengulangan ini dapat memperbesar ukuran bukti secara eksponensial. Jadi, bukti bebas-potong secara konseptual lebih sederhana tetapi bisa jauh lebih besar daripada bukti asli dengan potongan.