Yo uso la notación polaca. C denota un condicional, E lógica de la equivalencia, Una disyunción, K conjunción, y N la negación. La corrección de esta respuesta depende de las funciones unarias (o, equivalentemente, "functors") de quantum lógica proposicional. No sé cuáles son, pero me sentiría sorprendido si el método que yo en esta respuesta sería un fracaso.
Existe un lexema [al menos espero que pueda invocar aquí] que dice que "si x=y, entonces Exy" donde E viene como lógica de la equivalencia. Voy a utilizar los axiomas ecuacionales aquí para una orthomodular de celosía. En consecuencia, se sigue que cualquier axiomatization para un orthomodular celosía lógica proposicional va a satisfacer
commutation of disjunction 1 E Aab Aba
association of disjunction 2 E AAabc AaAbc
Double negation equivalence 3 E NNa a
A-K absorption 4 E AaKab a
Petrus Hispanus NANaNb-K 5 E NANaNb Kab
Modular Lattice Law 6 E Aab A[ K (Aab) Nb] b
Lo que habría de venir como una regla de inferencia? No podemos usar {E$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$ ya que todos los anteriores axiomas no tienen "E" como la principal conectivo de la antecedente. Así que, estructuralmente hablando, ¿qué ecuaciones nos permiten hacer? Ellos nos permiten reemplazar una adecuada o inadecuada subformula $\zeta$ otro $\epsilon$ donde $\zeta$=$\epsilon$. Sí existe un camino para obtener la misma capacidad para sustituir a una adecuada o inadecuada subformula con un equivalente lógicamente uno en un cálculo proposicional sin utilizar la lógica de equivalencia E. por Lo tanto, aunque los anteriores seis bien formado fórmulas no funcionan como un axioma conjunto, todavía vienen como útil para encontrar al menos una posible axioma conjunto.
Deje $\delta$ el valor de una variable en función de un argumento. Hay una proposición de ley, que Lukasiewicz llama "la ley de extensionality", que dice que C Epq C $\delta$ p $\delta$ q (Lukasiewicz consiguió su comprensión de estas ideas de Lesniewski). Ahora usted puede hacer sustituciones para la variable de funciones. Explicaré cómo saber cuando se puede hacer esto en la última parte de esta respuesta. También sostiene que dado el desapego, que "si "si C $\delta$ p $\delta$ p", entonces "si C $\delta$p $\delta$ p"." De ello se sigue que cualquier bien formado fórmula del tipo C $\delta$ p $\delta$ q, junto con la sustitución y el desapego le da el mismo poder de colocación adecuada o inadecuada subformulas con otro equivalente adecuado o inadecuado subformulas.
Ahora, supongamos que a=b y b=c. Por la propiedad de reemplazo de igualdad, a=b, podemos b por c y obtener a=c. Por lo tanto, la propiedad transitiva de la igualdad se sigue de la propiedad de reemplazo de la igualdad.
Ahora supongamos que a=b. Así, podemos reemplazar la derecha b con la obtención de un=un. Por lo tanto, la propiedad reflexiva de la igualdad se sigue de la propiedad de reemplazo.
También, bajo la hipótesis de que a=b, ya que a=a también, se puede sustituir el derecho "a" a=a y obtener b=a. Por lo tanto, la propiedad simétrica de la igualdad se sigue de reemplazo.
El resultado de todo esto viene como que cualquier cosa que nos da el mismo poder que la propiedad de reemplazo de la igualdad o equivalencia lógica, nos da el mismo poder que una teoría ecuacional con sólo cuantificadores universal.
Por lo tanto, a través de la ley de extensionality, el siguiente axioma conjunto (si todas las funciones unarias de orthomodular celosía cálculo proposicional asegúrese de que los siguientes axiomas como de sonido con respecto a la semántica de orthomodular lógica proposicional) tiene el mismo poder que el de la teoría ecuacional, y lo que, lógicamente, debería funcionar como un axioma establecido para el orthomodular celosía cálculo proposicional. También podríamos necesitar algo
commutation of disjunction 1 C δ Aab δ Aba.
association of disjunction 2 C δ AAabc δ AaAbc.
Double negation equivalence 3 C δ NNa δ a.
A-K absorption 4 C δ AaKab δ a.
Petrus Hispanus NANaNb-K 5 C δ NANaNb δ Kab.
Modular Lattice Law 6 C δ Aab δ A[ K (Aab) Nb] b.
Rule of detachment {Cαβ, α} ⊢ β.
The rule of uniform substitution.
También podríamos necesitar algún otro axioma(s) que nos dan un teorema de la deducción (tales como {CpCqp, CCpCqrCCpqCpr}) o si eso no funciona, entonces algo como CCpqCCqrCpr (si es que funciona).
La regla de uniforme de sustitución incluye la sustitución de $\delta$. Para saber cuando se puede utilizar una sustitución de $\delta$ puede hacer lo siguiente:
- Asignar -1 para el único símbolo apóstrofo '
- Asignar -1 a todas las letras en minúscula del alfabeto latino (o numéricamente subíndice letras minúsculas del alfabeto latino).
- Asignar 1 a todas las conectivas binarias.
- Asignar 0 a todos los unarios conectivas.
- Asignar 0 a $\delta$.
Un uniforme para la sustitución de $\delta$ es admisible, si y sólo si contiene al menos un apóstrofo, cuando se empieza con 0 antes de hacer cualquier suma, y la forma de sumas de izquierda a derecha utilizando las anteriores asignaciones de un proceso de totalización nunca llega a -2, y una suma de proceso termina con -1. Usted también podría suponer un "1" en el espacio en blanco a la izquierda de la bien formada fórmula, y, en consecuencia, un resumen del proceso terminará con 0 y nunca se corresponden en cualquier punto a -1 si es admisible la sustitución.
Algunos ejemplos de tales un resumen del proceso:
C p ' '
1 0 (-1) (-2)
--------------
C ' z
1 0 (-1)
--------------
A C ' ' δ '
1 2 1 0 0 (-1)
-----------------
K δ δ ' C p r
1 1 1 0 1 0 (-1)
Yo uso la notación de donde x/ y indica que x se presenta sustituido con y. También, C x- y indica que tenemos algún bien formado fórmula que comienza con C, se tiene x como su siguiente parte, y como su última parte, y dado que ya tenemos x vamos a separar y. "*" funciona como un separador donde el lado izquierdo de la * y el lado derecho de la "*" como se equiform si usted escribió las sustituciones indicadas en su totalidad.
Como un ejemplo de una prueba que demostrará $\vdash$CAAbacAaAbc.
1 C δ Aab δ Aba.
2 C δ AAabc δ AaAbc.
1 δ/CA'cAaAbc * 3
3 C CA Aab cAaAbc CA Aba cAaAbc.
2 δ/' * 4
4 CAAabcAaAbc.
3 * C 4 - 5
5 C AAbac AaAbc.
