Engineering in Mathematics

Spanish version below

I had no time to invest in this blog, but I managed to gather some to write an invited post in Lawrence Paulson’s Machine Logic.

It is related to new trend of computer formalization of mathematics, in which I have also been working.

You can access it through this link.


Aunque no tuve tiempo para dedicarle al blog, no pude resistirme a la invitación de Lawrence Paulson para escribir un post para el suyo.

Entre otras cosas, está relacionado con la nueva ola de formalización de matemática en computadoras, en lo cual también he trabajado. Pueden leerlo aquí.

El Axioma de Martin

En un post anterior dimos las definiciones básicas de conjuntos densos y filtros genéricos en conjuntos parcialmente ordenados (“posets”), y enunciamos el Teorema de Existencia de Filtro genérico, que copiamos a continuación:

Teorema 1. Si $\mathbb{P}$ es un poset, $\mathcal{D}$ es una familia contable de subconjuntos densos de $\mathbb{P}$ y $p\in\mathbb{P}$, hay un filtro $\mathcal{D}$-genérico $G$ tal que $p\in G$.

La prueba es una construcción recursiva y depende de $\AC$. La siguiente preocupación es saber cuán ajustadas son las hipótesis de este teorema. Por ejemplo, ¿vale si la familia $\mathcal{D}$ no es contable? Respuesta rebuscada: sin salirse del Universo, no. Continue reading

Nociones de Forzamiento

La técnica de forcing o forzamiento permite construir objetos mediante aproximaciones. En general es muy difícil o imposible dar una descripción completa del objeto a construir, pero esto no significa que no haya uno: muchas veces son la mayoría, y la gran idea detrás del forcing es que el objeto “genérico” cumplirá con los requerimientos, con una noción adecuada de genericidad. El Axioma de Martin ($\MA$) asegura que hay objetos genéricos para una variedad de situaciones, y su desarrollo fue en gran medida simultáneo con el forcing. Por eso ahora se usa $\MA$ para motivar este último. Continue reading

Models of the Universe

I promised my friend Zoltán a translation of an older post in Spanish, Modelos del Universo, so here it is. It is almost a literal version.


After some reflection on independence proofs in Set Theory using the method of forcing, one of my conclusions was that it should not be too counterintuitive the fact of adding a new set, i.e., a set not obtainable from previous existing ones using the already established operations of set construction.  For instance, we don’t feel any remorse for taking an arbitrary ring $k$ and adjoining an element transcendental over it, obtaining $k[x]$. Continue reading

Set partition, from Wikimedia Commons

Brevísimo panorama de la Teoría de Conjuntos

Como parte de un plan de trabajo que debí presentar recientemente, incluí una cortísima reseña sobre teoría de conjuntos. Aprovecho el trabajo hecho para compartirla por aquí.


La Teoría de Conjuntos (TC) tiene un doble rol en la matemática: es a la vez su fundamento y dentro de ella es un área de investigación vigente.

En su primera faceta, la TC surgió de entre varios enfoques alternativos (teoría de tipos y el intuicionismo) como respuesta a las contradicciones internas (antinomias) que sacudieron las bases de la matemática a principios del siglo XX. Con el tiempo se estableció como la opción que más se ajustaba a la práctica matemática usual, cristalizándose en los axiomas de Zermelo y Fraenkel con Elección ($\ZF + C = \ZFC$). Continue reading

Modelos del Universo

Después de reflexionar un rato sobre las pruebas de independencia en Teoría de Conjuntos que usan el método de “forzamiento” o forcing, una conclusión que se puede sacar es que no es tan anti-intuitivo poder agregar un conjunto nuevo, i.e., que no se pueda obtener a partir de los ya existentes usando las operaciones usualmente aceptadas de definición de conjuntos. Por ejemplo, no nos produce ninguna inquietud tomar un anillo arbitrario $k$ y adjuntarle un elemento trascendente sobre él, obteniendo $k[x]$.
Continue reading

Naïve set theory

This post is sort of a translation and a follow-up of a post in Spanish about the comparison between naïve and axiomatic set theory.

The point I made in the previous post is that

One leaves naïve set theory in the moment that first order logic (FOL) gets explicit.

Or, from a different perspective, when you realize in full the possibility of different models of set theory.
Continue reading