4
$\begingroup$

In studies of ZFC, it is conventional to take Peano arithmetic (hereafter PA) as the metatheory. However, I don't like this convention; I think a better approach would be a metatheory (like ZF-fin with $\in$-induction, or whatnot) that describes $V_\omega$, the universe of hereditarily finite sets. This creates a cleaner interface between the metatheory and the object theory, in my opinion.

Now suppose we instead wish to study ETCS. We could take Peano arithmetic as our metatheory; but, by the above argument, this probably isn't the right thing to do. We're better off having a metatheory that describes the category of finite sets. So I ask: Has anyone successfully axiomatized the category of finite sets in such a way that the resulting theory is bi-interpretable with PA?

$\endgroup$
  • $\begingroup$ This may be helpful: R. Diaconescu and L.A.S. Kirby, Models of arithmetic and categories with finiteness conditions, Annals of Pure and Applied Logic, Volume 35, 1987, Pages 123-148 $\endgroup$ – Lawrence Wong Jan 10 '14 at 9:54
4
$\begingroup$

I don't know if this fits to your question, but the category of finite sets is the free finitely cocomplete category on one object. That is, if $C$ is a category with finite coproducts and coequalizers, and $X \in C$, there is essentially a unique functor $F : \mathsf{FinSet} \to C$ preserving finite coequalizers and coproducts such that $F(\star)=X$, where $\star \in \mathsf{FinSet}$ is the terminal object. (For a characterization of $\mathsf{Set}$, replace "finitely cocomplete" by "cocomplete"). See here for another characterization involving the cartesian monoidal structure.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.