6
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ I suppose you mean to ask whether proofs can be transferred, and not just results? The answer should be no, if only because proofs can contain irrelevant steps... $\endgroup$
    – Zhen Lin
    Apr 27, 2014 at 8:00

3 Answers 3

8
$\begingroup$

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.

$\endgroup$
7
$\begingroup$

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).

$\endgroup$
1
  • $\begingroup$ So, for example, if we want to prove that the validity of some equation follows from the validity of other equations in the real interval [0, 1] (equations in any geometric language interpretable in [0, 1]), then we can proceed by cases, for example, (x = 1) or (not x = 1). Even though that [0, 1] is not decidable. So this proof using classical logic which is not valid intuitionistically will in practice be accepted as a proof in the internal language of any topos, since we accept the conclusion as true without requiring any other proof. $\endgroup$ Apr 29, 2014 at 13:48
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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