Доказать законы Деморгана

21

Использование десяти выводов Системы естественного удержания доказывает законы Деморгана .

Правила естественного удержания

  • Отрицание Введение: {(P → Q), (P → ¬Q)} ⊢ ¬P

  • Устранение отрицания: {(¬P → Q), (¬P → ¬Q)} ⊢ P

  • И введение: {P, Q} ⊢ P ʌ Q

  • И устранение: P ʌ Q ⊢ {P, Q}

  • Или введение: P ⊢ {(P ∨ Q),(Q ∨ P)}

  • Или устранение: {(P ∨ Q), (P → R), (Q → R)} ⊢ R

  • Iff Введение: {(P → Q), (Q → P)} ⊢ (P ≡ Q)

  • Если устранение: (P ≡ Q) ⊢ {(P → Q), (Q → P)}

  • Если введение: (P ⊢ Q) ⊢ (P → Q)

  • Если устранение: {(P → Q), P} ⊢ Q

Доказательство структуры

Каждое утверждение в вашем доказательстве должно быть результатом одного из десяти правил, примененных к некоторым ранее полученным предложениям (без круговой логики) или предположения (описанного ниже). Каждое правило действует через некоторые предложения в левой части (оператор логического следствия) и создает любое количество предложений из правой части. Введение If работает немного иначе, чем остальные операторы (подробно описано ниже). Он действует через одно утверждение, которое является логическим следствием другого.

Пример 1

У вас есть следующие заявления:

{(P → R), Q}

Вы можете использовать и введение, чтобы сделать:

(P → R) ʌ Q

Пример 2

У вас есть следующие заявления:

{(P → R), P}

Вы можете использовать Если исключение, чтобы сделать:

R

Пример 3

У вас есть следующие заявления:

(P ʌ Q)

Вы можете использовать И Исключение, чтобы сделать:

P

или сделать:

Q

Распространение предположения

Вы можете в любой момент принять любое заявление, которое пожелаете. Любое утверждение, основанное на этих предположениях, будет «зависеть» от них. Заявления также будут зависеть от допущений, на которые опираются их родительские заявления. Единственный способ устранить допущения - это «Введение». Для введения Если вы начинаете с утверждения Q, которое зависит от утверждения Pи заканчивается (P → Q). Новое утверждение зависит от каждого предположения Qопирается на только на предположение P. Ваше окончательное утверждение не должно основываться на предположениях.

Специфика и оценка

Вы построите одно доказательство для каждого из двух законов Деморгана, используя только 10 выводов исчисления естественного удержания.

Два правила:

¬(P ∨ Q) ≡ ¬P ʌ ¬Q

¬(P ʌ Q) ≡ ¬P ∨ ¬Q

Ваша оценка - это количество использованных выводов плюс количество сделанных предположений. Ваше окончательное утверждение не должно опираться на какие-либо предположения (т.е. должна быть теорема).

Вы можете отформатировать доказательство по своему усмотрению.

Вы можете переносить любые леммы из одного доказательства в другое без каких-либо затрат.

Пример доказательства

Я докажу что (P and not(P)) implies Q

(Каждая точка пули +1 балл)

  • Предполагать not (Q)

  • Предполагать (P and not(P))

  • Использование And Elim на (P and not(P))производном{P, not(P)}

  • Использование и введение Pи not(Q)для получения(P and not(Q))

  • Используйте And Elim в только что полученном заявлении P

Новое Pпредложение отличается от того, которое мы получили ранее. А именно он опирается на свои предположения not(Q)и (P and not(P)). В то время как первоначальное заявление было полагаться только на (P and not(P)). Это позволяет нам делать:

  • Если введение на Pвведение not(Q) implies P(по-прежнему зависит от (P and not(P))предположения)

  • Используйте И Введение на not(P)и not(Q)(из шага 3) для получения(not(P) and not(Q))

  • Используйте And Elim в только что сделанном заявлении not(P) (теперь зависит от not(Q))

  • Если введение о новом not(P)представленииnot(Q) implies not(P)

  • Теперь мы будем использовать исключение отрицания на not(Q) implies not(P)и not(Q) implies PполучитьQ

Это Qзависит только от предположения, (P and not(P))поэтому мы можем закончить доказательство

  • Если введение на Qвывод(P and not(P)) implies Q

Это доказательство набрало 11 баллов.

Мастер пшеницы
источник
7
Хотя консенсус в отношении мета ясен, еще не все его увидели, так что это просто для того, чтобы подчеркнуть, что доказательство игры в гольф - это тема .
Трихоплакс
2
Я думаю, что вы должны объяснить структуру доказательств и (символ также не отображается для меня на мобильном телефоне).
xnor
3
Я думаю, что объяснения определенно помогают. Что я нашел бы наиболее полезным, так это работающий и набранный пример некоторого простого доказательства, включающего в себя введение и предположения, предпочтительно вложенные. Может быть противозачаточного?
xnor
1
В вашем примере я полагаю, что первые два предположения должны были бы быть отброшены; нигде не говорится, что (P ⊢ (Q ⊢ R)) ⊢ (Q ⊢ (P ⊢ R))(в данном случае, ¬Q ⊢ ((P ʌ ¬P) ⊢ P)чтобы (P ʌ ¬P) ⊢ (¬Q ⊢ P)был использован).
LegionMammal978
1
Разрешено ли вам доказывать несколько вещей в одном «допущении контекста», а затем извлекать несколько выражений импликации, чтобы сэкономить на количестве «линий допущения»? например, (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чтобы получить оценку 9?
Даниэль Шеплер

Ответы:

6

Оценка: 81

Каждая строка должна стоить 1 балл. Законы Де Моргана можно найти в утверждениях (3) и (6). Метки в скобках обозначают предыдущие операторы, от которых зависит строка, если они не предшествуют непосредственно.

(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
источник
4

Оценка: 59

объяснение

Я буду использовать древовидную структуру для доказательства, так как я нахожу этот стиль вполне читабельным. Каждая строка помечена количеством используемых правил, например, «Пример 1» в задании будет представлен как это дерево (растущее снизу вверх):

AIntro

Обратите внимание, что неизвестные числа A, B, а также предположение Γ - так что это не теорема. Чтобы продемонстрировать, как доказать теорему, давайте предположим, что A, и введем Or следующим образом:

OIntro

Теперь это все еще зависит от предположения A, но мы можем вывести теорему, применив введение If:

IIntro

Таким образом, мы смогли вывести теорему ⊢ A → ( AB ) всего за 3 шага (1 предположение и 2 применяемых правила).

После этого мы можем доказать несколько новых правил, которые помогут нам доказать законы ДеМоргана.

Дополнительные правила

Давайте сначала выведем принцип взрыва и обозначим его PE в следующих доказательствах:

PE

Отсюда мы получаем другую форму: A ⊢ ¬ AX - назовем это CPE :

PE

Нам понадобится еще один, где отрицательный термин (¬) является предположением, и обозначим его как CPE - :

НКПР

Из двух правил, которые мы только что вывели ( CPE и CPE - ), мы можем вывести важное правило Double Negation :

DN

Следующее, что нужно сделать, это доказать что-то вроде Модуса Толленса - отсюда и MT :

Монтана

леммы

Лемма А

Лемма А1

Нам понадобится следующее правило два раза:

LA1

Лемма А

Используя дважды доказанную лемму, мы можем показать одно направление эквивалентности, оно нам понадобится в окончательном доказательстве:

Луизиана

Лемма Б

Чтобы показать другое направление, нам нужно сделать два раза несколько довольно повторяющихся вещей (для аргументов A и B в ( AB )) - это значит, что здесь я мог бы, возможно, доказать доказательство дальше ..

Лемма Б1 '

LB1_

Лемма В1

LB1

Лемма В2 '

LB2_

Лемма В2

LB2

Лемма Б

Наконец заключение B1 и B2 :

ФУНТ

Фактическое доказательство

Однажды мы доказали эти два утверждения:

  • Лемма A : ⊢ ( AB ) → ¬ (¬ A ʌ ¬ B )
  • Лемма Б : ⊢ ¬ ( AB ) → (¬ A ʌ ¬ B )

Мы можем доказать первую эквивалентность (¬ ( AB ) ≡ ¬ A ʌ ¬ B )) следующим образом:

P1

И с помощью только что доказанного правила вместе с Iff-Elvention мы можем доказать и вторую эквивалентность:

P2

Не уверен насчет счета - если я все сделал правильно, дайте мне знать, если что-то не так.

объяснение

Источник

Если кому-то нужен источник tex (нужен 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}:
ბიმო
источник
1
Насколько я могу судить, система доказательства естественного вывода здесь не позволяет доказать утверждение один раз с переменными общего предложения, а затем создавать его экземпляр. Таким образом, каждый раз , когда у вас есть различный экземпляр одного из ваших чешуй в терминах переменных Pи Q, вы должны рассчитывать свои шаги отдельно в конечном всего. (Другими словами, система доказательств не позволяет напрямую доказывать леммы «второго порядка», подобные «для всех предложений A и B A/\B -> B/\A», а затем использовать ее для доказательства обоих P/\(Q/\R) -> (Q/\R)/\Pи (P/\Q)/\R -> R/\(P/\Q).)
Даниэль Шеплер,
@DanielSchepler: Да, но циклических зависимостей нет, и в правиле, в котором говорится, вы можете переносить любые леммы из одного доказательства в другое бесплатно, чтобы получить оценку. так что все будет хорошо. Изменить : На самом деле, если бы это не было разрешено, я уверен, что этот вопрос будет иметь только один правомочный ответ.
მოიმო
Я интерпретировал это как просто означающий, что у вас могут быть общие доказательства набора конкретных формул, которые можно разделить между доказательствами двух последних утверждений.
Даниэль Шеплер
1

Оценка: 65

Законы де Моргана - строка 30 и строка 65.

(Я не прилагал особых усилий для игры в гольф, например, чтобы увидеть, есть ли какие-то повторные доказательства, которые можно было бы абстрагироваться в начале.)

 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
Даниэль Шеплер
источник