Ayuda de Fitch Proof by Contradiction

Las reglas de inferencia se nombran como son por una razón.

Cuando sienta la necesidad de plantear un contexto para derivar un objetivo, determine qué regla de introducción necesitará para deducir el objetivo. Eso le dirá qué suposición podría necesitar plantear y qué conclusión deberá derivar .

• Cuando el destino es un condicional, como Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)), use la introducción condicional . Asume el antecedente y deriva el consecuente .

• Cuando el objetivo es una negación, como ~(StrongPref(b,a) v StrongPref(a,b)), usa la introducción de negación . Asumir lo positivo y derivar una contradicción.

Al llegar a un objetivo que no es producido por una regla de introducción, observe los supuestos (y premisas) de las reglas de eliminación para completar las derivaciones.

• Cuando haya asumido una disyunción, como StrongPref(b,a) v StrongPref(a,b), utilice la eliminación de disyunción . Asuma cada caso en sucesión y obtenga la misma consecuencia.

De hecho, dejaré derivar la contradicción (pero, está bien, las premisas 3 y 4 son las más útiles).

|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x) 
|  Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]
|  |  |_ [b]
|  |  |  |_ Indiff(a,b)
|  |  |  |  :
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)
|  |  |  |  |  |_ StrongPref(b,a)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  :
|  |  |  |  |  |  #
|  |  |  |  |  #
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b))
|  |  :

Editar: la prueba completa

:
|  Ɐx Ɐy StrongPref(x,y) ↔ ~WeakPref(y,x) 
|_ Ɐx Ɐy Indiff(x,y) → WeakPref(y,x) ^ WeakPref(x,y)
|  |_ [a]                                                   Arbitrary Term
|  |  |_ [b]                                                Arbitrary Term
|  |  |  |_ Indiff(a,b)                                     Assumption
|  |  |  |  Ɐy Indiff(a,y) → WeakPref(y,a) ^ WeakPref(a,y)  Universal Elimination
|  |  |  |  Indiff(a,b) → WeakPref(b,a) ^ WeakPref(a,b)     Universal Elimination
|  |  |  |  WeakPref(b,a) ^ WeakPref(a,b)                   Conditional Elimination
|  |  |  |  WeakPref(b,a)                                   Conjunction Elimination 
|  |  |  |  WeakPref(a,b)                                   Conjunction Elimination
|  |  |  |  |_ StrongPref(b,a) v StrongPref(a,b)            Assumption
|  |  |  |  |  |_ StrongPref(b,a)                           Assumption
|  |  |  |  |  |  Ɐy StrongPref(b,y) ↔ ~WeakPref(y,b)       Universal Elimination
|  |  |  |  |  |  StrongPref(b,a) ↔ ~WeakPref(a,b)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(a,b)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  +
|  |  |  |  |  |_ StrongPref(a,b)
|  |  |  |  |  |  Ɐy StrongPref(a,y) ↔ ~WeakPref(y,a)       Universal Elimination
|  |  |  |  |  |  StrongPref(a,b) ↔ ~WeakPref(b,a)          Universal Elimination
|  |  |  |  |  |  ~WeakPref(b,a)                            Biconditional Elimination
|  |  |  |  |  |  #                                         Negation Elimination
|  |  |  |  |  #                                            Disjunction Elimination
|  |  |  |  ~(StrongPref(b,a) v StrongPref(a,b))            Negation Introduction
|  |  |  Indiff(a,b) → ~(StrongPref(b,a) v StrongPref(a,b)) Conditional Introduction
|  |  Ɐy Indiff(a,y) → ~(StrongPref(y,a) v StrongPref(a,y)) Universal Introduction
|  Ɐx Ɐy Indiff(x,y) → ~(StrongPref(y,x) v StrongPref(x,y)) Universal Introduction

Aquí hay una prueba usando un verificador de prueba diferente. También hice algunas sustituciones.

• Para Indiff usé I .
• Para StrongPref usé S .
• Para WeakPref usé W .

De las cuatro premisas solo utilicé la tercera y la cuarta.

Aquí están las preocupaciones:

He llegado tan lejos en la prueba ahora, pero no estoy seguro de si lo que estoy haciendo está mal, ya que ya no puedo usar instancias universales. De manera similar, no puedo encontrar la contradicción requerida para ~(StrongPref(b,a) v StrongPref(a,b)).

También me encontré con un problema con las instancias o introducciones universales, pero tenía dos premisas separadas en las que usé la eliminación universal. No asocié las variables en los enunciados universales con los mismos nombres en estas dos premisas. En otras palabras, solo porque asocié "x" con "a" en la cuarta premisa no significa que no pueda asociar "x" con "b" en la tercera premisa. Del mismo modo para "y". La "x" y la "y" son variables y pueden representar cualquier nombre, ya que son variables universalmente cuantificadas. Se puede usar cualquier nombre.

En particular, para eliminar el cuantificador universal de "x" en la premisa 4, reemplacé la variable "x" con el nombre "a" en la línea 5. Luego eliminé el cuantificador universal de "y" en la línea 5 reemplazando la variable "y" con el nombre "b". Esto produjo la línea 6.

Sin embargo, en la línea 9 usé la eliminación universal en la premisa 3 reemplazando "x" con "b" (no "a"). En la línea 10, usé eliminación universal en la línea 9 y reemplacé "y" con "a" (no "b").

Para introducir la negación en 15, asumí "Sba" en la línea 11, eliminé el bicondicional en la línea 12, eliminé la conjunción en la línea 13 y derivé una contradicción en la línea 14. Esa contradicción me permitió derivar "¬Sba" en la línea 15.

Referencias

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

PD Magnus, Tim Button con adiciones de J. Robert Loftis remezcladas y revisadas por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, invierno de 2018. http://forallx.openlogicproject.org/