Teorema Deduksi - Interpretasi
Dalam buku "Tur melalui logika matematika" - oleh Robert S. Wolf, teorema deduksi ditentukan sebagai berikut:
Jika T $\cup$ {P} $\vdash$ Q, lalu T $\vdash$ (P. $\to$ Q)
Dimana T adalah teori orde pertama dan P & Q adalah beberapa rumus, dalam bahasa teori orde pertama ini. Lalu, apakah interpretasi berikut, dari teorema deduksi, benar?
Jika Q dapat diturunkan / dapat dibuktikan dari T $\cup$ {P}, maka dapat dikatakan bahwa - jika P diturunkan dari T (yaitu P adalah teorema dari T) maka Q juga dapat diturunkan dari T.
Juga, apakah interpretasi ini menangkap esensi dari teorema deduksi?
PS: pertanyaan lain berjudul Teorema Deduksi - Intuisi , tampaknya berfokus terutama pada aspek sintaksis dari teorema dan predikat kalkulus secara umum - daripada pada semantiknya.
Jawaban
apakah interpretasi berikut, dari teorema deduksi, benar?
Tidak. Apa yang Anda tulis
Jika $T \cup \{P\} \vdash Q$, lalu jika $T \vdash P$, kemudian $T \vdash Q$.
Ini sama dengan mengatakan
(1) Jika $T \cup \{P\} \vdash Q$, kemudian $T \nvdash P$ atau $T \vdash Q$.
Tapi ini tidak sama dengan
(2) Jika $T \cup \{P\} \vdash Q$, kemudian $T \vdash P \to Q$.
Mungkin itu masalahnya $P$ tidak dapat dibuktikan, tetapi $P \to Q$tidak juga. Kemudian "$T \nvdash P$ atau $T \vdash Q$"memegang, tapi"$T \vdash P \to Q$"tidak. Jadi (1) $\not \Rightarrow$ (2).
Inilah yang dimaksud dalam komentar dengan "trivialization": "if $T \vdash P$ kemudian $T \vdash Q$"(= apa yang Anda tulis) menjadi benar sepele jika $T \nvdash P$, yaitu jika $P$tidak dapat dibuktikan. Tapi "$T \vdash P \to Q$"(= apa yang dinyatakan oleh teorema deduksi) tidak: Hanya karena kita tidak dapat membuktikan $P$ bukan berarti kita bisa membuktikan $P\to Q$- seperti yang Anda amati. Oleh karena itu mengapa "$T \vdash P \to Q$"adalah klaim yang lebih kuat bahwa" Jika $T \vdash P$ kemudian $T \vdash Q$".
Inti dari teorema deduksi adalah bahwa Anda dapat "membalik-balik" antara memiliki teorema yang bergantung pada asumsi terbuka dan membuktikan pernyataan bersyarat:
Jika ada bukti$Q$ yang masih bergantung pada asumsi $P$, maka akan ada bukti dalam teori pernyataan tersebut $P \to Q$. Ini adalah efek langsung dari teknik bukti bersyarat (lihat hlm. 14).
Dan untuk arah sebaliknya dari teorema deduksi, jika Anda bisa membuktikannya$P \to Q$, maka Anda akan bisa membuktikannya $Q$ dengan asumsi itu $P$. Ini adalah konsekuensi dari aturan modus ponens inferensi (lihat hlm. 13).
Gabungan dua arah, teorema deduksi hanya membenarkan apa yang kami maksud dengan memiliki bukti "$\to$".
Anda sepenuhnya benar dalam menunjukkan bahwa gagasan sentral dari sistem formal adalah bukti daripada kebenaran. Namun perlu diingat bahwa kami biasanya tertarik untuk merancang sistem pembuktian yang "berguna" yang "sejalan" dengan gagasan tentang kebenaran: Pernyataan harus dapat dibuktikan dalam suatu teori persis ketika pernyataan itu benar di semua model teori . Bagaimanapun, inti dari sistem pembuktian adalah memiliki perangkat mekanis untuk secara ketat membuktikan pernyataan yang kami anggap benar. Jadi sementara pengertian pembuktian$\to$ dirumuskan dalam istilah aturan inferensi, cara aturan ini digunakan mencerminkan tabel kebenaran $\to$: Sebuah sistem bukti harus (dan sebagai untuk sistem bukti yang disajikan dalam buku Wolf, adalah) suara wrt semantik: Apa yang dapat dibuktikan benar (sesuai dengan definisi tabel kebenaran) di semua struktur; sistem (mudah-mudahan) tidak membuktikan omong kosong acak.