1.10. Formalización de la teoría de conjuntos
El predicado de inclusión
El predicado de inclusión ⊂ entre dos conjuntos E y F,
se define como E ⊂ F ⇔
(∀x∈E, x
∈ F).
Se lee como: E está incluido en F, o E
es un subconjunto de F, o F incluye E.
Siempre tenemos E ⊂ E (ya que esto significa: ∀x, x ∈ E ⇒ x ∈ E).
Las cadenas de implicaciones también aparecen como cadenas de inclusión:
(E ⊂ F ⊂ G) ⇔ (E ⊂ F
∧ F ⊂ G) ⇒ E ⊂ G.
La traducción del definidor en la lógica de primer orden
La traducción del definidor en la lógica de primer orden
La traducción de la teoría de conjuntos en una teoría genérica convierte la
el definidor de la función en una infinidad de símbolos de operador: para
cada término t con un argumento (y los parámetros), la expresión completa
(E ∋ x ↦ t(x)) es vista como el nombre grande de un símbolo de operador
distinto, cuyos argumentos son E y los parámetros de t. (Aquellos en los que
cada subexpresión de t sin ninguna ocurrencia de x es la única ocurrencia
de un parámetro, sería suficiente para definir los otros). Lo mismo pasa
con el constructor del grupo, que aparecerá como un caso particular en 1.11.
De esta forma, la lista de los axiomas de la teoría de conjuntos puede
considerarse como la lista de los axiomas de la teoría genérica en la teoría
de conjuntos en la que se convierte. Todos los axiomas que dependen de una
expresión (un término para el definidor o una fórmula para el constructor
de conjunto) son esquemas de axiomas. (Un esquema de las reclamaciones,
es decir, axiomas o teoremas es una lista infinita de reclamaciones,
generalmente obtenida sustituyendo un símbolo extra de la estructura por
cualquier expresión posible difinida).
Primeros axiomas.
∀x,
∀Fnc x, |
¬(Set(x) ∧ Fnc(x))
Set(Dom x) |
∀E,
∀(parameteros),
∀SetE, ∀SetF, |
Fnc(E ∋ x ↦ t(x)) para cualquier termino t
E ⊂ F ⊂ E ⇒ E=F
(Axioma de Extensionalidad). |
El último redefine la igualdad entre los conjuntos de su equivalencia como
clases (dejando los elementos en la lista): E ⊂ F ⊂ E significa que E y F tienen los mismos
elementos (∀ x, x ∈ E ⇔ x ∈ F) así que para cualquier predicado R ,
(∀x ∈ F, R(x)) ⇔ (∀x
∈ E, R(x))
y lo mismo para ∃.
Axiomas para funciones. Para cualquier functor t (para ser reemplazado por
todos los términos que pueden definirlos), tenemos los siguientes axiomas
en los que el primero resume los otros 3: para todos los valores de los
parámetros de t, cualquier conjunto E incluido en la clase de definitud de t
(esta condición ∀x∈E, dt(x) es la condición de definitud para
(E ∋ x ↦ t(x))), y todas las funciones f y g,
f = (E ∋ x ↦ t(x))
⇔ ( Dom f = E ∧ (∀x∈E, f(x)
= t(x)))
Dom (E ∋ x ↦ t(x)) = E
∀x ∈ E, (E ∋ y ↦ t(y))
(x) = t(x)
(Dom f = Dom g ∧ ∀x∈Dom f, f(x)
= g(x)) ⇒ f = g
Un principio general para la formalización de la teoría de conjuntos
Para cualquier tipo de meta-objetos expresables indirectamente y utilizables
como objetos en expresiones, la teoría de conjuntos se enriquecerá con
las herramientas para presentarlas de una manera directa como objetos.
Es decir, las clases que se portan como conjuntos serán convertibles
en conjuntos (1.11), y los elementos indirectamente especificadas serán
directamente especificados (2.4). Pero cuando la expresión indirecta de
meta-objetos (aquí functores) puede ejecutarse sobre la infinidad de las
posibles expresiones (aquí cualquier término), se necesita otra razón
para ver todos estos meta-objetos como objetos definidos de un único tipo
(funciones): la razón aquí es que los dominios de estos functores son
conjuntos, dados como un argumento al definidor. Al contrario, no puede
existir una clase de todos los functores, ni de todas las clases:
ingenuamente tratando a insertalo en el mismo universo podría llevar a
contradicciones por razonamientos como la demostración de la paradoja de
Russell.
Los meta-objetos que se comportan como objetos con otra tarea más allá de
conjuntos y funciones, se representarán como otro tipo de objetos
(operaciones, relaciones, tuplas) y las herramientas de conversión de papeles
(meta-objetos) a los objetos se completarán por las nuevas herramientas de
conversión de objetos en sus papeles. Pero esto puede ser hecho dentro de la
misma teoría de conjuntos (simplemente desarrollandola), como los objetos ya
presentes (conjuntos o funciones) pueden encontrarse para interpretar de
forma natural los papeles de estos nuevos objetos. Entonces, las nuevas
nociones pueden ser definidas como clases de los objetos existentes
(que ofrecerán sus características expresables a los nuevos objetos),
mientras que las herramientas de la interpretación y definición de objetos
(convertiendo los objetos en sus funciones de meta-objetos y al revés) están
definidas como abreviaturas de algunas expresiones fijas. Entonces, los
únicos functores necesarios de la conversión entre los objetos que
interpretan el papel del mismo meta-objeto por diferentes métodos
(expresiones), se relacionarán los objetos diferentes de los tipos antiguos
que representan de una manera útil de maneras diferentes el mismo objeto del
tipo nuevo.
Formalización de las operaciones y currificación
La noción de la operación n-aria, los objetos que actúan como operadores
n-arios entre los conjuntos de n, se formalizarían por:
- funtores del dominio n (de poco uso práctico);
- un operador (n + 1)-ario de la evaluación (evaluador) escrita en
forma rellenada como f(x1,…,xn), con argumentos una operación
n-aria f y sus n argumentos x1,…,xn;
- un definidor de una operación, conectando n variables a sus
rangos correspondientes en un término.
La noción de operación puede representarse como una clase de funciones, de
la manera siguiente llamada currificación. El papel de la operación
definidor (conexión de n variables) es interpretado por la sucesión de
n utilizaciones del definidor de una función (uno para cada variable
ligada); y de misma manera como un evaluador, n usos del evaluador de
funcion. Por ejemplo (n = 2), la operación binaria f definida por el término
(predicado binario) t con argumentos x en E e y en F, puede ser formalizada por
f ≈ (E ∋ x ↦
(F ∋ y ↦ t(x,y))) = g
f(x,y) = g(x)(y) = t(x,y)
La función intermedia g(x) = (F ∋ y
↦ t(x,y)) con argumento y, visto x como fijo e y como ligado. Pero esto rompe la simetría entre los
argumentos, y pierde los datos de F cuando E está vacío, pero no al revés.
Una formalización sin estos defectos será posible usando las tuplas (2.1.).
La formalización de las relaciones n-arias implica un predicado (n+1)-ario
de evaluación, y un definidor que conecta n variables a una fórmula.
También podemos ver tanto las relaciones n-arias como casos particulares de
las operaciones n-arias (que representan Booleanos como objetos), como ver
las operaciones de n-arias como casos particulares de relaciones (n + 1)-arios
(ver 2.3). Y al igual que las operaciones, las relaciones pueden reducirse
al caso unario de 2 formas: por currificación (con n-1 usos del definidor de
la función y 1 uso de constructor de conjuntos, como se hará en 2.3 con n = 2),
o utilizando tuplas (2.1).
Other languages:
FR : 1.10. Formalisation de
la théorie des ensembles