txt

← Vida real

Completitud del cálculo de secuentes LK

Holaaa, díganme si les parece bien esta prueba de completitud de secuentes clásicos:

Primero supongo una tautología C cualquiera en forma normal conjuntiva, i.e. C1∧...∧Ck, donde cada Ci tiene la forma ~P1∨...∨~Pn ∨ Q1∨...∨Qm. (puede ser cualquier sucesión de proposiciones afirmadas y negadas, simplemente las ordené primero las negadas y después las afirmadas por comodidad, que se verá a continuación). Esto nos permite aplicar un criterio de tautología: Una cláusula Ci es tautológica si y solo si algún átomo aparece tanto en el grupo de los negados como en el de los afirmados ---ya que para que la disyunción sea falsa deberíamos tener una asignación que haga verdadero todos los P y falso todos los Q, pero dado que existe un Pn=Qm, esto no puede ocurrir---.

Por otro lado, sabemos (por las reglas) que ⊢Δ,A∧B es derivable si y solo si tanto ⊢Δ,A como ⊢Δ,B son derivables. Por lo tanto, el secuente ⊢C es derivable si y solo si cada uno de sus ⊢Ci constituyentes es derivable. O, lo que es lo mismo, si

⊢ ~P1∨...∨~Pn ∨ Q1∨...∨Qm

es derivable.

También sabemos (por las reglas) que ⊢Δ,A∨B es derivable si y solo si ⊢Δ,A,B es derivable. (del lado derecho podemos convertir las comas en disyunciones y viceversa). Así que convertimos todas las disyunciones en comas y obtenemos:

⊢ ~P1,...,~Pn, Q1,...,Qm

Finalmente, por la regla de la negación sabemos que Γ⊢Δ,~A es derivable si y solo si A,Γ⊢Δ es derivable. (recordemos que A⊢ ≡ ⊢~A).

Entonces, podemos aplicar esa operación a todas las P, pasándolas una a una al lado izquierdo, donde quedarán afirmadas. Así obtendremos esto:

P1,...,Pn ⊢ Q1,...,Qm

Ahora bien, claramente P⊢Q no es formalmente válido. Es decir, que la única manera de que el secuente anterior se de es que sea una instancia de reflexividad (A⊢A) a la que se le agregaron fórmulas con weakening. Quiero decir: P1,...,Pn ⊢ Q1,...,Qm es derivable cuando un átomo x está entre los P y entre los Q. i.e. para algun i,j,Pi≡Qj. Y esa es exactamente la cláusula para que Ci sea una tautología.

Es decir, para ser derivable y para ser una tautología deben satisfacer la misma condición. Por lo tanto, un secuente es derivable si y solo si es lógicamente verdadero.

Espero que les haya gustado. Acepto sugerencias y correcciones :) buenas vibras (~._.)~
Sisi, esta bien

Respuestas: >>2106

>>1897 Gracias, me preocupaba
Gordo me la paso fumando per te amo seguí estudiando esto que el país necesita gente que aunque lo descansen o ni pelota, hable de esto

Entrá para responder.