En matemáticas , un álgebra de Heyting (también conocida como álgebra pseudo-booleana [1] ) es una red acotada (con operaciones de unión y encuentro escritas ∨ y ∧ y con el elemento mínimo 0 y el elemento mayor 1) equipado con una operación binaria a → b de implicación tal que ( c ∧ a ) ≤ b es equivalente ac ≤ ( a → b ). Desde un punto de vista lógico, A → B es por esta definición la proposición más débil para la cual modus ponens, la regla de inferencia A → B , A ⊢ B , es correcta. Como las álgebras de Boole , las álgebras de Heyting forman una variedad axiomatizable con un número finito de ecuaciones. Las álgebras de Heyting fueron introducidas por Arend Heyting ( 1930 ) para formalizar la lógica intuicionista .
Como retículas, las álgebras de Heyting son distributivas . Cada álgebra booleana es un álgebra de Heyting cuando a → b se define como de costumbre como ¬ a ∨ b , al igual que todo retículo distributivo completo que satisface una ley distributiva infinita unilateral cuando a → b se toma como el supremo del conjunto de todos c para lo cual c ∧ a ≤ b . En el caso finito, cada retícula distributiva no vacía, en particular cada cadena finita no vacía , es automáticamente completa y completamente distributiva y, por tanto, es un álgebra de Heyting.
Se deduce de la definición que 1 ≤ 0 → a , correspondiente a la intuición de que cualquier proposición a está implicada por una contradicción 0. Aunque la operación de negación ¬ a no es parte de la definición, se puede definir como a → 0. El intuitivo El contenido de ¬ a es la proposición de que asumir a conduciría a una contradicción. La definición implica que a ∧ ¬ a = 0. Puede demostrarse además que a ≤ ¬¬ a , aunque lo contrario, ¬¬ a ≤ a , no es cierto en general, es decir, la eliminación de la doble negación no se cumple en general. en un álgebra de Heyting.
Las álgebras de Heyting generalizan las álgebras booleanas en el sentido de que una álgebra de Heyting que satisface a ∨ ¬ a = 1 ( centro excluido ), equivalentemente ¬¬ a = a ( eliminación de doble negación ), es un álgebra booleana. Los elementos de un álgebra de Heyting H de la forma ¬ a comprenden una red booleana, pero en general no es una subálgebra de H (ver más abajo ).
Las álgebras de Heyting sirven como modelos algebraicos de la lógica intuicionista proposicional de la misma manera que las álgebras booleanas modelan la lógica clásica proposicional . La lógica interna de un topos elemental se basa en el álgebra de Heyting de subobjetos del objeto terminal 1 ordenados por inclusión, equivalentemente los morfismos de 1 al clasificador de subobjetos Ω.
Los conjuntos abiertos de cualquier espacio topológico forman un álgebra de Heyting completa . Las álgebras de Heyting completas se convierten así en un objeto central de estudio en la topología sin sentido .
Cada álgebra de Heyting cuyo conjunto de elementos no mayores tiene un elemento mayor (y forma otra álgebra de Heyting) es subdirectamente irreductible , por lo que cada álgebra de Heyting puede hacerse subdirectamente irreductible mediante la unión de un nuevo elemento mayor. De ello se deduce que incluso entre las álgebras finitas de Heyting existen infinitos que son subdirectamente irreductibles, de los cuales no hay dos que tengan la misma teoría ecuacional. Por tanto, ningún conjunto finito de álgebras de Heyting finitas puede proporcionar todos los contraejemplos de las no leyes del álgebra de Heyting. Esto está en marcado contraste con las álgebras de Boole, cuya única subdirección irreductible es la de dos elementos, que por sí sola, por lo tanto, es suficiente para todos los contraejemplos de las no leyes del álgebra de Boole, la base del método de decisión de tabla de verdad simple . Sin embargo, es decidible si una ecuación es válida para todas las álgebras de Heyting. [2]
Las álgebras de Heyting se denominan con menos frecuencia álgebras pseudo-booleanas , [3] o incluso retículas de Brouwer , [4] aunque este último término puede denotar la definición dual, [5] o tener un significado un poco más general. [6]
Definicion formal
Un álgebra de Heyting H es un retículo acotado tal que para todo a y b en H hay un elemento mayor x de H tal que
Este elemento es el pseudocomplemento relativo de a con respecto a b , y se denota a → b . Escribimos 1 y 0 para el elemento más grande y más pequeño de H , respectivamente.
En cualquier álgebra de Heyting, se define el pseudo-complemento ¬ a de cualquier elemento a estableciendo ¬ a = ( a → 0). Por definición,, y ¬ a es el elemento más grande que tiene esta propiedad. Sin embargo, en general no es cierto que, por lo tanto, ¬ es solo un pseudocomplemento, no un complemento verdadero , como sería el caso en un álgebra booleana.
Un álgebra de Heyting completa es un álgebra de Heyting que es una celosía completa .
Una subálgebra de un álgebra de Heyting H es un subconjunto H 1 de H que contiene 0 y 1 y se cierra bajo las operaciones ∧, ∨ y →. De ello se deduce que también está cerrado bajo ¬. Una subálgebra se convierte en un álgebra de Heyting mediante las operaciones inducidas.
Definiciones alternativas
Definición teórica de categorías
Un álgebra de Heyting es una celosía acotada que tiene todos los objetos exponenciales .
La celosía se considera una categoría donde se encuentran,, es el producto . La condición exponencial significa que para cualquier objeto y en un exponencial existe de forma única como un objeto en .
Una implicación de Heyting (a menudo escrita con o para evitar confusiones como el uso de para indicar un functor ) es solo un exponencial: es una notación alternativa para . De la definición de exponenciales tenemos esa implicación () está justo al lado de cumplir (). Este adjunto se puede escribir como o más completamente como:
Definiciones de la teoría de celosía
Se puede dar una definición equivalente de las álgebras de Heyting considerando las asignaciones:
para algunos fija una en H . Un retículo acotado H es un álgebra de Heyting si y solo si cada mapeo f a es el adjunto inferior de una conexión de Galois monótona . En este caso, el adjunto superior respectivo g a viene dado por g a ( x ) = a → x , donde → se define como antes.
Otra definición más es como una celosía residual cuya operación monoide es ∧. La unidad de monoide debe ser entonces el elemento superior 1. La conmutatividad de este monoide implica que los dos residuos coinciden como a → b .
Celosía acotada con una operación de implicación
Dada una red acotada A con elementos más grandes y más pequeños 1 y 0, y una operación binaria →, estos juntos forman un álgebra de Heyting si y solo si se cumple lo siguiente:
donde 4 es la ley distributiva para →.
Caracterización utilizando los axiomas de la lógica intuicionista
Esta caracterización de las álgebras de Heyting hace que la prueba de los hechos básicos relacionados con la relación entre el cálculo proposicional intuicionista y las álgebras de Heyting sea inmediata. (Para estos hechos, consulte las secciones " Identidades probables " y " Construcciones universales ".) Uno debe pensar en el elementocomo significando, intuitivamente, "demostrablemente cierto". Compare con los axiomas en Lógica intuicionista # Axiomatización ).
Dado un conjunto A con tres operaciones binarias →, ∧ y ∨, y dos elementos distinguidos y , entonces A es un álgebra de Heyting para estas operaciones (y la relación ≤ definida por la condición de quecuando a → b =) si y solo si se cumplen las siguientes condiciones para cualquier elemento x , y y z de A :
Finalmente, definimos ¬ x como x →.
La condición 1 dice que deben identificarse fórmulas equivalentes. La condición 2 dice que las fórmulas comprobablemente verdaderas se cierran bajo modus ponens . Las condiciones 3 y 4 son entonces condiciones. Las condiciones 5, 6 y 7 son y condiciones. Las condiciones 8, 9 y 10 son o condiciones. La condición 11 es una condición falsa .
Por supuesto, si se eligiera un conjunto diferente de axiomas para la lógica, podríamos modificar el nuestro en consecuencia.
Ejemplos de
- Todo álgebra de Boole es un álgebra de Heyting, con p → q dado por ¬ p ∨ q .
- Cada conjunto totalmente ordenado que tiene un elemento mínimo 0 y un elemento mayor 1 es un álgebra de Heyting (si se ve como una red). En este caso p → q es igual a 1 cuando p≤q , y q en caso contrario.
- El álgebra de Heyting más simple que aún no es un álgebra booleana es el conjunto totalmente ordenado {0, 1/2, 1} (visto como una celosía), produciendo las operaciones: Ba
0 1/2 1 0 0 0 0 1/2 0 1/2 1/2 1 0 1/2 1 Ba0 1/2 1 0 0 1/2 1 1/2 1/2 1/2 1 1 1 1 1 a → b Ba0 1/2 1 0 1 1 1 1/2 0 1 1 1 0 1/2 1 a ¬ a 0 1 1/2 0 1 0 En este ejemplo, eso 1/2∨¬ 1/2 = 1/2∨ ( 1/2 → 0) = 1/2∨0 = 1/2 Falsifica la ley del medio excluido.
- Cada topología proporciona un álgebra de Heyting completa en forma de celosía de conjuntos abiertos . En este caso, el elemento de A → B es el interior de la unión de un C y B , donde A c denota el complemento del conjunto abierto A . No todas las álgebras de Heyting completas son de esta forma. Estos problemas se estudian en topología sin sentido , donde las álgebras de Heyting completas también se denominan marcos o localizaciones .
- Cada álgebra interior proporciona un álgebra de Heyting en la forma de su celosía de elementos abiertos. Cada álgebra de Heyting tiene esta forma, ya que un álgebra de Heyting se puede completar a un álgebra booleana tomando su extensión booleana libre como una red distributiva acotada y luego tratándola como una topología generalizada en esta álgebra booleana.
- El álgebra de Lindenbaum de la lógica intuicionista proposicional es un álgebra de Heyting.
- Los elementos globales del clasificador de subobjetos Ω de un topos elemental forman un álgebra de Heyting; es el álgebra de Heyting de valores de verdad de la lógica intuicionista de orden superior inducida por el topos.
- Las álgebras de Łukasiewicz-Moisil (LM n ) también son álgebras de Heyting para cualquier n [7] (pero no son álgebras MV para n ≥ 5 [8] ).
Propiedades
Propiedades generales
El ordenamiento en un álgebra de Heyting, H se puede recuperar de la operación → de la siguiente manera: para cualquier elemento a , b de H ,si y solo si a → b = 1.
En contraste con algunas lógicas de muchos valores , las álgebras de Heyting comparten la siguiente propiedad con las álgebras de Boole: si la negación tiene un punto fijo (es decir, ¬ a = a para alguna a ), entonces el álgebra de Heyting es el álgebra de Heyting trivial de un elemento.
Identidades demostrables
Dada una fórmula del cálculo proposicional (utilizando, además de las variables, las conectivas , y las constantes 0 y 1), es un hecho, demostrado desde el principio en cualquier estudio de álgebras de Heyting, que las dos condiciones siguientes son equivalentes:
- La fórmula F es probadamente cierta en el cálculo proposicional intuicionista.
- La identidad es cierto para cualquier álgebra H de Heyting y cualquier elemento.
La metaimplicación 1 ⇒ 2 es extremadamente útil y es el principal método práctico para probar identidades en álgebras de Heyting. En la práctica, se usa con frecuencia el teorema de la deducción en tales demostraciones.
Dado que para cualquier a y b en un álgebra de Heyting H tenemossi y solo si a → b = 1, se sigue de 1 ⇒ 2 que siempre que una fórmula F → G sea probadamente cierta, tenemospara cualquier álgebra H de Heyting y cualquier elemento. (Se deduce del teorema de la deducción que F → G es demostrable [de la nada] si y solo si G es demostrable a partir de F , es decir, si G es una consecuencia demostrable de F ). En particular, si F y G son demostrablemente equivalentes , luego, ya que ≤ es una relación de orden.
1 ⇒ 2 se puede demostrar examinando los axiomas lógicos del sistema de prueba y verificando que su valor es 1 en cualquier álgebra de Heyting, y luego verificando que la aplicación de las reglas de inferencia a expresiones con valor 1 en un álgebra de Heyting da como resultado expresiones con valor 1. Por ejemplo, escojamos el sistema de prueba que tiene modus ponens como su única regla de inferencia, y cuyos axiomas son los del estilo de Hilbert dados en Lógica intuicionista # Axiomatización . Entonces, los hechos a verificar se derivan inmediatamente de la definición de álgebras de Heyting, similar a un axioma, dada anteriormente.
1 ⇒ 2 también proporciona un método para probar que ciertas fórmulas proposicionales, aunque son tautologías en la lógica clásica, no pueden probarse en la lógica proposicional intuicionista. Para demostrar que alguna fórmulano es demostrable, basta con exhibir un álgebra H de Heyting y elementos tal que .
Si se quiere evitar la mención de la lógica, a continuación, en la práctica se hace necesario demostrar que es un lema de una versión del teorema de deducción válida para las álgebra de Heyting: para cualquier elemento de una , b y c de un álgebra de Heyting H , tenemos.
Para obtener más información sobre la metaimplicación 2 ⇒ 1, consulte la sección " Construcciones universales " a continuación.
Distributividad
Las álgebras de Heyting son siempre distributivas . En concreto, siempre tenemos las identidades
La ley distributiva a veces se enuncia como un axioma, pero de hecho se deriva de la existencia de pseudo-complementos relativos. La razón es que, al ser el adjunto inferior de una conexión de Galois , conserva todo suprema existente . La distributividad, a su vez, es solo la preservación del supremo binario por.
Mediante un argumento similar, la siguiente ley distributiva infinita se cumple en cualquier álgebra de Heyting completa:
para cualquier elemento x en H y cualquier subconjunto Y de H . Por el contrario, cualquier retícula completa que satisfaga la ley distributiva infinita anterior es un álgebra de Heyting completa, con
siendo su operación relativa de pseudo-complemento.
Elementos regulares y complementados
Un elemento x de un álgebra de Heyting H se llama regular si se cumple alguna de las siguientes condiciones equivalentes:
- x = ¬¬ x .
- x = ¬ y para algunos y en H .
La equivalencia de estas condiciones puede ser reexpresada simplemente como la identidad ¬¬¬ x = ¬ x , válido para todo x en H .
Elementos x y y de un Heyting algebra H se denominan complementos una a otra si x ∧ y = 0 y x ∨ y = 1. Si existe, tal y es único y debe de hecho ser igual a ¬ x . Llamamos complementado a un elemento x si admite un complemento. Es cierto que si x se complementa, entonces también lo es ¬ x , y entonces x y ¬ x se complementan entre sí. Sin embargo, de manera confusa, incluso si x no se complementa, ¬ x puede tener un complemento (no igual ax ). En cualquier álgebra de Heyting, los elementos 0 y 1 se complementan entre sí. Por ejemplo, es posible que ¬ x sea 0 para cada x diferente de 0, y 1 si x = 0, en cuyo caso 0 y 1 son los únicos elementos regulares.
Cualquier elemento complementado de un álgebra de Heyting es regular, aunque lo contrario no es cierto en general. En particular, 0 y 1 son siempre regulares.
Para cualquier álgebra H de Heyting , las siguientes condiciones son equivalentes:
- H es un álgebra de Boole ;
- cada x en H es regular; [9]
- cada x en H se complementa. [10]
En este caso, el elemento a → b es igual a ¬ a ∨ b .
Los elementos regulares (o complementados) de cualquier álgebra de Heyting H constituyen un álgebra booleana H reg (resp. H comp ), en la que las operaciones ∧, ¬ y →, así como las constantes 0 y 1, coinciden con las de H . En el caso de H borrador , la operación ∨ es también el mismo, por lo tanto, H borrador es una subálgebra de H . Sin embargo, en general, H reg no será una subálgebra de H , porque su operación de unión ∨ reg puede ser diferente de ∨. Para x , y ∈ H reg , tenemos x ∨ reg y = ¬ (¬ x ∧ ¬ y ). Consulte a continuación las condiciones necesarias y suficientes para que ∨ reg coincida con ∨.
Las leyes de De Morgan en un álgebra de Heyting
Una de las dos leyes de De Morgan se satisface en cada álgebra de Heyting, a saber
Sin embargo, la otra ley de De Morgan no siempre se cumple. En cambio, tenemos una ley de Morgan débil:
Las siguientes afirmaciones son equivalentes para todas las álgebras H de Heyting :
- H satisface ambas leyes de De Morgan,
La condición 2 es la otra ley de De Morgan. Condición 6 dice que la operación de unión ∨ reg en el álgebra de Boole H reg de elementos regulares de H coincide con la operación de ∨ H . La condición 7 establece que todos los elementos regulares están complementados, es decir, H reg = H comp .
Demostramos la equivalencia. Claramente, las metaimplicaciones 1 ⇒ 2, 2 ⇒ 3 y 4 ⇒ 5 son triviales. Además, 3 ⇔ 4 y 5 ⇔ 6 resultan simplemente de la primera ley de De Morgan y la definición de elementos regulares. Demostramos que 6 ⇒ 7 tomando ¬ x y ¬¬ x en lugar de x e y en 6 y usando la identidad a ∧ ¬ a = 0. Observe que 2 ⇒ 1 se sigue de la primera ley de De Morgan, y 7 ⇒ 6 resulta del hecho de que la operación de unión ∨ en la subálgebra H comp es solo la restricción de ∨ a H comp , teniendo en cuenta las caracterizaciones que hemos dado de las condiciones 6 y 7. La metaimplicación 5 ⇒ 2 es una consecuencia trivial de la la ley de Morgan, teniendo ¬ x y ¬ y en lugar de x e y en 5.
Las álgebras de Heyting que satisfacen las propiedades anteriores están relacionadas con la lógica de De Morgan de la misma manera que las álgebras de Heyting en general están relacionadas con la lógica intuicionista.
Heyting morfismos de álgebra
Definición
Dados dos Heyting álgebras H 1 y H 2 y un mapeo f : H 1 → H 2 , se dice que ƒ es un morfismo de álgebras de Heyting si, por cualquier elemento de x y y en H 1 , tenemos:
De cualquiera de las últimas tres condiciones (2, 3 o 4) se deduce que f es una función creciente, es decir, que f ( x ) ≤ f ( y ) siempre que x ≤ y .
Suponga que H 1 y H 2 son estructuras con operaciones →, ∧, ∨ (y posiblemente ¬) y constantes 0 y 1, y f es un mapeo sobreyectivo de H 1 a H 2 con propiedades 1 a 4 anteriores. Entonces, si H 1 es un álgebra de Heyting, también lo es H 2 . Esto se deriva de la caracterización de las álgebras de Heyting como retículas acotadas (consideradas como estructuras algebraicas en lugar de conjuntos parcialmente ordenados) con una operación → que satisface ciertas identidades.
Propiedades
El mapa de identidad f ( x ) = x desde cualquier álgebra de Heyting a sí mismo es un morfismo, y el material compuesto g ∘ f de cualesquiera dos morfismos f y g es un morfismo. Por tanto, las álgebras de Heyting forman una categoría .
Ejemplos de
Dada un álgebra de Heyting H y cualquier subálgebra H 1 , el mapeo de inclusión i : H 1 → H es un morfismo.
Para cualquier álgebra de Heyting H , el mapa x ↦ ¬¬ x define un morfismo de H al álgebra de Boole de sus elementos regulares H reg . Esto es no en un morfismo en general de H a sí mismo, ya que la operación de combinación de H reg puede ser diferente de la de H .
Cocientes
Deje H un álgebra de Heyting, y dejar F ⊆ H . Llamamos a F un filtro en H si satisface las siguientes propiedades:
La intersección de cualquier conjunto de filtros en H es nuevamente un filtro. Por lo tanto, dado cualquier subconjunto S de H hay un filtro más pequeño que contiene S . Lo llamamos el filtro generado por S . Si S está vacío, F = {1}. De lo contrario, F es igual al conjunto de x en H tal que existen y 1 , y 2 , ..., y n ∈ S con y 1 ∧ y 2 ∧ ... ∧ y n ≤ x .
Si H es un álgebra de Heyting y F es un filtro en H , definimos una relación ~ en H de la siguiente manera: escribimos x ~ y cuando x → Y y Y → X tanto pertenecen a F . Entonces ∼ es una relación de equivalencia ; escribimos H / F para el conjunto de cocientes . Hay una estructura de álgebra de Heyting única en H / F tal que la sobreyección canónica p F : H → H / F se convierte en un morfismo de álgebra de Heyting. Llamamos a la Heyting algebra H / F del cociente de H por F .
Deje S ser un subconjunto de una Heyting algebra H y dejar que F sea el filtro generado por S . Entonces H / F satisface la siguiente propiedad universal:
- Dado cualquier morfismo de Heyting álgebra f : H → H ' que satisface f ( y ) = 1 para cada y ∈ S , f factores de forma única a través de la surjection canónica p F : H → H / F . Es decir, hay un morfismo único f ′ : H / F → H ′ que satisface f′p F = f . Se dice que el morfismo f ′ es inducido por f .
Sea f : H 1 → H 2 un morfismo de las álgebras de Heyting. El núcleo de f , escrito ker f , es el conjunto f −1 [{1}]. Es un filtro en H 1 . (Se debe tener cuidado porque esta definición, si se aplica a un morfismo de álgebras de Boole, es dual con lo que se llamaría el núcleo del morfismo visto como un morfismo de anillos). Por lo anterior, f induce un morfismo f ′ : H 1 / (ker f ) → H 2 . Es un isomorfismo de H 1 / (ker f ) sobre la subálgebra f [ H 1 ] de H 2 .
Construcciones universales
Heyting álgebra de fórmulas proposicionales en n variables hasta equivalencia intuicionista
La metaimplicación 2 ⇒ 1 en la sección " Identidades probables " se demuestra mostrando que el resultado de la siguiente construcción es en sí mismo un álgebra de Heyting:
- Considere el conjunto L de fórmulas proposicionales en las variables A 1 , A 2 , ..., A n .
- Dotar L con un orden previo ≼ definiendo F ≼ G si G es un (intuitionist) consecuencia lógica de F , es decir, si G es demostrable de F . Es inmediato que ≼ es un pedido por adelantado.
- Considere la relación de equivalencia F ∼ G inducida por el preorden F≼G. (Está definido por F ∼ G si y solo si F ≼ G y G ≼ F. De hecho, ∼ es la relación de equivalencia lógica (intuicionista).)
- Sea H 0 el cociente establecido L / ∼. Esta será la álgebra de Heyting deseada.
- Escribimos [ F ] para la clase de equivalencia de una fórmula F . Operaciones →, ∧, ∨ y ¬ se definen de una manera obvia en L . Verifique que dadas las fórmulas F y G , las clases de equivalencia [ F → G ], [ F ∧ G ], [ F ∨ G ] y [¬ F ] dependen solo de [ F ] y [ G ]. Esto define las operaciones →, ∧, ∨ y ¬ en el cociente conjunto H 0 = L / ∼. Defina además 1 como la clase de enunciados demostrablemente verdaderos, y establezca 0 = [⊥].
- Verifique que H 0 , junto con estas operaciones, sea un álgebra de Heyting. Hacemos esto usando la definición de axioma de álgebras de Heyting. H 0 satisface las condiciones ENTONCES-1 hasta FALSO porque todas las fórmulas de las formas dadas son axiomas de la lógica intuicionista. MODUS-PONENS se deriva del hecho de que si una fórmula ⊤ → F es demostrablemente verdadera, donde ⊤ es demostrablemente verdadera, entonces F es demostrablemente verdadera (mediante la aplicación de la regla de inferencia modus ponens). Finalmente, EQUIV resulta del hecho de que si F → G y G → F son ambos demostrablemente verdaderos, entonces F y G son probables entre sí (mediante la aplicación de la regla de inferencia modus ponens), por lo tanto [ F ] = [ G ] .
Como siempre bajo la definición de axioma de álgebras de Heyting, definimos ≤ en H 0 por la condición de que x ≤ y si y solo si x → y = 1. Dado que, por el teorema de la deducción , una fórmula F → G es probablemente verdadera si y solo si G es demostrable a partir de F , se sigue que [ F ] ≤ [ G ] si y solo si F≼G. En otras palabras, ≤ es la relación de orden en L / ~ inducida por la orden previo ≼ en L .
Álgebra de Heyting gratis en un conjunto arbitrario de generadores
De hecho, la construcción anterior se puede realizar para cualquier conjunto de variables { A i : i ∈ I } (posiblemente infinitas). Se obtiene así el álgebra de Heyting libre sobre las variables { A i }, que de nuevo denotaremos por H 0 . Es libre en el sentido de que, dado cualquier Heyting algebra H dado junto con una familia de sus elementos < un i : i ∈ I >, hay un único morfismo f : H 0 → H satisfacer f ([ A i ]) = una yo . La unicidad de f no es difícil de ver, y su existencia resulta esencialmente de la metaimplicación 1 ⇒ 2 de la sección " Identidades demostrables " anterior, en la forma de su corolario de que siempre que F y G son fórmulas demostrablemente equivalentes, F (〈a i >) = G (< un i >) para cualquier familia de elementos < un i > en H .
Heyting álgebra de fórmulas equivalentes con respecto a una teoría T
Dado un conjunto de fórmulas T en las variables { A i }, vistas como axiomas, la misma construcción podría haberse llevado a cabo con respecto a una relación F ≼ G definida en L para significar que G es una consecuencia demostrable de F y el conjunto de axiomas T . Denotemos por H T el álgebra de Heyting así obtenida. Entonces H T satisface la misma propiedad universal como H 0 anterior, pero con respecto a Heyting álgebra de H y familias de elementos < un i > que satisfacen la propiedad de que J (< un i >) = 1 para cualquier axioma J (< A i > ) en T . (Observemos que H T , tomado con la familia de sus elementos 〈[ A i ]〉, satisface esta propiedad por sí misma.) La existencia y unicidad del morfismo se demuestra de la misma manera que para H 0 , excepto que se debe modificar la metaimplicación 1 ⇒ 2 en " Identidades probables " de modo que 1 dice "probablemente verdadero a partir de T " y 2 dice "cualquier elemento a 1 , a 2 , ..., a n en H que satisfaga las fórmulas de T ".
El álgebra de Heyting H T que acabamos de definir puede verse como un cociente del álgebra de Heyting libre H 0 sobre el mismo conjunto de variables, aplicando la propiedad universal de H 0 con respecto a H T , y la familia de sus elementos 〈[ A i ]〉.
Cada álgebra Heyting es isomorfo a una de la forma H T . Para ver esto, que H sea cualquier álgebra de Heyting, y dejar < un i : i ∈I> ser una familia de elementos de generación de H (por ejemplo, cualquier familia sobreyectiva). Consideremos ahora el conjunto T de las fórmulas J (< A i >) en las variables < A i : i ∈I> tal que J (< un i >) = 1. Entonces obtenemos un morfismo f : H T → H por la propiedad universal de H T , que es claramente sobreyectiva. No es difícil demostrar que f es inyectiva.
Comparación con las álgebras de Lindenbaum
Las construcciones que acabamos de dar juegan un papel completamente análogo con respecto a las álgebras de Heyting al de las álgebras de Lindenbaum con respecto a las álgebras de Boole . De hecho, el álgebra de Lindenbaum B T en las variables { A i } con respecto a los axiomas T es solo nuestro H T ∪ T 1 , donde T 1 es el conjunto de todas las fórmulas de la forma ¬¬ F → F , ya que los axiomas adicionales de T 1 son los únicos que deben agregarse para hacer demostrables todas las tautologías clásicas.
Heyting álgebras aplicadas a la lógica intuicionista
Si uno interpreta los axiomas de la lógica proposicional intuicionista como términos de un álgebra de Heyting, entonces evaluarán al elemento más grande, 1, en cualquier álgebra de Heyting bajo cualquier asignación de valores a las variables de la fórmula. Por ejemplo, ( P ∧ Q ) → P es, por definición del pseudo-complemento, el elemento más grande x tal que. Esta inecuación se satisface para cualquier x , por lo que el mayor de tales x es 1.
Además, la regla de modus ponens nos permite derivar la fórmula Q partir de las fórmulas P y P → Q . Pero en cualquier álgebra de Heyting, si P tiene el valor 1 y P → Q tiene el valor 1, entonces significa que, y entonces ; solo puede ser que Q tenga el valor 1.
Esto significa que si una fórmula es deducible de las leyes de la lógica intuicionista, derivada de sus axiomas por medio de la regla del modus ponens, entonces siempre tendrá el valor 1 en todas las álgebras de Heyting bajo cualquier asignación de valores a las variables de la fórmula. . Sin embargo, se puede construir un álgebra de Heyting en la que el valor de la ley de Peirce no siempre sea 1. Considere el álgebra de 3 elementos {0, 1/2, 1} como se indica arriba. Si asignamos 1/2a P y 0 a Q , entonces el valor de la ley de Peirce (( P → Q ) → P ) → P es 1/2. De ello se sigue que la ley de Peirce no puede derivarse intuicionistamente. Ver isomorfismo de Curry-Howard para el contexto general de lo que esto implica en la teoría de tipos .
También se puede probar lo contrario: si una fórmula siempre tiene el valor 1, entonces es deducible de las leyes de la lógica intuicionista, por lo que las fórmulas intuicionistas válidas son exactamente aquellas que siempre tienen un valor de 1. Esto es similar a la noción que las fórmulas clásicamente válidas son aquellas fórmulas que tienen un valor de 1 en el álgebra booleana de dos elementos bajo cualquier posible asignación de verdadero y falso a las variables de la fórmula, es decir, son fórmulas que son tautologías en el sentido habitual de tabla de verdad. Un álgebra de Heyting, desde el punto de vista lógico, es entonces una generalización del sistema habitual de valores de verdad, y su elemento más grande 1 es análogo a "verdadero". El sistema lógico de dos valores habitual es un caso especial de un álgebra de Heyting, y el más pequeño no trivial, en el que los únicos elementos del álgebra son 1 (verdadero) y 0 (falso).
Problemas de decisión
El problema de si una ecuación dada se cumple en cada álgebra de Heyting fue resuelto por S. Kripke en 1965. [2] La complejidad computacional precisa del problema fue establecida por R. Statman en 1979, quien demostró que era PSPACE-completo. [11] y por lo tanto al menos tan difícil como decidir ecuaciones del álgebra de Boole (mostrado coNP-completo en 1971 por S. Cook) [12] y conjeturado que es considerablemente más difícil. La teoría elemental o de primer orden de las álgebras de Heyting es indecidible. [13] Queda abierto si la teoría universal de Horn de las álgebras de Heyting, o el problema verbal , es decidible. [14] A propósito del problema verbal se sabe que las álgebras de Heyting no son localmente finitas (ninguna álgebra de Heyting generada por un conjunto finito no vacío es finita), en contraste con las álgebras booleanas que son localmente finitas y cuyo problema verbal es decidible. Se desconoce si existen álgebras de Heyting completas libres excepto en el caso de un solo generador donde el álgebra de Heyting libre en un generador se puede completar trivialmente al unir un nuevo top.
Notas
- ^ https://www.encyclopediaofmath.org/index.php/Pseudo-Boolean_algebra
- ↑ a b Kripke, SA: 1965, 'Análisis semántico de la lógica intuicionista I'. En: JN Crossley y MAE Dummett (eds.): Sistemas formales y funciones recursivas. Amsterdam: Holanda Septentrional, págs. 92–130.
- ^ Helena Rasiowa; Roman Sikorski (1963). Las matemáticas de las metamatemáticas . Państwowe Wydawnictwo Naukowe (PWN). págs. 54–62, 93–95, 123–130.
- ^ AG Kusraev; Samson Semenovich Kutateladze (1999). Análisis con valores booleanos . Saltador. pag. 12. ISBN 978-0-7923-5921-0.
- ^ Yankov, VA (2001) [1994], "Celosía de Brouwer" , Enciclopedia de Matemáticas , EMS Press
- ^ Thomas Scott Blyth (2005). Celosías y estructuras algebraicas ordenadas . Saltador. pag. 151. ISBN 978-1-85233-905-0.
- ^ Georgescu, G. (2006). "Lógicas con valores N y Łukasiewicz – Moisil Algebras". Axiomates . 16 : 123. doi : 10.1007 / s10516-005-4145-6 ., Teorema 3.6
- ↑ Iorgulescu, A .: Conexiones entre MV n- álgebras y n -álgebras de Łukasiewicz-Moisil valoradas en n -I. Matemáticas discretas. 181, 155-177 (1998) doi : 10.1016 / S0012-365X (97) 00052-6
- ↑ Rutherford (1965), Th.26.2 p.78.
- ↑ Rutherford (1965), Th.26.1 p.78.
- ^ Statman, R. (1979). "La lógica proposicional intuicionista es espacio polinómico completo". Computación teórica. Sci . 9 : 67–72. doi : 10.1016 / 0304-3975 (79) 90006-9 . hdl : 2027,42 / 23534 .
- ^ Cook, SA (1971). "La complejidad de los procedimientos de demostración de teoremas". págs. 151-158. doi : 10.1145 / 800157.805047 . Parámetro desconocido
|book-title=
ignorado ( ayuda ) - ^ Grzegorczyk, Andrzej (1951). "Indecidibilidad de algunas teorías topológicas" (PDF) . Fundamenta Mathematicae . 38 : 137–52.
- ^ Peter T. Johnstone, Stone Spaces , (1982) Cambridge University Press, Cambridge, ISBN 0-521-23893-5 . (Ver párrafo 4.11)
Ver también
- Topología Alexandrov
- Lógicas superintuicionistas (también conocidas como intermedias)
- Lista de temas de álgebra de Boole
- Álgebra de Ockham
Referencias
- Rutherford, Daniel Edwin (1965). Introducción a la teoría de celosía . Oliver y Boyd. OCLC 224572 .
- F. Borceux, Manual de álgebra categórica 3 , En la Enciclopedia de las matemáticas y sus aplicaciones , Vol. 53, Cambridge University Press, 1994. ISBN 0-521-44180-3OCLC 52238554
- G. Gierz, KH Hoffmann, K. Keimel, JD Lawson, M. Mislove y DS Scott, Continuous Lattices and Domains , In Encyclopedia of Mathematics and its Applications , Vol. 93, Cambridge University Press, 2003.
- S. Ghilardi. Álgebras de Heyting libres como álgebras bi-Heyting , Matemáticas. Rep. Acad. Sci. Canadá XVI., 6: 240–244, 1992.
- Heyting, A. (1930), "Die formalen Regeln der intuitionistischen Logik. I, II, III", Sitzungsberichte Akad. Berlín : 42–56, 57–71, 158–169, JFM 56.0823.01
enlaces externos
- Heyting álgebra en PlanetMath .