¿Axiomas basados en ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot para la lógica intuicionista proposicional?

Question

¿Axiomas basados en ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot para la lógica intuicionista proposicional?

lógica
axiomas
Matemáticas
cálculo proposicional
matematicas-constructivas

MarnixKlooster ReintegroMonica

La lógica intuicionista proposicional se puede axiomatizar basándose en $\;\to, \land, \lor, \bot\;$ , con modus ponens

de ϕ y ϕ \to ψ inferir ψ

$\text{from }\; \phi \;\text{ and }\; \phi \to \psi \;\text{ infer }\; \psi$ como la única regla de inferencia, y una lista de axiomas como

ϕ \to (x \to ϕ)

$\phi \to (\chi \to \phi )$ Consulte la página de Wikipedia sobre 'Lógica intuicionista' en 'Cálculo al estilo de Hilbert' para obtener una lista completa de axiomas.

Ahora esa misma página también afirma que "{∨, ↔, ⊥} y {∨, ↔, ¬} son bases completas de conectores intuicionistas". Y lo que estoy buscando es una lista de reglas de inferencia y axiomas para respaldar la afirmación de Wikipedia.

Estrictamente hablando, esto es, por supuesto, simple: se puede tomar la $\;\to, \land, \lor, \bot\;$ axiomas, y reemplazar cada $\;\phi \to \psi\;$ por $\;(\phi \lor \psi) \leftrightarrow \psi\;$ , y cada $\;\phi \land \psi\;$ por $\;(\phi \lor \psi) \leftrightarrow (\phi \leftrightarrow \psi)\;$ . Pero el resultado no es muy elegante.

He estado desconcertado un poco sobre la construcción de una mejor axiomatización, y creo que al menos debería tener la regla de inferencia

de ϕ y ϕ \leftrightarrow ψ inferir ψ

$\text{from }\; \phi \;\text{ and }\; \phi \leftrightarrow \psi \;\text{ infer }\; \psi$ y axiomas como

(ϕ \leftrightarrow ψ) \leftrightarrow (ψ \leftrightarrow ϕ) (ϕ \leftrightarrow (x \leftrightarrow ψ)) \leftrightarrow ((ϕ \leftrightarrow x) \leftrightarrow ψ)

$(\phi \leftrightarrow \psi) \;\leftrightarrow\; (\psi \leftrightarrow \phi) \\ (\phi \leftrightarrow (\chi \leftrightarrow \psi)) \;\leftrightarrow\; ((\phi \leftrightarrow \chi) \leftrightarrow \psi)$

Por lo tanto, mi pregunta es: ¿Qué es una axiomatización completa y elegante de la lógica intuicionista proposicional basada en $\;\leftrightarrow, \lor, \bot\;$ ?

usuario14972

Siempre hay "definir

\lor, \to

$\vee, \to$ en términos de eso, y luego usa la buena axiomatización que ya conoces".

hmakholm sobra a Monica

@Hurkyl: Ese parece ser el punto del párrafo "Estrictamente hablando ..." del OP. Estoy de acuerdo en que el resultado de eso difícilmente sería elegante.

dfeuer

¿Quién dice que hay una forma elegante de hacerlo?

MarnixKlooster ReintegroMonica

@dfeuer Nadie, que yo sepa. Espero que haya una manera elegante de hacer esto.

hmakholm sobra a Monica

Estás seguro que

(ϕ \land ψ)

$(\phi\land\psi)$ es intuitivamente equivalente a

(ϕ \lor ψ) \leftrightarrow (ϕ \leftrightarrow ψ)

$(\phi\lor\psi)\leftrightarrow(\phi\leftrightarrow\psi)$ ? Funciona clásicamente, por supuesto, pero no veo cómo se puede derivar

ϕ

$\phi$ de este último de forma intuicionista.

dfeuer

Puede encontrar el tipo de caracterización que está buscando si examina las álgebras de Heyting .

dfeuer

@HenningMakholm, creo que tienes razón, pero no sé lo suficiente para demostrarlo . Supongo que necesito encontrar un álgebra de Heyting en la que no se cumpla. Estoy tratando de encontrar algo en el conjunto de conjuntos abiertos de la línea real, pero incluso expandiendo la expresión

(p \cup q) \leftrightarrow (p \leftrightarrow q)

$(p\cup q)\leftrightarrow(p\leftrightarrow q)$ está demostrando ser un proceso bastante largo y no me está dando nada que parezca tener mucha esperanza de significado intuitivo susceptible de producción de contraejemplo.

hmakholm sobra a Monica

@dfeuer: Los modelos de Kripke pueden ser más fáciles. Desde

ϕ \equiv (A \lor B) \leftrightarrow (A \leftrightarrow B)

$\phi\equiv(A\lor B)\leftrightarrow(A\leftrightarrow B)$ tiene solo dos variables proposicionales, hay solo cuatro posibles estados del mundo. Y no parece posible armar un marco donde

ϕ

$\phi$ alguna vez tiene un valor diferente a

A \land B

$A\land B$ , lo que IIRC debería significar que esta representación de

\land

$\land$ es en realidad intuicionistamente válido. Realmente no produce una derivación de

A

$A$ de

ϕ

$\phi$ , aunque ...

dfeuer

@HenningMakholm, desafortunadamente ahora has volado por encima de mi cabeza. Si es intuicionistamente válido, ¿no significaría eso que tiene que haber una derivación (lo que parece poco probable)?

hmakholm sobra a Monica

@dfeuer: Sí, si es válido, entonces tiene que haber una derivación. Desafortunadamente, la verificación de fuerza bruta de los posibles modelos de Kripke no ayuda a encontrar esa derivación, aunque (a menos que no recuerde cómo funcionan, lo cual es posible) implican que debe haber uno en alguna parte.

dfeuer

Según Wikipedia,

(p \land q) \equiv (((p \lor q) ⟺ p) ⟺ q)

$(p\land q)\equiv (((p\lor q)\iff p)\iff q)$ , pero tampoco tengo idea de dónde viene eso.

hmakholm sobra a Monica

@dfeuer: encontré una prueba; mira mi respuesta

Doug Spoonwood

No creo que "↔" se asocie con la lógica intuicionista, ¿verdad?

Doug Spoonwood

¿La afirmación de Wikipedia implica algo sobre la posibilidad de tal axiomatización, o simplemente implica una afirmación sobre la representabilidad de los conectores?

Respuestas (1)

¿Axiomas basados en ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot para la lógica intuicionista proposicional?

Siempre hay "definir $\vee, \to$ en términos de eso, y luego usa la buena axiomatización que ya conoces".
@Hurkyl: Ese parece ser el punto del párrafo "Estrictamente hablando ..." del OP. Estoy de acuerdo en que el resultado de eso difícilmente sería elegante.
@dfeuer Nadie, que yo sepa. Espero que haya una manera elegante de hacer esto.
Estás seguro que $(\phi\land\psi)$ es intuitivamente equivalente a $(\phi\lor\psi)\leftrightarrow(\phi\leftrightarrow\psi)$ ? Funciona clásicamente, por supuesto, pero no veo cómo se puede derivar $\phi$ de este último de forma intuicionista.
Puede encontrar el tipo de caracterización que está buscando si examina las álgebras de Heyting .
@HenningMakholm, creo que tienes razón, pero no sé lo suficiente para demostrarlo . Supongo que necesito encontrar un álgebra de Heyting en la que no se cumpla. Estoy tratando de encontrar algo en el conjunto de conjuntos abiertos de la línea real, pero incluso expandiendo la expresión $(p\cup q)\leftrightarrow(p\leftrightarrow q)$ está demostrando ser un proceso bastante largo y no me está dando nada que parezca tener mucha esperanza de significado intuitivo susceptible de producción de contraejemplo.
@dfeuer: Los modelos de Kripke pueden ser más fáciles. Desde $\phi\equiv(A\lor B)\leftrightarrow(A\leftrightarrow B)$ tiene solo dos variables proposicionales, hay solo cuatro posibles estados del mundo. Y no parece posible armar un marco donde $\phi$ alguna vez tiene un valor diferente a $A\land B$ , lo que IIRC debería significar que esta representación de $\land$ es en realidad intuicionistamente válido. Realmente no produce una derivación de $A$ de $\phi$ , aunque ...
@HenningMakholm, desafortunadamente ahora has volado por encima de mi cabeza. Si es intuicionistamente válido, ¿no significaría eso que tiene que haber una derivación (lo que parece poco probable)?
@dfeuer: Sí, si es válido, entonces tiene que haber una derivación. Desafortunadamente, la verificación de fuerza bruta de los posibles modelos de Kripke no ayuda a encontrar esa derivación, aunque (a menos que no recuerde cómo funcionan, lo cual es posible) implican que debe haber uno en alguna parte.
Según Wikipedia, $(p\land q)\equiv (((p\lor q)\iff p)\iff q)$ , pero tampoco tengo idea de dónde viene eso.
No creo que "↔" se asocie con la lógica intuicionista, ¿verdad?
¿La afirmación de Wikipedia implica algo sobre la posibilidad de tal axiomatización, o simplemente implica una afirmación sobre la representabilidad de los conectores?

hmakholm sobra a Monica · Answer 1

¿Qué tal un cálculo secuencial, con reglas estándar?

\frac{Γ, PAG, PAG ⊢ q}{Γ, PAG ⊢ q} C L \frac{}{Γ, PAG ⊢ PAG} A X \frac{}{Γ, ⊥ ⊢ PAG} ⊥ L

$\frac{\Gamma, P, P\vdash Q}{\Gamma, P\vdash Q}CL \qquad \frac{}{\Gamma,P \vdash P}Ax \qquad \frac{}{\Gamma, \bot \vdash P}{\bot}L$

\frac{Γ ⊢ q Γ, PAG ⊢ R}{Γ, PAG \leftrightarrow q ⊢ R} \leftrightarrow L_{1} \frac{Γ ⊢ PAG Γ, q ⊢ R}{Γ, PAG \leftrightarrow q ⊢ R} \leftrightarrow L_{2} \frac{Γ, PAG ⊢ q Γ, q ⊢ PAG}{Γ ⊢ PAG \leftrightarrow q} \leftrightarrow R

$\frac{\Gamma\vdash Q\quad \Gamma,P\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_1 \quad \frac{\Gamma\vdash P\quad \Gamma,Q\vdash R}{\Gamma,P\leftrightarrow Q\vdash R}{\leftrightarrow}L_2 \quad \frac{\Gamma,P\vdash Q\quad \Gamma,Q\vdash P}{\Gamma\vdash P\leftrightarrow Q}{\leftrightarrow}R$

\frac{Γ, PAG ⊢ R Γ, q ⊢ R}{Γ, PAG \lor q ⊢ R} \lor L \frac{Γ ⊢ PAG}{Γ ⊢ PAG \lor q} \lor R_{1} \frac{Γ ⊢ q}{Γ ⊢ PAG \lor q} \lor R_{2}

$\frac{\Gamma,P\vdash R \quad \Gamma,Q\vdash R}{\Gamma,P\lor Q\vdash R}{\lor}L \quad \frac{\Gamma\vdash P}{\Gamma\vdash P\lor Q}{\lor}R_1 \quad \frac{\Gamma\vdash Q}{\Gamma\vdash P\lor Q}{\lor}R_2$ Esto es completo para el

{\leftrightarrow, \lor, ⊥}

$\{{\leftrightarrow},{\lor},\bot\}$ fragmento porque el cálculo secuente intuicionista completo satisface la eliminación cortada.

Para mostrar que este fragmento es completo en expresividad , expresa $P\to Q$ como $(P\lor Q)\leftrightarrow Q$ -- esta equivalencia es intuicionistamente válida, y las reglas usuales de izquierda y derecha para $\to$ se construyen fácilmente como combinaciones de las reglas anteriores.

Similarmente, $\neg P$ es por supuesto equivalente a $P\leftrightarrow \bot$ .

Por conjunción, contrariamente a la especulación en los comentarios, resulta que $(P\lor Q)\leftrightarrow(P\leftrightarrow Q)$ es de hecho intuicionistamente equivalente a $P\land Q$ . La dirección difícil es ver que lo habitual ${\land}L$ regla es admisible, lo que se puede hacer de la siguiente manera en el cálculo secuencial anterior:

\begin{aligned} 0. & Γ, PAG, q ⊢ R & premisa de la regla derivada \\ 1. & PAG ⊢ PAG \lor q & fácil \\ 2. & PAG \leftrightarrow q, PAG ⊢ q & fácil \\ 3. & (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q), PAG ⊢ q & 1, 2, \leftrightarrow L_{2} \\ 4. & (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q), q ⊢ PAG & mutatis mutandis \\ 5. & (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q) ⊢ PAG \leftrightarrow q & 3, 4, \leftrightarrow R \\ 6. & PAG \lor q ⊢ PAG \lor q & axioma \\ 7. & Γ, PAG \lor q, PAG \leftrightarrow q ⊢ R & fácil consecuencia de 0 \\ 8. & Γ, (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q), PAG \lor q ⊢ R & 6, 7, \leftrightarrow L_{2} \\ 9. & Γ, (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q), (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q) ⊢ R & 5, 8, \leftrightarrow L_{1} \\ 10 & Γ, (PAG \lor q) \leftrightarrow (PAG \leftrightarrow q) ⊢ R & 9, C L \end{aligned}

$\begin{array}{rll} 0. & \Gamma,~ P,~ Q \vdash R & \text{premise of derived rule} \\ 1. & P\vdash P\lor Q & \text{easy} \\ 2. & P\leftrightarrow Q,~ P \vdash Q & \text{easy} \\ 3. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P \vdash Q & 1, 2, {\leftrightarrow}L_2 \\ 4. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ Q \vdash P & \text{mutatis mutandis} \\ 5. & (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash P\leftrightarrow Q & 3,4, {\leftrightarrow}R \\ 6. & P\lor Q \vdash P\lor Q & \text{axiom} \\ 7. & \Gamma,~ P\lor Q,~ P\leftrightarrow Q \vdash R & \text{easy consequence of }0 \\ 8. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ P\lor Q \vdash R & 6,7, {\leftrightarrow}L_2 \\ 9. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q),~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 5,8, {\leftrightarrow}L_1 \\ 10. & \Gamma,~ (P\lor Q)\leftrightarrow(P\leftrightarrow Q) \vdash R & 9, CL \end{array}$

(¡Prueba encontrada por búsqueda exhaustiva!)

O, para aquellos que favorecen el isomorfismo de Curry-Howard para pruebas intuicionistas, la idea en pseudosintaxis tipo Haskell para el ${\leftrightarrow}{\lor}{\bot}$ fragmento es para reemplazar

conj :: (P,Q)
let (x::P,y::Q) = conj
in  <..x..y..>

por

conj :: (Either P Q) <-> (P <-> Q)
let eq1 :: P <-> Q
    eq1 (x :: P) = let eq2 :: P <-> Q = conj (Left x) in eq2 x
    eq1 (y :: Q) = let eq2 :: P <-> Q = conj (Right y) in eq2 y
    disj :: Either P Q = conj eq1
in case disj of
     Left(x::P) -> let y::Q = eq1 x in <..x..y..>
     Right(y::Q) -> let x::P = eq1 y in <..x..y..>

donde P <-> Qse supone que se comporta como una función que se puede aplicar a Po Qy produce una salida del tipo opuesto, y la disyunción está representada por el Eithertipo estándar.

que reglas son $\leftrightarrow L$ y $\leftrightarrow R$ , ¿exactamente?
Tal vez soy tonto, pero ¿cómo $\Gamma,P,Q\vdash R$ tiene sentido como premisa?
@dfeuer: El objetivo aquí es construir $\frac{Γ, PAG, q ⊢ R}{Γ, PAG \land q ⊢ R} \land L$ $\frac{\Gamma, P, Q\vdash R}{\Gamma,~P\land Q\vdash R}{\land}L$ como regla derivada. Si solo quieres derivar $P\land Q\vdash P$ , reemplazar $R$ con $P$ y deja $\Gamma$ estar vacío
Lo he leído un poco más detenidamente ahora. Parece que los pasos clave son realmente 3 a 5, y el resto se construye y se desmonta. ¿Es eso correcto?
@dfeuer: Creo que sí, aunque los "pasos clave" son, por supuesto, subjetivos. Se podría argumentar que la inferencia que concluye 9 también es bastante clave: "Ahora que hemos probado $P\leftrightarrow Q$ , nuestra codificación de $P\land Q$ nos dice que también tenemos $P\lor Q$ ". En mi opinión, ahí es cuando empezamos a saber algo positivo . Pero, por otro lado, fue fácil desde el principio ver que podríamos hacer eso si solo pudiéramos probar $P\leftrightarrow Q$ , por lo que los pasos 3-5 son de hecho lo que requirió inspiración (o más bien, para mí, fuerza bruta) para encontrar.

¿Axiomas basados en ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot para la lógica intuicionista proposicional?

MarnixKlooster ReintegroMonica

usuario14972

hmakholm sobra a Monica

dfeuer

MarnixKlooster ReintegroMonica

hmakholm sobra a Monica

dfeuer

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

Doug Spoonwood

Doug Spoonwood

Respuestas (1)

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

Derivación axiomática: ¿qué implica prácticamente la instanciación de un axioma?

¿Las tablas de verdad para los conectores lógicos se deducen de los axiomas en la lógica proposicional?

Diferencia entre axiomas lógicos y reglas de inferencia

¿Cómo decidimos qué axiomas son necesarios?

Necesito ayuda con respecto a una prueba en First Order Logic

Las teorías de máxima consistencia tienen subteorías contables completas en cada sublenguaje contable.

¿Probar la solidez de la lógica proposicional sin usar la inducción?

¿Cómo se sabe si A⟹BA⟹BA \implica que B (una implicación) es verdadera sin saber si BBB (el consecuente) es verdadera?

Notaciones equivalentes aparentes para el axioma del infinito

¿Bajo qué condiciones un sistema de prueba axiomática tiene un equivalente de deducción natural?

¿Axiomas basados ​​en ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot para la lógica intuicionista proposicional?

MarnixKlooster ReintegroMonica

usuario14972

hmakholm sobra a Monica

dfeuer

MarnixKlooster ReintegroMonica

hmakholm sobra a Monica

dfeuer

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

Doug Spoonwood

Doug Spoonwood

Respuestas (1)

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

dfeuer

hmakholm sobra a Monica

¿Axiomas basados en ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot para la lógica intuicionista proposicional?