Пропозициональная логика: как доказать противопоставление в системе Fitch?

1. p => q         Premise
2.   | ~q         Assumption
3.      || p      Assumption    
4.      || ~q     Reiteration: 2
5.   | p => ~q    Implication Introduction: 3, 4
6.   | ~p         Negation Introduction: 1, 5
7. ~q => ~p       Implication Introduction: 2, 6

Я не очень хорошо знаком с Fitch, но вот как бы я это сделал:

Во-первых, предположим данное нам предположение.

Затем определите вероятный путь к заключению. Учитывая, что наш вывод является условным, есть два или три основных способа закончить его. Во-первых, это импликация материала (~avb |- a -> b). Во-вторых, условное введение — возьмите аргумент, начинающийся с предположения, и опустите его на уровень ниже условного. В-третьих, это вытекает из какого-то большего выражения.

В этом случае единственным жизнеспособным кандидатом является условное введение. Таким образом, наша вторая строка должна быть предположением о ~q.

Наш следующий вопрос — как добраться до ~p. Чтобы получить не, мы можем либо сделать что-то вроде условной импликации Де Моргана, либо отказаться от предположения из-за противоречия. Здесь мы собираемся сделать последнее.

1. p -> q A

2. | ~q А

3. | | р А

4. | | q МП 1,3

5. | | ~q R 2

6. | | ⊥ Введение (⊥ Intro) 4,5

7. | ~p Контра. Элим 3-5

8. ~q -> ~p Условное введение 2-6

Используя редактор доказательства естественной дедукции в стиле Fitch и средство проверки, связанное с forall x: Calgary Remix , я могу действовать следующим образом:

Строка 1 является предпосылкой.

В строке 2 я предполагаю, что «¬Q», и поэтому начинаю дополнительное доказательство, которое имеет отступ в соответствии с обозначениями Fitch.

В строке 3, чтобы окончательно прийти к противоречию, я предполагаю «¬¬P». Я использую двойное отрицание, так как хочу удалить один из этих не-символов (¬), когда вывожу противоречие (⊥).

В строке 4 я удаляю двойное отрицание из строки 3, что дает мне «P».

В строке 5 я использую это «P» в строке 4 и исключаю условное предложение (→E) в строке 1. Это также называется modus ponens , то есть, учитывая «P» и «P → Q», я могу сделать вывод «Q ".

Объединение строк 5 со строками 2 позволяет мне ввести противоречие (⊥I) в строку 6.

Противоречие в строке 6 позволяет мне использовать косвенное доказательство (IP), чтобы получить «¬P» в строке 7.

В строке 8 я могу закрыть поддоказательство, которое опровергает предположение, сделанное в строке 2, путем введения условного оператора (→I), основанного на поддоказательстве в строках со 2 по 7.