¿Esta prueba es correcta? (deducción natural)

Question

Estoy trabajando a través de La ciencia de la programación por David Gries. Esta pregunta es la número 18 de la sección 3.3.

Prueba $((P \land \lnot Q) \to Q) \to (P \to Q)$

Usando el sistema de deducción natural aquí está mi prueba.

1. $(P \land \lnot Q) \to Q)$ (premisa)

2. Desde $P$ inferir $Q$ (subprueba)

   • 2.1 $P$ (premisa)

   • 2.2 De $\lnot Q$ inferir $Q$ (subprueba)

   • 2.2.1 $\lnot Q$ (premisa)

   • 2.2.2 $P \land \lnot Q$ ( $\land$ -Introducción, 2.1, 2.2.1)

   • 2.2.3 $Q$ ( $\to$ -E, 1, 2.2.2)

3. $P \to Q$ ( $\to$ -I, 2)

¿Es esto correcto? Siento que me estoy estirando al tratar de probar $P\to Q$ especialmente con la subprueba de $\lnot Q \to Q$ .

Answer 1

Tenías razón al dudar de tu prueba; no es del todo correcta.

El principal error es que estás cerrando dos subpruebas a la vez una vez que pasas de 2.2.3 a 3, pero sólo puedes cerrar una subprueba a la vez, en el orden inverso al que las abriste.

Además: necesitas tener la línea 1 como una suposición de una subprueba, y cerrar esa subprueba una vez que hayas llegado a la línea 3, para que puedas inferir toda la condicional deseada por $\rightarrow$ Introducción

Entonces, ¿qué hacer? Bueno, eso depende de las reglas que tengas. Déjame darte algunas opciones:

Opción 1:

Después de la 2.2.3 puedes conseguir:

2.3 $\neg Q \rightarrow Q$

A continuación, utilice la equivalencia de implicación para obtener $\neg \neg Q \lor Q$ y, por tanto, mediante la doble negación a $Q \lor Q$ y finalmente por Idempotencia a $Q$

Opción 2:

En primer lugar, consiga $Q \lor \neg Q$ por la Ley del Medio Excluido. Entonces, de nuevo, obtenga $\neg Q \rightarrow Q$ pero haz una segunda subprueba interna en la que asumes $Q$ , reiterar $Q$ , cierra esa subprueba para obtener $Q \rightarrow Q$ y luego obtener $Q$ de $\neg Q \rightarrow Q$ , $Q \rightarrow Q$ et $Q \lor \neg Q$ mediante una prueba por casos, probablemente formalizada como $\lor $ Elim

Opción 3:

Obtener una contradicción en 2.2.4 entre $\neg Q $ y $Q$ y, por lo tanto, concluye $\neg \neg Q$ mediante una prueba por contradicción (probablemente formalizada por $\neg \ Intro$ ), y por lo tanto el $Q$ que realmente quieres.

Answer 2

Yo lo haría de forma ligeramente diferente, pero como siempre la gente utiliza sistemas algo diferentes para la deducción natural.

• Inicie
  • 1) $(P \land \lnot Q) \rightarrow Q$ (culo.)
    • 2) $P$ (culo.)
      • 3) $\lnot Q$ (culo.)
      • 4) $(P \land \lnot Q)$ introducción $\lnot$ de 2,3.
      • 5) $Q$ (modus ponens de 1. y 4.)
      • 6) $\bot$ de $5$ y $3$ .
    • 7) $\lnot \lnot Q$ (de la introducción $\lnot$ y 3, 6, dejamos el 3).
    • 8) $Q$ (regla de la doble negación).
  • 9) $P \rightarrow Q$ (a partir de 2,8 e introducción $\to$ ); dejamos de lado el 2.
• 10) $((P \land \lnot Q) \to Q)\to (P \to Q)$ (introducción $\to$ 1, 9) dejamos caer el 1.

Hecho.

Answer 3

$\def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}}$

¿Puede utilizar la Ley del Medio Excluido?

$$\fitch{}{\fitch{(P\land\lnot Q)\to Q}{\fitch{P}{\left.\raise{5ex}{Q\vee\lnot Q\\\fitch{Q}{Q}\\Q\to Q}\right\}&\text{add this}\\\fitch{\lnot Q}{P\wedge\lnot Q\\ Q}\\\lnot Q \to Q\\Q}\\P\to Q}\\((P\land\lnot Q)\to Q )\to(P\to Q)}$$

Si no, existe la vía de la doble negación.

$$\fitch{}{\fitch{(P\land\lnot Q)\to Q}{\fitch{P}{\fitch{\lnot Q}{P\wedge\lnot Q\\ Q\\\bot}\\\lnot\lnot Q \\Q }\\P\to Q}\\((P\land\lnot Q)\to Q )\to(P\to Q)}$$

Si no se acepta el símbolo falsum, se puede modificar para introducir la negación mediante $X\to\neg Y, X\to Y\vdash \neg X$

$$\fitch{}{\fitch{(P\land\lnot Q)\to Q}{\fitch{P}{\fitch{\lnot Q}{\neg Q}\\\lnot Q\to\lnot Q\\\fitch{\lnot Q}{P\wedge\lnot Q\\ Q}\\\neg Q\to Q\\\lnot\lnot Q \\Q }\\P\to Q}\\((P\land\lnot Q)\to Q )\to(P\to Q)}$$

Te dejo las justificaciones.

Answer 4

Tu intento de derivación es erróneo porque en tu subprueba 2 no puedes tener la hipótesis $\lnot Q$ , sólo estás asumiendo que $(P \land \lnot Q) \to Q$ .

Creo que $((P \land \lnot Q) \to Q) \to (P \to Q)$ es demostrable sólo en la lógica clásica, no en lógicas más débiles como la intuicionista. Por ejemplo, puede utilizar la Ley del Medio Excluido (o alguna fórmula equivalente demostrable sólo en la lógica clásica) en su derivación en la deducción natural:

\begin{align} \dfrac{\dfrac{\dfrac{Q \lor \lnot Q \qquad [Q]^1 \qquad \dfrac{[(P \land \lnot Q) \to Q]^3 \qquad \dfrac{[P]^2 \qquad [\lnot Q]^1}{P \land \lnot Q}\land_i}{Q}\to_e}{Q}\lor_e^1}{P\to Q}\to_i^2}{((P \land \lnot Q) \to Q) \to (P \to Q)}\to_i^3 \end{align}

donde la Ley del Medio Excluido $Q \lor \lnot Q$ es demostrable en la deducción natural clásica como sigue:

\begin{align} \dfrac{\dfrac{[\lnot (Q \lor \lnot Q)]^2 \qquad \dfrac{\dfrac{\dfrac{[\lnot (Q \lor \lnot Q)]^2 \qquad \dfrac{[Q]^1}{Q \lor \lnot Q}\lor_{i_L}}{\bot}}{\lnot Q}\lnot_i^1}{Q \lor \lnot Q}\lor_{i_R}}{\bot}\lnot_e}{Q \lor \lnot Q}\text{raa}^2 \end{align}