В Fitch, как можно доказать «(P → Q)» из посылки «(¬P ∨ Q)»?

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

1) Q --- предполагается для доказательства по случаям [а-1]

2) P → Q --- из 1) по условному введению

3) ¬P --- предполагается для доказательства по случаям [a-2]

4) Р --- предполагается [б]

5) противоречие!

6) Q --- из 5) Ex falso

7) P → Q --- из 6) Условным введением, разрядкой [б]

и это сделано.

Используя редактор и средство проверки естественного вывода в стиле Fitch, я могу написать следующее доказательство:

Строка 1 содержит предпосылку.

Поскольку мы в конечном итоге хотим, чтобы при предположении «P» получилось «Q», я предполагаю «P» в строке 2, запуская подпроверку, которая, согласно нотации Fitch, имеет отступ.

Чтобы получить противоречие, я начинаю еще одно поддоказательство и предполагаю, что «¬Q» в строке 3.

В строке 4 я использую правило дизъюнктивного силлогизма (DS). У меня есть дизъюнкция «¬P ∨ Q» и «¬Q». Я могу заключить дизъюнктивным силлогизмом «¬P». См. forall x: Calgary Remix , стр. 124–125, описание этого правила.

В строке 5 я ввожу противоречие (⊥) из-за строк 2 и 4.

Противоречие завершает косвенное доказательство (IP), которое позволяет мне закрыть поддоказательство, освобождающее от предположения «¬Q» в строке 6.

В строке 7 я ввожу условное выражение из строк 2–6, что завершает доказательство.

Поскольку вы пытаетесь доказать, что дизъюнкция влечет за собой условное , поэтому ваша стратегия должна заключаться в следующем: используйте устранение дизъюнкции и, в каждом случае, условное введение , если можете.

|_ ~p v q         : premise
|  |_ ~p          : assumed case 1
|  |  |_ p        : assumption
|  |  |           : ...
|  |  |  q        : ...
|  |  p -> q      : conditional introduction (...)
|  ~p -> (p -> q) : conditional introduction (...)
|  |_ q           : assumed case 2
|  |  |_ p        : assumption
|  |  |  q        : reiteration (...)
|  |  p -> q      : conditional introduction (...)
|  q -> (p -> q)  : conditional introduction (...)
|  p -> q         : disjunction elimination (...)

Тогда остается только решить , будет ли p подразумевать q в каждом из двух случаев, и как , если да.

В качестве альтернативы сначала предположим p, а затем используем устранение дизъюнкции. [Часто оказывается более эффективным отложить DE как можно дольше: построить гору с двумя вершинами, а не с двумя горами.]

 |_ ~p v q      : premise
 |  |_ p        : assumption
 |  |  |_ ~p    : assumption
 |  |  |  :     : ...
 |  |  |  q     : ...
 |  |  ~p -> q  : conditional introduction
 |  |  |_ q     : assumption
 |  |  q -> q   : conditional introduction
 |  |  q        : disjunction elimination
 |  p -> q      : conditional introduction