Un prueba en la teoría Nicod-Lukasiewicz

Veamos la prueba de «p → p» en el sistema Nicod-Lukasiewicz.

Recordemos el axioma: p/qr | (s/ss) / (sq → ps)

Sustituyendo en él: 'p' por 'p/qr', 'q' por 's/ss', 'r' por 'sq → ps' y 's' por 't', obtememos:

[p/qr|(s/ss)/(sq → ps)] | t/tt / (t|s/ss → p/qr|t)

Nótese que la parte entre corchetes es el axioma mismo, por tanto podemos aplicar la regla, lo cual nos permite afirmar:

(I)  t|s/ss → p/qr|t


Sustituyendo, nuevamente en el axioma, 'p' por 't|s/ss', 'q' y 'r' por 'p/qr|t', 's' por 'w', obtenemos:


(t|(s/ss) → p/qr|t) | (w → w) / (w|(p/qr|t) → t/(s/ss)|w)

Y aplicando la regla (teniendo en cuenta I), obtenemos:

(II)   w|(p/qr|t) → t/(s/ss)|w


Ahora, realizamos en (II) la siguiente sustitución:

'w' por 'p/qr'; 'p', 'q' y 'r' por 's'; 't' por 'sq → ps', 's' por 't' y 't' por 'sq → ps'. Obtenemos el condicional:

p/qr|(s/ss)/(sq → ps) → (sq → ps)/(t/tt)|p/qr

Cuyo antecedente no es sino al axioma, y por ende:

(III)    (sq → ps)/(t/tt)|p/qr

Sustityendo en (I) 't' por '((st → ts)|t/tt)' y 's' por 't':

(st → ts)/(t/tt)| t/tt → p/qr | (st → ts)/(t/tt)

Y como reemplazando en (III) 'p', 'q' y 'r' por 't' nos da:

 (st → ts)/(t/tt)|t/tt

Luego:

(IV)     p/qr | (st → ts)/(t/tt)


Reemplazando en (IV) 'p' por 't|s/ss' y 'q' y 'r' por 'p/qr|t', obtenemos:

(t|s/ss → p/qr|t) | (st → ts) / (t/tt)

Aplicando la regla (teniendo en cuenta (I)), deducimos:

⊢ t/tt

Que es lo que se quería probar.

Más del axioma de Nicod

En el post anterior se hace rerefencia a un axioma que permite, usando la regla de sustitución y una regla de inferencia deducir toda fórmula proposicional. Lukasiwiecz menciona que Leśniewski fue quien notó que la prueba dada por Nicod de «p → p» incluía un error y que, por tanto, no era tal prueba. Esa deducción es publicada por Lukasiewicz en 1931¹. Asimismo, introduce también una modificación en el  axioma de Nicod por otro que es deductible a partir de él en un paso con una sustitución, y que es el presentado en el post citado. El de Nicod es:

p/qr | Ctt / (sq → ps)²

A partir del cual con la sustitución de t por s obtenemos el de Lukasiewicz. Otra prueba que da este autor es la que parte de esta segunda versión del axioma y concluye en la primera, permitiendo afirmar su equivalencia. Se menciona a su vez otro axioma, respecto del cual Wajsberg mostró que servía en lugar del de Nicod. Éste es:

p/qr | [(sr → ps) | p/pq]

Ejercicios:

Usando el axioma y las reglas del post citado, probar:

a. p → p
b. p/qr | Ctt / (sq → ps)



Nota:
1. Luakasiewicz, J. «Uwagi o aksjomacie Nicoda i 'dedukcji uogólniajacej'»
2. Para leer lafórmula téngase en cuenta que: dos letras minuculas una después de la otra, por ejemplo 'pq' representa «p|q»; la barra «/» tiene el mismo significado que «|», pero al momento de cerrar entre paréntesis prepondera la seguda, o sea que 'p|q/p' significa 'p|(q|p)'; 'Css' representa 's → s'.

Función Lisp para convertir fórmula en notación habitual en una de notación prefija

Habitualmente, las fórmulas de la lógica proposicional se escriben usando letras minúsculas como «p», «q», etc., para expresar proposiciones y los signos conectivos, como «→», «∧», etc. se sitúan «entre» ellas para expresar funciones veritativas en las que hagan de argumentos.

Por ejemplo: p → q, p ∧ (q → p), etc.

Se vé, en el segundo caso, que figuran dos paréntesis, lo cual resulta necesario debido a que sin ellos no resultaría claro si lo que se quiere expresar es la función escrita, a saber una conjunción cuyo segundo miembro es un condicional o (como se interpretaría sin los paréntesis) un condicional cuyo primer miembro es una conjunción.  Pero existe una manera, debida a Lukasiewicz, de expresar todas las fórmulas de la lógica proposicional (y aún con predicados y cuantificadores) sin recurrir paréntesis. Estos mismos ejemplos se escribirían así:

Cpq, KpCqp

En este post ya habíamos hecho mención de ello. Pero en el presente nos interesa mostrar una cierta función que sirve para, dada una fórmula expresada en la notación habitual, obtener una equivalente pero expresada en la de Lukasiewicz. A tal fin recurriremos al lenguaje Lisp para escribir la función.

La idea entones es partir de una fórmula tal como:

(p → q) → (p ∧ (q → p))

para obtener una como:

CCpqKpCqp

Para ello usaremos «replace-regexp-in-string». Utilizaremos los siguientes signos conectivos (en otro post, de seguir con el tema, incluiremos además los cuantificadores y los operadores modales):

→ (que en notación prefija es «C»)
∧ («K»)
∨ («A»)
↔ («E»)
|  («D»)

Lo que necesitamos hacer es que cualquier expresión "(x_*_y)" sea transformada en una expresión "*xy" donde el signo conectivo (que está representado por el asterisco, en en el que en cada caso representa un caracter diferente) pase a la primer posición izquierda, y se eliminen  los paréntesis y los espacios en blanco, representados con los guiones bajos. Para que sea más legible, procederemos a reemplazar todo paréntesis izquierdo por el número 0 y todo paréntesis derecho por el 1. Veamos, para empezar, el caso de la conjunción únicamente.

(defun conj (formula)
 (setq formula (replace-regexp-in-string " " "" formula))
 (while (string-match "∧" formula)
  (setq formula (replace-regexp-in-string "(" "0" formula)
        formula (replace-regexp-in-string ")" "1" formula)
        formula (replace-regexp-in-string "0\\([^10]*\\)∧\\([^01]*\\)1" "K\\1\\2" formula)
           )
  )
 (message "%s" formula)
 )

¿Qué hace esta función que llamamos conj?. Pues bien, primero elimina los espacios en blanco. Una vez hecho esto corrobora si en la cadena en cuestión hay algún signo conjuntivo en notación habitual. Si la prueba da t (true) esto significa que hay que aplicar los cambios que siguen. A saber, se cambian los paréntesis por 0 y 1 (como dije, para mayor claridad), luego se toma cualquier subcadena que figure entre paréntesis (0 y 1) y que tenga una signo conectivo ∧ y que no incluya otros paréntesis que los extremos y se reemplaza por otra cadena compuesta por:

Primero, la letra K, que es el signo de la conectiva sobre la que se aplica la función en la notación de Lukasiewicz
Segundo, la parte que se encontraba a izquierda del signo conectivo y
Tercero, la parte que se hallaba a la derecha.

Evidentemente, esto impone la condición de que la fórmula que sea tomada por argumento no debe tener conjunciones de más de dos miembros. Así, en lugar de

p ∧ q ∧ r

debemos escribir, por ejemplo, la fórmula equivalente:

((p ∧ q) ∧ r)

También debe notarse que la fórmula ingresada debe tener paréntesis extremos, aunque sería sencillo evitar esta condición agregándolos en la misma función.

Ahora tenemos que hacer una función que haga la tarea requerida, que llamaremos «nlukasiewicz»

(defun nlukasiewicz (formula)
 (setq formula (replace-regexp-in-string " " "" formula)
       formula (replace-regexp-in-string "¬" "N" formula))
 (while (or (string-match "∧" formula)
        (string-match "∨" formula)
        (string-match "→" formula)
        (string-match "↔" formula))
  (setq formula (replace-regexp-in-string "(" "0" formula)
        formula (replace-regexp-in-string ")" "1" formula)
        formula (replace-regexp-in-string "0\\([^10]*\\)∧\\([^01]*\\)1" "K\\1\\2" formula)
        formula (replace-regexp-in-string "0\\([^10]*\\)∨\\([^01]*\\)1" "A\\1\\2" formula)
        formula (replace-regexp-in-string "0\\([^10]*\\)→\\([^01]*\\)1" "C\\1\\2" formula)
        formula (replace-regexp-in-string "0\\([^10]*\\)↔\\([^01]*\\)1" "E\\1\\2" formula)
           )
  )
 (message "%s" formula)
 )

El lector puede probar en el programa "Emacs" el siguiente ejemplo (luego, claro, de haber evaluado la función):

(nlukasiewicz "((p ∧ (¬q ∨ (¬q → p))) ↔ (p ∧ (p ∨ (q → ¬p))))")

Cuyo resultado es:  EKpANqCNqpKpApCqNp

Dejaremos la barra de Sheffer como ejercicio para el lector.

Un método para el cálculo restringido de predicados

El método de la cuarta edición de Hilbert-Ackerman (Grundzüge der theoretischen Logic) para demostrar las fórmulas válidas proposicionales fue presentado en este post.

Sobre dicha base se formula en el mismo libro un sistema axiomático para la expresiones universalmente válidas del cálculo restringido de predicados (la lógica de primer orden).

Se reformula el concepto de fórmula elemental¹. Serán elementales las fórmulas que consistan en una disyunción «α₁ ∨ ... ∨ α₂» donde:

1) α_i será una fórmula primaria, una fórmula primaria negada o será de la forma: «∃x β» o «∃y β» o «∃z β», etc.
2) han de existir una α_i y uan α_j tales que α_i sea una fórmula primaria y α_j sea «¬α_i».

Las reglas de deducción son:

(a)


   θ ∨ α ∨ γ 
θ ∨ ¬¬α ∨ γ

No es necesario que θ y γ estén presentes en la deducción. Si lo hace γ, ninguno de sus miembros disyuntivos tendrá la forma «¬¬β», «¬(β ∨ δ)» o «¬∃x β» (ni tener una forma así).

(b)

θ ∨ ¬α ∨ γ             θ ∨ ¬β ∨ γ
        θ ∨ ¬(α ∨ β) ∨ γ

Aquí se cumplen para θ y γ las mismas reglas que en (a). En cuanto a β, ésta no puede ser una disyunción.

la siguiente regla no tenía lugar en el cálculo proposicional:

(c)

  θ ∨ ¬α(y) ∨ γ 
θ ∨ ¬∃x α(x) ∨ γ

La expresión «α(y)» contiene una variable libre y. θ y γ (que están sujetas a idénticas condiciones que en (a)) pueden no estar presentes y si lo están en ellas no aparecerá dicha variable, ni tampoco la variable x (pueden tener otras variables).

La última regla es la siguiente:

(d)

θ ∨ ∃x α(x) ∨ α(y) ∨ γ
   θ ∨   ∃x α(x)   ∨   γ

θ y γ deben cumplir con las mismas condiciones que en (a) se exigen para θ. «α(y)» no debe aparecer como miembro disyuntivo una segunda en la fórmula superior.

La equivalencia entre las fórmulas de cada uno de los pisos de (c) se vé así: «¬α(y)» significa que esta fórmula si es verdadero, lo es de cualquier y, pues es una variable libre. Esto equivale a decir que lo es de todo «y», es decir «∀y ¬α(y)». Es cierto además que decir que para todo «x» se cumple que no es α es lo mismo que decir que no existe «x» alguno para el que se cumpla α. O sea: «¬∃y α(y)».

La equivalencia entre los pisos de (d) se sigue de la equivalencia siguiente:

∃x α(x) ∨ α(x)   ≡eq   ∃x α(x)

Esto es así porque:

Primero: ∃x α(x) ∨ α(x)  →   ∃x α(x)

1) ∃x α(x) implica   ∃x α(x) por motivos obvios.
2) Si α(x), esto significa que α es verdadero de cualquier x, asi dado que el dominio de la función no es vacío, existe en él al menos un x que es α

Segundo: ∃x α(x)   →    ∃x α(x) ∨ α(x)

Basta con que el antecedente implique cualquiera de los miembros disyuntivos del consecuente, que es el caso de 1).

___________
1. Se agregan las fórmulas con letras de predicados y cuantificadores a las variables proposicionales.

Demostraciones lógicas

Obtuvimos de la página rinconmatematico.com (del foro de lógica y teoría de conjuntos), el siguiente ejercicio:


1. El lenguaje a utilizar consta del alfabeto de símbolos: ¬, →, (, ), p, q, etc.

2. Un conjunto de fórmulas bien formadas (fbf), que son aquellas que cumplen:

i. p, q, r, etc. son cada una fbf.

ii. Si A y B son fbf, así lo son ¬A y  ¬B.

iii. El conjunto de todas las fbf. es generado por (i) y (ii)

3. Axiomas. Para cada A, B, fbf  se cumple:

L1  (A → (B → A))
L2  ((A → (B → C) → ((A → B) → (A → C))
L3  (¬A → ¬B) → (B → A)

4. Regla de inferencia.
De A, A → B  es consecuencia inmediata B.

5. También pueden usarse las siguientes formas adicionales de deducción:
1. Si γ, A ⊢ B entonces γ ⊢ (A → B)
2. A → B, B → C ⊢ A → C

A) Demuéstrese:

A.1) (p → q) → ((¬p → ¬q) → (q → q)
A.2) ((p → (q → r)) → (p → q)) → ((p → (q → r)) → (p → r))
A.3) (p → (p → q)) → (p → q)
A.4)  p → (q → (p → q))

B) Como ejercicio adicional puede intentarse demostrar estas formas adicionales a partir de L1, L2, L3 y la regla de inferencia. 

Demostraciones formales Implicación estricta

Hace unos días, en este post, citamos un sistema lógico que figura en el libro de Hilbert y Ackermann de la bibliografía, que se caracteriza por un concepto de implicación que no es el mas frecuente. Mostraré ahora cómo puede procederse con él para demostrar algunas de las fórmulas que figuran en este post. Desde ya, de aquellas proposiciones que se demuestran en una línea figura a la derecha el esquema axiomático del que son instancias.


i) A → ¬¬A                              Esquema Axiomático 14


iii) A ∧ (A → B) → B

a) (A → B) → ((A ∧ (A → B) → A) → (A ∧ (A → B ) → B))   EA 3
b) A ∧ (A → B) → A                                                         EA 5
c) (A → B) → (A ∧ (A → B ) → B)                                 Regla IV a,b
d) ((A → B) → (A ∧ (A → B) → B)) → ((A ∧ (A → B) → (A → B)) →
     → ((A ∧ (A → B) → (A ∧ (A → B) → B)))                    
                                                                                           EA3
e) ((A ∧ (A → B) → (A → B)) → ((A ∧ (A → B) → (A ∧ (A → B) → B))
                                                                                   Rega I, c,d
f) A ∧ (A → B) → (A → B)                                                 EA 6
g) A ∧ (A → B) → (A ∧ (A → B) → B)                             Regla I, e,f
h) A ∧ (A → B) → (A ∧ (A → B) → B)) → (A ∧ (A → B) → B)    EA 4
i) A ∧ (A → B) → B                                                       Regla I g,h




iv) (A → B) → (¬B → ¬A)                     E.A. 12



v) (A → B) → ((B → C) → (A → C))        E.A. 3



vi) ¬¬¬A → ¬A                                   E.A. 15



vii) ¬A → ¬¬¬A                                      E.A. 14


viii) ¬A → ¬(A ∧ B)

a)  A ∧ B → A                                          E.A.5
b)  (A ∧ B → A) → (¬A → ¬(A ∧ B))          E.A.12
c)  ¬A → ¬(A ∧ B)                                   R.I, a, b.




xi) ¬(A ∨ B) → ¬A ∧ ¬B

a)  A → A ∨ B                                             E.A.5
b)  B → A ∨ B                                             E.A.6
c)  (A → A ∨ B) → (¬(A ∨ B) → ¬A)            E.A.12
d)  ¬(A ∨ B) → ¬A                                     Regla I, a, c
e)  (B → A ∨ B) → (¬(A ∨ B) → ¬B)              E.A.12
f)  ¬(A ∨ B) → ¬B                                       Regla I, b, e
g)  (¬(A ∨ B) → ¬A) ∧ (¬(A ∨ B) → ¬B) →
    → (¬(A ∨ B) → ¬A ∧ ¬B)                        E.A.7
h)  (¬(A ∨ B) → ¬A) ∧ (¬(A ∨ B) → ¬B)      R.II, d, f.
i)  ¬(A ∨ B) → ¬A ∧ ¬B                              R.I, g, h.