Menggunakan sepuluh kesimpulan dari Sistem Deduksi Alami membuktikan hukum DeMorgan .
Aturan Pengurangan Alam
Pendahuluan Negasi:
{(P → Q), (P → ¬Q)} ⊢ ¬P
Penghapusan Negasi:
{(¬P → Q), (¬P → ¬Q)} ⊢ P
Dan Pendahuluan:
{P, Q} ⊢ P ʌ Q
Dan Eliminasi:
P ʌ Q ⊢ {P, Q}
Atau Pendahuluan:
P ⊢ {(P ∨ Q),(Q ∨ P)}
Atau Eliminasi:
{(P ∨ Q), (P → R), (Q → R)} ⊢ R
Iff Pendahuluan:
{(P → Q), (Q → P)} ⊢ (P ≡ Q)
Penghapusan Iff:
(P ≡ Q) ⊢ {(P → Q), (Q → P)}
Jika Pendahuluan:
(P ⊢ Q) ⊢ (P → Q)
Jika Eliminasi:
{(P → Q), P} ⊢ Q
Struktur bukti
Setiap pernyataan dalam bukti Anda harus merupakan hasil dari satu dari sepuluh aturan yang diterapkan pada beberapa proposisi yang diturunkan sebelumnya (tidak ada logika sirkular) atau asumsi (dijelaskan di bawah). Setiap aturan beroperasi di beberapa proposisi di sebelah kiri⊢
(operator konsekuensi logis) dan membuat sejumlah proposisi dari sisi kanan. Pendahuluan Jika bekerja sedikit berbeda dari operator lainnya (dijelaskan secara rinci di bawah). Ini beroperasi di satu pernyataan yang merupakan konsekuensi logis dari yang lain.
Contoh 1
Anda memiliki pernyataan berikut:
{(P → R), Q}
Anda dapat menggunakan Dan Pendahuluan untuk membuat:
(P → R) ʌ Q
Contoh 2
Anda memiliki pernyataan berikut:
{(P → R), P}
Anda dapat menggunakan If Elimination untuk membuat:
R
Contoh 3
Anda memiliki pernyataan berikut:
(P ʌ Q)
Anda dapat menggunakan Dan Penghapusan untuk membuat:
P
atau untuk membuat:
Q
Propagasi Asumsi
Anda dapat, pada suatu saat, mengambil pernyataan yang Anda inginkan. Pernyataan apa pun yang berasal dari asumsi-asumsi ini akan "bergantung" padanya. Pernyataan juga akan bergantung pada asumsi yang diandalkan oleh pernyataan orang tua mereka. Satu-satunya cara untuk menghilangkan asumsi adalah dengan Jika Pendahuluan. Untuk Jika pengantar Anda mulai dengan Pernyataan Q
yang bergantung pada pernyataan P
dan diakhiri dengan (P → Q)
. Pernyataan baru bergantung pada setiap asumsi Q
bergantung kecuali asumsi P
. Pernyataan akhir Anda seharusnya tidak bergantung pada asumsi.
Spesifik dan pemberian skor
Anda akan membuat satu bukti untuk masing-masing dari dua undang-undang DeMorgan hanya dengan menggunakan 10 kesimpulan dari Natural Deduction Calculus.
Kedua aturan tersebut adalah:
¬(P ∨ Q) ≡ ¬P ʌ ¬Q
¬(P ʌ Q) ≡ ¬P ∨ ¬Q
Skor Anda adalah jumlah kesimpulan yang digunakan ditambah jumlah asumsi yang dibuat. Pernyataan akhir Anda tidak boleh bergantung pada asumsi apa pun (yaitu harus menjadi teorema).
Anda bebas memformat bukti sesuai keinginan Anda.
Anda dapat membawa Lemmas dari satu bukti ke yang lain tanpa biaya untuk mencetak gol.
Contoh Bukti
Saya akan buktikan itu (P and not(P)) implies Q
(Setiap poin-poin adalah +1 poin)
Menganggap
not (Q)
Menganggap
(P and not(P))
Menggunakan Dan Elim pada
(P and not(P))
turunan{P, not(P)}
Gunakan Dan Pendahuluan tentang
P
dannot(Q)
untuk mendapatkan(P and not(Q))
Gunakan Dan Elim pada pernyataan yang baru saja diturunkan untuk dibuat
P
P
Proposisi baru ini berbeda dari yang lain yang kita dapatkan sebelumnya. Yaitu itu bergantung pada asumsi not(Q)
dan (P and not(P))
. Padahal pernyataan aslinya hanya bergantung pada (P and not(P))
. Ini memungkinkan kita untuk melakukan:
Jika Pendahuluan tentang
P
pengantarnot(Q) implies P
(masih bergantung pada(P and not(P))
asumsi)Gunakan Dan Pendahuluan tentang
not(P)
dannot(Q)
(dari langkah 3) untuk diturunkan(not(P) and not(Q))
Gunakan Dan Elim pada pernyataan yang baru saja diturunkan untuk membuat
not(P)
(sekarang bergantung padanot(Q)
)Jika Pengantar tentang
not(P)
pengantar barunot(Q) implies not(P)
Kami sekarang akan menggunakan penghapusan negasi pada
not(Q) implies not(P)
dannot(Q) implies P
untuk mendapatkanQ
Ini Q
hanya bergantung pada asumsi (P and not(P))
sehingga kita bisa menyelesaikan buktinya
- Jika Pendahuluan terus
Q
diturunkan(P and not(P)) implies Q
Bukti ini skor total 11.
sumber
⊢
(simbol juga tidak membuat saya di ponsel).(P ⊢ (Q ⊢ R)) ⊢ (Q ⊢ (P ⊢ R))
(dalam hal ini,¬Q ⊢ ((P ʌ ¬P) ⊢ P)
untuk(P ʌ ¬P) ⊢ (¬Q ⊢ P)
digunakan).(assume (P/\~P); P,~P by and-elim; (assume ~Q; P by assumption; ~P by assumption); ~Q->P by impl-intro; ~Q->~P by impl-intro; Q by neg-elim); P/\~P->Q by impl-intro
untuk mendapatkan skor 9?Jawaban:
Nilai: 81
Setiap baris harus bernilai 1 poin. Hukum De Morgan ditemukan di pernyataan (3) dan (6). Label dalam tanda kurung menunjukkan pernyataan sebelumnya (s) garis tergantung pada jika mereka tidak segera mendahului.
sumber
Nilai: 59
Penjelasan
Saya akan menggunakan struktur seperti pohon sebagai buktinya karena saya menemukan gaya ini cukup mudah dibaca. Setiap baris dijelaskan oleh hitungan aturan yang digunakan, misalnya "Contoh 1" dalam tantangan akan direpresentasikan sebagai pohon ini (tumbuh dari bawah ke atas):
Perhatikan jumlah A, B yang tidak diketahui dan juga asumsi Γ - jadi ini bukan teorema. Untuk menunjukkan bagaimana membuktikan teorema, mari kita asumsikan A dan gunakan Atau-pengantar sebagai berikut:
Sekarang ini masih tergantung pada asumsi A tetapi kita dapat memperoleh teorema dengan menerapkan Jika-pengantar:
Jadi kami bisa mendapatkan teorema ⊢ A → ( A ∨ B ) dalam total 3 langkah (1 asumsi & 2 aturan yang diterapkan).
Dengan ini kita dapat terus membuktikan beberapa aturan baru yang membantu kita membuktikan Hukum DeMorgan.
Aturan tambahan
Mari kita pertama-tama menurunkan Prinsip Ledakan dan menunjukkannya dengan PE sebagai bukti lebih lanjut:
Dari sini kita mendapatkan bentuk lain dari itu: A ⊢ ¬ A → X - kita akan menyebutnya CPE :
Kita akan membutuhkan yang lain di mana istilah yang dinegasikan (¬) adalah asumsi dan menyebutnya sebagai CPE - :
Dari dua aturan yang baru saja diturunkan ( CPE dan CPE - ), kita dapat memperoleh aturan penting Negasi Ganda :
Hal selanjutnya yang harus dilakukan adalah membuktikan sesuatu seperti Modus Tollens - maka MT :
Lemma
Lemma A
Lemma A1
Kami membutuhkan aturan berikut dua kali:
Lemma A
Dengan meng-instantiating lemma yang baru saja terbukti dua kali kita dapat menunjukkan satu arah kesetaraan, kita akan membutuhkannya dalam bukti akhir:
Lemma B
Untuk menunjukkan arah lain, kita perlu melakukan dua kali beberapa hal yang cukup berulang (untuk kedua argumen A dan B di ( A ∨ B )) - ini berarti di sini saya mungkin bisa golf bukti lebih lanjut ..
Lemma B1 '
Lemma B1
Lemma B2 '
Lemma B2
Lemma B
Akhirnya kesimpulan dari B1 dan B2 :
Bukti aktual
Setelah kami membuktikan dua pernyataan ini:
Kita dapat membuktikan kesetaraan pertama (¬ ( A ∨ B ) ≡ ¬ A ʌ ¬ B )) sebagai berikut:
Dan dengan aturan yang terbukti bersama-sama dengan Iff-Elimination kita dapat membuktikan kesetaraan kedua juga:
Tidak yakin dengan skor - jika saya melakukannya dengan benar, beri tahu saya jika ada sesuatu yang salah.
Penjelasan
Sumber
Jika seseorang menginginkan sumber tex (perlu mathpartir ):
sumber
P
danQ
, Anda harus menghitung langkah-langkahnya secara terpisah dalam total akhir. (Dengan kata lain, sistem pembuktian tidak secara langsung memungkinkan pembuktian lemma "orde kedua" seperti "untuk semua proposisi A dan B,A/\B -> B/\A
" dan kemudian menggunakannya untuk membuktikan keduanyaP/\(Q/\R) -> (Q/\R)/\P
dan(P/\Q)/\R -> R/\(P/\Q)
.)Nilai: 65
Hukum de Morgan adalah garis 30 dan garis 65.
(Saya belum melakukan upaya khusus untuk bermain golf ini, misalnya untuk melihat apakah ada beberapa bukti berulang yang dapat disarikan pada awalnya.)
sumber