Lógica sin disyunción

Question

Estoy trabajando en un pequeño sistema de pruebas, que en principio sólo tiene la igualdad como predicado. Esta igualdad tiene algunos axiomas que la convierten en una especie de igualdad estructural: dos términos son iguales si sus constructores coinciden y todos los subterminos son iguales también. Aparte de la igualdad, también hay conjunción e implicación.

Actualmente, estoy intentando añadir la negación al lenguaje para hacerlo más expresivo. En este momento, he introducido un nuevo predicado "no igual", con algunas reglas estructurales también: dos términos con diferentes constructores son "no iguales", y si dos subtérminos son "no iguales" entonces dos términos que los contienen en la misma posición son "no iguales".

El problema viene con la implicación. En principio, si tengo a = b => F a b = G puedo construir una implicación contrapositiva F a b != G => a != b . El problema es que, si tengo la conjunción, no puedo construir directamente la implicación contrapositiva, como en a = b and a = c => F a b c = G porque mi sistema no contiene disyunción.

¿Existen referencias sobre la lógica con esta propiedad? ¿Hay alguna explicación de la expresividad que pierdo al omitir por completo la disyunción?

Answer 1

Si quiere que su lógica sea clásico (es decir, para validar principios como la ley de la doble negación), entonces, como dice Emil Jeřábek en los comentarios, se puede derivar la disyunción en términos de implicación como $\varphi \lor \psi := (\varphi \to \psi) \to \psi$ . Generalmente, en las lógicas clásicas, hay tantas maneras de interdefinir las conectivas que es difícil dar un sistema no demasiado débil que no implique el sistema usual completo.

Por otro lado, si te conformas con que tu lógica acabe siendo constructiva/intuicionista (es decir, no poder demostrar la ley de la doble negación, el medio excluido, etc.), entonces sí, se han estudiado lógicas de este tipo.

Las dos con las que estoy más familiarizado que omiten la disyunción son lógica regular y el fragmento de la Teoría de Tipos de Martin-Löf válido en cualquier LCCC (véase Martin Hofmann , Sobre la interpretación de la teoría de tipos en categorías cerradas localmente cartesianas ), es decir, sólo con tipos de función y tipos de producto.

Sin embargo, ambos suenan exagerados para tu caso - lo que esbozas suena más como el fragmento de conjunción-implicación de lógica intuicionista . En presentación de sequent caluclus separa bien las reglas para las distintas conectivas, de modo que cada una sigue funcionando bien en ausencia de las demás. Me temo que no conozco ningún lugar en el que se haya estudiado o debatido este fragmento en concreto, aunque supongo que sí.

Edita. Buscando en Google varias agrupaciones de las palabras clave conjunction , implication , fragment , intuitionistic , logic aparecen bastantes artículos que trabajan con este tipo de sistemas, aunque no encuentro ninguno que tome el propio sistema como objeto de estudio.

Answer 2

Estoy demasiado alejado del tema estos días, así que mi respuesta puede no ser muy perspicaz (pero espero que los expertos ayuden aquí). Si estás dispuesto a admitir cuantificadores (que aparecen en algunos sistemas de prueba), puedes acabar con un cálculo equivalencial parecido al prototético de Leśniewski (quizá quieras comprobar también su mereología y ontología, ya que estás interesado en la igualdad de términos cuyos "constructores" coinciden). Cita de la Stanford Encyclopedia of Philosophy, http://plato.stanford.edu/entries/lesniewski/

"La preferencia de Leśniewski por un sistema axiomático, basada en parte en el éxito de Ontología, y también en consideraciones sobre la naturaleza de la definición, era basar un sistema lógico en la conectiva única de equivalencia material, junto con el cuantificador universal. Su incapacidad para ver cómo eliminar el conectivo de conjunción en términos de equivalencia le impidió durante algún tiempo hacer esto para el Prototético. Dada la cuantificación y la equivalencia, la negación es fácil de definir, del modo que Russell sugirió una vez a Frege:

$\text{Def. }\sim: \forall p\,\ulcorner {\sim} p \leftrightarrow (p \leftrightarrow \forall r \,\ulcorner r\urcorner)\urcorner$

La solución fue encontrada por Leśniewski por su estudiante de doctorado de 21 años Alfred Teitelbaum, más tarde conocido bajo su nombre adoptivo de Alfred Tarski. Consistía en cuantificar no solo oraciones, sino funciones sentenciales o conectivas:

$\text{Def. }\wedge: \forall pq\,\ulcorner p \wedge q \leftrightarrow \forall f\,\ulcorner p \leftrightarrow (f(p) \leftrightarrow f(q))\urcorner \urcorner$

en este caso, cuantificando conectivos de un lugar. Suponiendo que sólo haya cuatro de estas conectivas, aserción, negación, Verum (tautología) y Falsum (contradicción), es sencillo demostrar que el lado derecho es equivalente a la conjunción de $p$ et $q$ . La tesis doctoral de Tarski se centra en este resultado.

En cuanto a la axiomatización, Leśniewski sabía que la teoría pura de la equivalencia podía basarse en dos axiomas que establecían la sesgo-transitividad y la asociatividad:

$P1 \quad ((p \leftrightarrow r)\leftrightarrow (q \leftrightarrow p)) \leftrightarrow (r \leftrightarrow q)$

$P2 \quad (p \leftrightarrow (q\leftrightarrow r)) \leftrightarrow ((p \leftrightarrow q) \leftrightarrow r)$ .

El cálculo equivalencial puro tiene la pintoresca propiedad, demostrada por Leśniewski, de que una fórmula es un teorema si y sólo si cada variable proposicional en ella ocurre un número par de veces."

Hago este CW, primero porque no soy un experto; segundo, porque parece que me vendría bien algo de ayuda con TeX, que está dando guerra...