Buktikan hukum DeMorgan

21

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 Qyang bergantung pada pernyataan Pdan diakhiri dengan (P → Q). Pernyataan baru bergantung pada setiap asumsi Qbergantung 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 Pdan not(Q)untuk mendapatkan(P and not(Q))

  • Gunakan Dan Elim pada pernyataan yang baru saja diturunkan untuk dibuat P

PProposisi 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 Ppengantar not(Q) implies P(masih bergantung pada (P and not(P))asumsi)

  • Gunakan Dan Pendahuluan tentang not(P)dan not(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 pada not(Q))

  • Jika Pengantar tentang not(P)pengantar barunot(Q) implies not(P)

  • Kami sekarang akan menggunakan penghapusan negasi pada not(Q) implies not(P)dan not(Q) implies Puntuk mendapatkanQ

Ini Qhanya bergantung pada asumsi (P and not(P))sehingga kita bisa menyelesaikan buktinya

  • Jika Pendahuluan terus Qditurunkan(P and not(P)) implies Q

Bukti ini skor total 11.

Wisaya Gandum
sumber
7
Meskipun konsensus tentang meta jelas, tidak semua orang akan melihatnya, jadi ini hanya untuk menyoroti bahwa golf bukti ada di topik .
trichoplax
2
Saya pikir Anda harus menjelaskan struktur bukti dan (simbol juga tidak membuat saya di ponsel).
xnor
3
Saya pikir penjelasannya pasti membantu. Apa yang saya anggap paling berguna adalah contoh bukti sederhana yang berfungsi dan mencetak Jika-Pendahuluan dan asumsi-asumsi, lebih disukai bersarang. Mungkin kontrapositif?
xnor
1
Dalam contoh Anda, saya percaya bahwa dua asumsi pertama harus dibalik; tidak ada yang menyatakan bahwa (P ⊢ (Q ⊢ R)) ⊢ (Q ⊢ (P ⊢ R))(dalam hal ini, ¬Q ⊢ ((P ʌ ¬P) ⊢ P)untuk (P ʌ ¬P) ⊢ (¬Q ⊢ P)digunakan).
LegionMammal978
1
Apakah Anda diizinkan untuk membuktikan banyak hal dalam "konteks asumsi" tunggal, dan kemudian mengekstraksi beberapa pernyataan implikasi, untuk menghemat berapa banyak "garis asumsi" yang dibutuhkan? misalnya (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-intrountuk mendapatkan skor 9?
Daniel Schepler

Jawaban:

6

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.

(a) assume P {
    (aa) P ^ P
    (ab) P
    (ac) P v Q
} (a1) P -> P
  (a2) P -> P v Q
(1) assume ~P ^ ~Q {
    (1a) assume P v Q {
        (1aa) assume Q {
            (1aaa) assume ~P {
                (1aaaa) Q ^ Q [1aa]
                (1aaab) Q
                (1aaac) ~Q [1]
            } (1aaa1) ~P -> Q
              (1aaa2) ~P -> ~Q
            (1aab) P
        } (1aa1) Q -> P
        P [1a, a1, 1aa1]
        ~P [1]
    } (1a1) P v Q -> P
      (1a2) P v Q -> ~P
    (1b) ~(P v Q)
} (11) ~P ^ ~Q -> ~(P v Q)
(2) assume ~(P v Q) {
    (2a) ~(P v Q) ^ ~(P v Q)
    (2b) assume P {
        (2aa) ~(P v Q) [2a]
    } (2b1) P -> ~(P v Q)
    (2c) ~P [a2, 2b1]
    (2d) assume Q {
        (2da) ~(P v Q) [2a]
        (2db) P v Q
    } (2d1) Q -> ~(P v Q)
      (2d2) Q -> P v Q
    (2e) ~Q
    (2f) ~P ^ ~Q
} (21) ~(P v Q) -> ~P ^ ~Q
(3) ~(P v Q) == ~P ^ ~Q [11, 21]
(4) assume ~P v ~Q {
    (4a) assume ~P {
        (4aa) assume P ^ Q {
            (4aaa) P
            (4aab) ~P ^ ~P [4a]
            (4aac) ~P
        } (4aa1) P ^ Q -> P
          (4aa2) P ^ Q -> ~P
        (4ab) ~(P ^ Q)
    } (4a1) ~P -> ~(P ^ Q)
    (4b) assume ~Q {
        (4ba) assume P ^ Q {
            (4baa) Q
            (4bab) ~Q ^ ~Q [4b]
            (4bac) ~Q
        } (4ba1) P ^ Q -> Q
          (4ba2) P ^ Q -> ~Q
        (4bb) ~(P ^ Q)
    } (4b1) ~P -> ~(P ^ Q)
    (4c) ~(P ^ Q) [4, 4a1, 4b1]
} (41) ~P v ~Q -> ~(P ^ Q) 
(5) assume ~(P ^ Q) {
    (5a) assume ~(~P v ~Q) {
        (5aa) ~(~P v ~Q) ^ ~(P ^ Q) [5, 5a]
        (5ab) assume ~P {
            (5aba) ~P v ~Q
            (5abb) ~(~P v ~Q) [5aa]
        } (5ab1) ~P -> ~P v ~Q
          (5ab2) ~P -> ~(~P v ~Q)
        (5ac) P
        (5ad) assume ~Q {
            (5ada) ~P v ~Q
            (5adb) ~(~P v ~Q) [5aa]
        } (5ad1) ~Q -> ~P v ~Q
          (5ad2) ~Q -> ~(~P v ~Q)
        (5ae) Q
        (5af) P ^ Q [5ac, 5ae]
        (5ag) ~(P ^ Q) [5aa]
    } (5a1) ~(~P v ~Q) -> P ^ Q
      (5a2) ~(~P v ~Q) -> ~(P ^ Q)
    (5b) ~P v ~Q
} (51) ~(P ^ Q) -> ~P v ~Q
(6) ~(P ^ Q) == ~P v ~Q [41, 51]
feersum
sumber
4

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):

AIntro

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:

OIntro

Sekarang ini masih tergantung pada asumsi A tetapi kita dapat memperoleh teorema dengan menerapkan Jika-pengantar:

IIntro

Jadi kami bisa mendapatkan teorema ⊢ A → ( AB ) 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:

pe

Dari sini kita mendapatkan bentuk lain dari itu: A ⊢ ¬ AX - kita akan menyebutnya CPE :

pe

Kita akan membutuhkan yang lain di mana istilah yang dinegasikan (¬) adalah asumsi dan menyebutnya sebagai CPE - :

NCPE

Dari dua aturan yang baru saja diturunkan ( CPE dan CPE - ), kita dapat memperoleh aturan penting Negasi Ganda :

DN

Hal selanjutnya yang harus dilakukan adalah membuktikan sesuatu seperti Modus Tollens - maka MT :

MT

Lemma

Lemma A

Lemma A1

Kami membutuhkan aturan berikut dua kali:

LA1

Lemma A

Dengan meng-instantiating lemma yang baru saja terbukti dua kali kita dapat menunjukkan satu arah kesetaraan, kita akan membutuhkannya dalam bukti akhir:

LA

Lemma B

Untuk menunjukkan arah lain, kita perlu melakukan dua kali beberapa hal yang cukup berulang (untuk kedua argumen A dan B di ( AB )) - ini berarti di sini saya mungkin bisa golf bukti lebih lanjut ..

Lemma B1 '

LB1_

Lemma B1

LB1

Lemma B2 '

LB2_

Lemma B2

LB2

Lemma B

Akhirnya kesimpulan dari B1 dan B2 :

LB

Bukti aktual

Setelah kami membuktikan dua pernyataan ini:

  • Lemma A : ⊢ ( AB ) → ¬ (¬ A ʌ ¬ B )
  • Lemma B : ⊢ ¬ ( AB ) → (¬ A ʌ ¬ B )

Kita dapat membuktikan kesetaraan pertama (¬ ( AB ) ≡ ¬ A ʌ ¬ B )) sebagai berikut:

P1

Dan dengan aturan yang terbukti bersama-sama dengan Iff-Elimination kita dapat membuktikan kesetaraan kedua juga:

P2

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 ):

In the following a rule \textbf{XYZ'} will denote the rule XYZ's second last
step, for example \textbf{PE'} will be $ A \land \lnot A \vdash X $.

\section*{Principle of Explosion [PE]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=10]
    {\inferrule*[Left=$\lnot$-Elim,Right=9]
      {\inferrule*[Left=$\to$-Intro,Right=4]
        {\inferrule*[Left=$\land$-Elim,Right=3]
          {\inferrule*[Left=Axiom,Right=2]
            { }
            { A \land \lnot A, \lnot X \vdash A \land \lnot A }
          }
          { A \land \lnot A, \lnot X \vdash A }
        }
        { A \land \lnot A \vdash \lnot X \to A } \\
       \inferrule*[Right=$\to$-Intro,Left=4]
          {\inferrule*[Right=$\land$-Elim,Left=3]
            {\inferrule*[Right=Axiom,Left=2]
              { }
              { A \land \lnot A, \lnot X \vdash A \land \lnot A }
            }
            { A \land \lnot A, \lnot X \vdash \lnot A }
          }
        { A \land \lnot A \vdash \lnot X \to \lnot A }
      }
      { A \land \lnot A \vdash X }
    }
    { \vdash (A \land \lnot A) \to X }
\end{mathpar}

\section*{Conditioned PE [CPE]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=5]
  {\inferrule*[Left=$\to$-Elim,Right=4]
    {\inferrule*[Left=$\land$-Intro,Right=3]
      {\inferrule*[Left=Axiom,Right=1]
        { } { A \vdash A } \\
       \inferrule*[Right=Axiom,Left=1]
        { } { \lnot A \vdash \lnot A }
      }
      { A, \lnot A \vdash A \land \lnot A } \\
     \inferrule*[Right=PE,Left=0]
      { } { \vdash (A \land \lnot A) \to X }
    }
    { A, \lnot A \vdash X }
  }
  { A \vdash \lnot A \to X }
\end{mathpar}

to get \textbf{CPE$^-$}:

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=1]
    {\inferrule*[Left=CPE',Right=0]
      { }
      { A, \lnot A \vdash X }
    }
    { \lnot A \vdash A \to X }
\end{mathpar}

\section*{Double Negation [DN]}

\begin{mathpar}
  \inferrule*[Left=$\equiv$-Intro,Right=5]
    {\inferrule*[Left=$\to$-Intro,Right=2]
      {\inferrule*[Left=$\lnot$-Elim,Right=1]
        {\inferrule*[Left=CPE$^-$,Right=0]
          { }
          { \lnot\lnot A \vdash \lnot A \to X } \\
          \inferrule*[Right=CPE$^-$,Left=0]
          { }
          { \lnot\lnot A \vdash \lnot A \to \lnot X }
        }
        { \lnot\lnot A \vdash A }
      }
      { \vdash \lnot\lnot A \to A } \\ \\ \\
      \inferrule*[Left=$\to$-Intro,Right=2]
        {\inferrule*[Left=$\lnot$-Intro,Right=1]
          {\inferrule*[Left=CPE,Right=0]
            { }
            {  A \vdash \lnot A \to X } \\
            \inferrule*[Right=CPE,Left=0]
            { }
            { A \vdash \lnot A \to \lnot X }
          }
          { A \vdash \lnot\lnot A }
        }
        { \vdash A \to \lnot\lnot A }
    }
    { \vdash \lnot\lnot A \equiv A  }
\end{mathpar}

\section*{Modus Tollens [MT]}

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=6]
    {\inferrule*[Left=$\lnot$-Intro,Right=5]
      {\inferrule*[Left=Axiom,Right=1]
       { }
       { A \to \lnot B \vdash A \to \lnot B } \\
       \inferrule*[Right=$\to$-Intro,Left=3]
         {\inferrule*[Right=Axiom,Left=2]
           { }
           { A, B \vdash B }
         }
         { B \vdash A \to B }
       }
      { A \to \lnot B, B \vdash \lnot A }
    }
    { A \to \lnot B \vdash B \to \lnot A }
\end{mathpar}

\section*{Lemma A}

\textbf{Lemma A1}:

\begin{mathpar}
  \inferrule*[Left=$\to$-Intro,Right=9]
    {\inferrule*[Left=$\lor$-Elim,Right=8]
       { \inferrule*[Left=CPE,Right=3]
          {\inferrule*[Left=$\land$-Elim,Right=2]
            {\inferrule*[Left=Axiom,Right=1]
              { }
              { A \land B \vdash A \land B }
            }
            { A \land B \vdash B}
          }
          { A \land B \vdash \lnot B \to X } \\
         \inferrule*[Right=CPE,Left=3]
          {\inferrule*[Right=$\land$-Elim,Left=2]
            {\inferrule*[Right=Axiom,Left=1]
              { }
              { A \land B \vdash A \land B }
            }
            { A \land B \vdash A }
          }
          { A \land B \vdash \lnot A \to X } \\ \\ \\
         \inferrule*[Right=Axiom,Left=1]
          { }
          { \lnot A \lor \lnot B \vdash \lnot A \lor \lnot B }
       }
       { A \land B, \lnot A \lor \lnot B \vdash X }
    }
    { \lnot A \lor \lnot B \vdash (A \land B) \to X }
\end{mathpar}

\textbf{Lemma A}:
ბიმო
sumber
1
Sejauh yang saya tahu, sistem bukti deduksi alami di sini tidak memungkinkan untuk membuktikan pernyataan sekali dengan variabel proposisi generik, dan kemudian instantiasi. Jadi, setiap kali Anda memiliki instantiasi berbeda dari salah satu lemma Anda dalam hal variabel Pdan Q, 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 keduanya P/\(Q/\R) -> (Q/\R)/\Pdan (P/\Q)/\R -> R/\(P/\Q).)
Daniel Schepler
@DanielSchepler: Ya tetapi tidak ada dependensi melingkar dan dalam aturan itu menyatakan Anda dapat membawa Lemmas dari satu bukti ke yang lain tanpa biaya untuk mencetak gol. , jadi itu akan baik-baik saja. Sunting : Sebenarnya jika itu tidak diizinkan, saya yakin pertanyaan ini hanya akan memiliki satu jawaban yang memenuhi syarat.
ბიმო
Saya menafsirkan bahwa itu hanya berarti bahwa Anda dapat memiliki beberapa bukti umum dari serangkaian formula konkret yang dibagikan di antara bukti dari dua pernyataan terakhir.
Daniel Schepler
1

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.)

 1. assume ~(P\/Q)
 2.   assume P
 3.     P\/Q  by or-introl, 2
 4.   P -> P\/Q  by impl-intro, 2, 3
 5.   P -> ~(P\/Q)  by impl-intro, 2, 1
 6.   ~P  by neg-intro, 4, 5
 7.   assume Q
 8.     P\/Q  by or-intror, 7
 9.   Q -> P\/Q  by impl-intro, 7, 8
10.   Q -> ~(P\/Q) by impl-intro, 7, 1
11.   ~Q  by neg-intro, 9, 10
12.   ~P /\ ~Q  by and-intro, 6, 11
13. ~(P\/Q) -> ~P/\~Q  by impl-intro, 1, 12
14. assume ~P /\ ~Q
15.   ~P, ~Q  by and-elim, 14
16.   assume P \/ Q
17.     assume P
18.     P -> P  by impl-intro, 17, 17
19.     assume Q
20.       assume ~P
21.       ~P -> Q  by impl-intro, 20, 19
22.       ~P -> ~Q  by impl-intro, 20, 15
23.       P  by neg-elim, 21, 22
24.     Q -> P  by impl-intro, 19, 23
25.     P  by or-elim, 16, 18, 24
26.   P\/Q -> P  by impl-elim, 16, 25
27.   P\/Q -> ~P  by impl-elim, 16, 15
28.   ~(P\/Q)  by neg-intro, 26, 27
29. ~P/\~Q -> ~(P\/Q)  by impl-intro, 14, 28
30. ~(P\/Q) <-> ~P/\~Q  by iff-intro, 13, 29
31. assume ~(P/\Q)
32.   assume ~(~P\/~Q)
33.     assume ~P
34.       ~P\/~Q  by or-introl, 33
35.     ~P -> ~P\/~Q  by impl-intro, 33, 34
36.     ~P -> ~(~P\/~Q)  by impl-intro, 33, 32
37.     P  by neg-elim, 35, 36
38.     assume ~Q
39.       ~P\/~Q  by or-intror, 38
40.     ~Q -> ~P\/~Q  by impl-intro, 38, 39
41.     ~Q -> ~(~P\/~Q)  by impl-intro, 38, 32
42.     Q  by neg-elim, 40, 41
43.     P /\ Q  by and-intro, 37, 42
44.   ~(~P\/~Q) -> P /\ Q  by impl-intro, 32, 43
45.   ~(~P\/~Q) -> ~(P /\ Q)  by impl-intro, 32, 31
46.   ~P \/ ~Q  by neg-elim, 44, 45
47. ~(P/\Q) -> ~P\/~Q  by impl-intro, 31, 46
48. assume ~P\/~Q
49.   assume ~P
50.     assume P/\Q
51.       P, Q  by and-elim, 50
52.     P/\Q -> P  by impl-intro, 50, 51
53.     P/\Q -> ~P  by impl-intro, 50, 49
54.     ~(P/\Q)  by neg-intro, 52, 53
55.   ~P -> ~(P/\Q)  by impl-intro, 49, 54
56.   assume ~Q
57.     assume P/\Q
58.       P, Q  by and-elim, 57
59.     P/\Q -> Q  by impl-intro, 57, 58
60.     P/\Q -> ~Q  by impl-intro, 57, 56
61.     ~(P/\Q)  by neg-intro, 59, 60
62.   ~Q -> ~(P/\Q)  by impl-intro, 56, 61
63.   ~(P/\Q)  by or-elim, 48, 55, 62
64. ~P\/~Q -> ~(P/\Q)  by impl-intro, 48, 63
65. ~(P/\Q) <-> ~P\/~Q  by iff-intro, 47, 64
Daniel Schepler
sumber