Makkai's work my fit: "First Order Logic with Dependent Sorts,with Applications to Category Theory"
"For instance, the definition of elementary topos (with operations defined by universal properties up to isomorphism, not specified as
univalued operations) can be given as a finite set of sentences in FOLDS."
Interesting find, but again an example of where you first need to learn some new logic FOLDS ("FOLDS has the first two of these, contexts and types (although the latter are called 'sorts'), but it does not have the third, terms (except in the rudimentary form of mere variables), and it has equality in a greatly restricted form only.").
I wonder if it is impossible to describe a topos as a normal axiom system of first-order logic, or if people are just unwilling to do it.
Comments
Makkai's work my fit: "First Order Logic with Dependent Sorts,with Applications to Category Theory"
"For instance, the definition of elementary topos (with operations defined by universal properties up to isomorphism, not specified as univalued operations) can be given as a finite set of sentences in FOLDS."
https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
Interesting find, but again an example of where you first need to learn some new logic FOLDS ("FOLDS has the first two of these, contexts and types (although the latter are called 'sorts'), but it does not have the third, terms (except in the rudimentary form of mere variables), and it has equality in a greatly restricted form only.").
I wonder if it is impossible to describe a topos as a normal axiom system of first-order logic, or if people are just unwilling to do it.