Validity of equations in a topos

Question

To simplify consider simple algebraic theories (universal algebra) A and L, but the question applies to geometric theories.

1) Syntactically, we can interpret L in A if we can define the operations of L as terms in A, AND then a) prove the axioms of L (which are equations in A) from the axioms of A, or even less, b) argue by any means that the equations hold in any model in Sets (using Choice etc) and then use the (easy) classical completeness theorem for algebraic theories.

2) This, given a model of A, determines a model of L (with same underlying set).

3) In the literature it is accepted that 2) holds for any (say, Grotendieck) topos, not only for models in Set.

4) In fact the proof in 1) a) can be done (or reproduced) directly in the internal language of the topos reasoning with the model (an object with operations etc) as it were a model in Set.

Now, in 1) a) the proofs are accepted to be classical (use excluded middle, etc), and in 1) b) even worst, no need to exhibit a proof in the theory A.

Then, in 3), this classical arguing of 1) a) would, in this case, be valid in any topos ?. And even worst, how can we justify 3) if b) was used in 1).

Help !

The only way out I see is that in 1) a) only intuitionistic logic is accepted, and b) is not accepted, for the validity of 3). But this is not what is usually done in the literature.

e.d.

Answer 1

If I understand the question correctly, it amounts to the following: Suppose I have an equation E (namely the translation of some axiom of L into the language of A) and a set A of identities, i.e., universally quantified equations (namely the axioms of the theory A), and suppose I know that E follows from A under some strong logical and set-theoretic assumptions (excluded middle, axiom of choice). Can I conclude that E follows from A in an intuitionistic type theory of the sort that occurs as the internal logic of a general topos?

The answer is yes, because the deduction of E from A can be carried out in a purely equational logic that is intuitionistically valid. I believe this result is due to Birkhoff. Here's an outline of the argument.

First, form the free algebra F generated by the variables occurring in E using the operations of the language of A (including constants as 0-ary operations). Then form the quotient of F by the smallest congruence relation ~ that makes the assumptions A valid. Since E follows from A in, say, ZFC, we know that E is satisfied in this quotient algebra F/~. (The E that I refer to here is not the universally quantified E but the simple equation E; this is why I used the variables in E as generators of F.) But the congruence ~ can be explicitly generated in a very easy way from A, namely start with the pairs (u,v) where u and v are obtained by instantiating the two sides of an equation from A; then close this set of ordered pairs to produce a congruence relation. The pair consisting of the two sides of E must occur in this closure. If we write the pairs (u,v) as equations u=v, the closure process becomes a deductive process, using very simple, intuitionistically correct rules of deduction for equations, and it leads from instances of A to E.

Answer 2

Here's another approach, using some topos theory and working in greater generality. The key is the Barr cover, which provides, for any topos $\mathcal E$, a topos $\mathcal B$ satisfying the internal axiom of choice (hence also the law of the excluded middle), and a surjective geometric morphism $f:\mathcal B\to\mathcal E$. Now suppose we have a geometric theory $T$ implying, in the presence of the internal axiom of choice, some geometric sequent $S$. Then I claim that $T$ implies $S$ in $\mathcal E$. Indeed, suppose $S$ is $\forall\vec x(\phi(\vec x)\implies\psi(\vec x))$, consider any model $M$ of $T$ in $\mathcal E$, and consider the truth values $u$ and $v$ in this model of $\phi$ and $\phi\land\psi$. What I must show is that the inclusion $i$ from $v$ to $u$ is an isomorphism. But $f^*$ preserves everything in sight; in particular $f^*(M)$ is a model of $T$ in $\mathcal B$, and $f^*(u)$ and $f^*(v)$ are the truth values in this model $f^*(M)$ of $\phi$ and $\phi\land\psi$, respectively. But $S$ follows from $T$ in $\mathcal B$, because internal choice holds there. So $f^*(i)$ is an isomorphism. As $f$ is surjective, $i$ is also an isomorphism, as required.

The moral of this story is that, when deducing geometric sequents from other geometric sequents, we lose no generality by assuming the internal axiom of choice (and, with it, the law of the excluded middle).

Answer 3

I am not sure I understand what is your question, but I think the following observation should answer it:

The classifying topos of an algebraic theory is the topos of presheaves over the opposite category of the category of its finitely presented models. A model of $T$ in $Set[L]$ is hence exactly a functor from the category of finitely presentable models of $L$ to the category of models of $T$. So if you have any such functor, then you have a geometric morphism from $Set[L]$ to $Set[T]$ which will extend your functor into something that transform any model of $L$ in any Grothendieck topos to a model of $T$. In fact, it work as soon as $L$ is a theory of type presheaves (which include all algebraic and all cartesian theory) and $T$ any geometric theory.