Creo que la respuesta a su pregunta está en el Álgebra Lindenbaum que es un álgebra booleana (y espacio topológico) que se asocia de forma natural con cualquier lenguaje formal y que proporciona una forma de pensar sobre el contenido informativo de una aserción. Visto así, el contenido informativo de una aserción no es un número real, sino un elemento de un álgebra booleana, el álgebra de Lindenbaum. En términos más generales, el contenido informativo de un conjunto de afirmaciones es un filtro de esta álgebra.
A saber, considere el conjunto L de todas las aserciones del lenguaje. Y considere cualquier teoría T en este lenguaje. (Por cierto, el uso que hace del término "universo" en este contexto es muy poco habitual. universo se considera casi universalmente una noción semántica, que se refiere a un modelo o estructura que satisface algunas afirmaciones; en cambio, lo que usted tiene es un concepto sintáctico, un teoría que es una colección de afirmaciones).
Podemos definir naturalmente una relación de equivalencia sobre las afirmaciones, relativa a la base de la teoría T, donde φ ≡ ψ si T demuestra que φ y ψ son equivalentes. La colección de clases de equivalencia forma un álgebra booleana, donde [φ] ∧ [ψ] = [φ ∧ ψ] y ¬[φ] = [¬φ]. En particular, existe también el orden que viene con cualquier álgebra booleana, que equivale a φ <= ψ sólo en el caso de que T demuestre que ψ implica φ.
Para cada afirmación ψ, sea F ψ sea el conjunto de todas las consecuencias de ψ sobre la teoría T. Este es, por supuesto, el verdadero "contenido informativo" de ψ en relación con T. Se trata de un filtro (principal) en el álgebra de Lindenbaum.
En términos más generales,
-
Si S es una teoría que extiende T, entonces los elementos del álgebra de Lindenbaum sobre T correspondientes a teoremas de S forman un filtro.
-
En este caso, el álgebra de Lindenbaum de S es el cociente del álgebra de T módulo a este filtro.
-
Si S es una teoría completa, entonces el filtro es un ultrafiltro.
-
El espacio de Stone (que es compacto, Hausdorff, totalmente desconectado, con una base clopen) es el conjunto de todos los ultrafiltros, y podemos asociar cualquier filtro (y por lo tanto cualquier declaración φ) con la colección de todos los ultrafiltros que lo contienen.
Volviendo a tu pregunta. Si tengo una colección de axiomas A, entonces puedo considerar el filtro F A que generan en el álgebra de Lindenbaum de T. Este filtro es exactamente el mismo que el conjunto de clases de equivalencia de consecuencias de A sobre T, y podría decirse que es el contenido exacto de información de A sobre T.
Para cualquier conjunto de axiomas A, el contenido informativo F A es precisamente la unión F φ 1 ∧ ... ∧ φ n donde cada φ i está en A. Pero equivalentemente, podríamos haber dicho: donde cada φ i es un teorema de A. Y debido a esto, cualquier colección de axiomas que conduzca al mismo conjunto de teoremas tendrá exactamente lo mismo contenido informativo, en el sentido de que el filtro que se genere será exactamente el mismo.
En particular, se utiliza una operación + para añadir "contenido informativo", y en este contexto, puesto que estamos utilizando filtros F para medir la información, definimos naturalmente F + G como el filtro generado por F y G juntos. En este caso, he explicado que cualquier elección de axiomas que conduzca a los mismos teoremas tendrá exactamente la misma suma de contenido de información. Por lo tanto, supongo que es correcto decir que todos ellos también minimizan esa suma.
Puede leer más sobre el álgebra de Lindenbaum en Lógica, inducción y conjuntos por Thomas Forster. Además, hay muchas conexiones con el concepto de teoría de tipos .
Acabo de fijarme en la parte final de tu pregunta, sobre la redundancia en los axiomas. Para esto, creo que el álgebra de Lindenbaum también es la forma correcta de pensar. Si tienes una lista de axiomas φ 0 , φ 1 ..., entonces se puede eliminar fácilmente cualquier redundancia sustituyendo cada afirmación φ n con la declaración ψ n que afirma: "o bien φ n o algún φ anterior i fracasa". Si uno elimina las validaciones lógicas de la nueva lista de axiomas, entonces es un ejercicio que ninguno de ellos implica a otro, y de hecho, ninguna colección de los nuevos axiomas implica nada fuera de esa colección. Estas operaciones son el análogo algebraico booleano de la "disjunción" que a veces se produce al tomar uniones de conjuntos superpuestos.
