Tiene a nadie con éxito axiomatized la categoría de conjuntos finitos? De tal manera que el resultado de la teoría es bi-interpretables con PA.

Question

En los estudios de ZFC, es convencional para tomar la aritmética de Peano (en adelante PA) como la metatheory. Sin embargo, no me gusta la presente convención; creo que un mejor enfoque sería un metatheory (como ZF-aleta con $\in$-inducción, o lo que sea) que se describen $V_\omega$, el universo de hereditariamente finitos conjuntos. Esto crea una interfaz más limpia entre el metatheory y el objeto de la teoría, en mi opinión.

Ahora supongamos que en vez deseen estudiar ETCS. Podríamos tomar la aritmética de Peano como nuestro metatheory; pero, por el argumento anterior, esto probablemente no es la cosa correcta a hacer. Estamos mejor tener un metatheory que describe la categoría de conjuntos finitos. Así que me pregunto: ¿alguien Ha con éxito axiomatized la categoría de conjuntos finitos de tal manera que el resultado de la teoría es bi-interpretables con PA?

Answer 1

No sé si esto se ajusta a tu pregunta, pero la categoría de conjuntos finitos es la libre finitely cocomplete categoría en un objeto. Es decir, si $C$ es una categoría con finito de co-productos y coequalizers, y $X \in C$, que es esencialmente un único functor $F : \mathsf{FinSet} \to C$ preservar finito coequalizers y co-productos tal que $F(\star)=X$ donde $\star \in \mathsf{FinSet}$ es el terminal de objeto. (Para una caracterización de $\mathsf{Set}$, reemplazar "finitely cocomplete" por "cocomplete"). Ver aquí para otra caracterización que involucran el concepto cartesiano de estructura monoidal.