En Fitch, ¿cómo se prueba "(P → Q)" a partir de la premisa "(¬P ∨ Q)"?

Tiene razón: la forma correcta es usar Prueba por casos (también conocido como eliminación de disyunción ):

1) Q --- asumido para la prueba por casos [a-1]

2) P → Q --- de 1) por introducción condicional

3) ¬P --- asumido para la prueba por casos [a-2]

4) P --- asumido [b]

5) ¡contradicción!

6) P --- de 5) por Ex falso

7) P → Q --- de 6) por introducción condicional, descarga [b]

y está hecho

Usando el editor y verificador de prueba de deducción natural al estilo de Fitch, puedo escribir la siguiente prueba:

La línea 1 contiene la premisa.

Dado que finalmente queremos que al asumir "P" obtengamos "Q", asumo "P" en la línea 2 al comenzar una subdemostración que, según la notación de Fitch, está sangrada.

Para obtener una contradicción, empiezo otra subdemostración y asumo "¬Q" en la línea 3.

En la línea 4, uso la regla del silogismo disyuntivo (DS). Tengo una disyunción, "¬P ∨ Q" y "¬Q". Puedo concluir por silogismo disyuntivo "¬P". Ver forall x: Calgary Remix , páginas 124-5, para una descripción de esta regla.

En la línea 5, introduzco una contradicción (⊥) debido a las líneas 2 y 4.

La contradicción completa una prueba indirecta (IP) que me permite cerrar la subprueba descargando la suposición, "¬Q", en la línea 6.

En la línea 7, introduzco un condicional de las líneas 2 a la 6 que completa la demostración.

Dado que busca probar que una disyunción implica un condicional , su estrategia debería ser: usar la eliminación de la disyunción y, en cada caso, la introducción condicional , si puede.

|_ ~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 (...)

Entonces solo es cuestión de decidir si p implicaría q en cada uno de los dos casos, y cómo , si es así.

Alternativamente, asuma p primero y luego use la eliminación por disyunción. [A menudo resulta más eficiente retrasar la DE el mayor tiempo posible: construir una montaña con dos picos en lugar de dos montañas.]

 |_ ~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