Deduksi Alami dan Kalkulus Sekuen
Deduksi alami dan kalkulus sekuen adalah dua sistem formal bergaya Gentzen yang merepresentasikan bukti melalui aturan introduksi dan eliminasi untuk penghubung logis, membentuk mekanisme dasar teori bukti struktural.
Definition
Deduksi alami menurunkan formula dari asumsi menggunakan aturan introduksi dan eliminasi yang mencerminkan penalaran informal, sementara kalkulus sekuen memanipulasi sekuen, yaitu pernyataan bahwa daftar formula menyiratkan formula lain, melalui aturan yang bekerja di sisi kiri dan kanan suatu implikasi.
Scope
Topik ini mencakup aturan deduksi alami dengan pasangan introduksi dan eliminasinya, struktur kalkulus sekuen dengan aturan kiri dan kanannya serta aturan struktural, normalisasi untuk deduksi alami, hubungan antara kedua sistem, dan varian intuisionistik serta klasiknya.
Core questions
- Bagaimana aturan introduksi dan eliminasi memberikan makna pada penghubung logis?
- Apa itu sekuen dan bagaimana aturannya berbeda dari aturan deduksi alami?
- Bagaimana normalisasi menyederhanakan bukti deduksi alami?
- Bagaimana versi klasik dan intuisionistik dari kalkulus ini saling terkait?
Key theories
- Aturan introduksi dan eliminasi
- Setiap penghubung diatur oleh aturan yang memperkenalkannya dan aturan yang memanfaatkannya, dan harmoninya, bahwa eliminasi mengembalikan persis apa yang dimasukkan oleh introduksi, mengekspresikan makna penghubung tersebut.
- Teorema normalisasi
- Prawitz menunjukkan bahwa bukti deduksi alami dapat direduksi ke bentuk normal bebas dari jalan memutar di mana sebuah introduksi segera dibatalkan oleh sebuah eliminasi, analog deduksi alami dari eliminasi-potong.
- Korespondensi kedua kalkulus
- Deduksi alami dan kalkulus sekuen membuktikan teorema yang sama dan dapat diterjemahkan satu sama lain, dengan aturan kiri sekuen yang sesuai dengan aturan eliminasi deduksi alami.
Clinical relevance
Kalkulus ini adalah format standar untuk mempelajari bukti secara struktural: deduksi alami mendasari teori tipe dan asisten bukti melalui korespondensi bukti-sebagai-program, sementara kalkulus sekuen, dengan properti subformula setelah eliminasi-potong (cut-elimination), menjadi dasar pencarian bukti otomatis dan tableau analitik.
History
Gentzen memperkenalkan deduksi alami dan kalkulus sekuen pada tahun 1934 dan 1935, merancang kalkulus sekuen untuk mendapatkan teorema eliminasi-potongnya setelah menemukan deduksi alami lebih sulit dianalisis. Prawitz menghidupkan kembali deduksi alami pada tahun 1965 dengan studi normalisasi yang menyeluruh, dan sistem-sistem ini menjadi pusat perkembangan bukti-sebagai-program di kemudian hari.
Key figures
- Gerhard Gentzen
- Dag Prawitz
- Stanislaw Jaskowski
- Jan von Plato
Related topics
Seminal works
- troelstra2000
- prawitz1965
- negri2001
Frequently asked questions
- Apa perbedaan antara deduksi alami dan kalkulus sekuen?
- Deduksi alami bekerja dengan formula di bawah konteks asumsi dan menggunakan aturan eliminasi, sangat cocok dengan bukti informal. Kalkulus sekuen bekerja dengan implikasi eksplisit dan menggantikan aturan eliminasi dengan aturan introduksi-kiri, sebuah format yang membuat eliminasi-potong dan properti subformula menjadi transparan.
- Mengapa normalisasi penting?
- Bukti normal tidak mengandung jalan memutar dan memiliki properti subformula, sehingga setiap formula di dalamnya adalah subformula dari kesimpulan atau premis. Ini membatasi bentuk bukti, menghasilkan hasil konsistensi, dan, melalui korespondensi bukti-sebagai-program, sesuai dengan mengevaluasi program ke suatu nilai.