Validity_of_equations_in_topos

Validity_of_equations_in_topos

[Eduardo J. Dubuc]

I clarify my previous question with a simple example. It is also a
simpler (and more general) question whose resolution resolves the
previous question on interpreting a theory in another.

QUESTION: If an equation (in an algebraic theory) can be proved to hold
by any means (choice, excluded middle, etc) in any Set-Model, then it
holds in any model in any topos. No need to do an intuitionistic
proof ?

For example if we use the excluded middle in any totally ordered poset,
(this includes the real interval [0, 1])

Example:

The reference is the book [CDM] ``Algebraic foundations of Many-valued
Reasoning??  Kluver Academic Publishers (2000)

Consider the theory of MV-algebras. By a standard choice argument we have:

1) Every MV-algebra is a subalgebra of a product of
MV-chains with the pointwise structure.

Corollary. Given any two terms p(x, y, ... z) and   q(x, y, ... z), the
equation

p(x, y, \ldots z) = q(x, y, \ldots z)

holds in every MV-algebra if and only if it holds in every MV-chain.

(denote "@" for $\oplus$,  and "*" for $\odot$

2) x @ y < 1  ==>  x * y = 0 holds in any MV-chain.

(very easy, [CDM] 1.6.1 page 27).

3)  $x @ 0 = x$  (axiom, [CDM] page 7),
      $1 @ x = 1$  (very easy, [CDM] page 9).


4) The equation (a): (x @ y) @ (x * y) = (x @ y)
holds in any MV-algebra.

proof: By 1) it is enough to prove it for MV-chains:

case (x @ y) = 1: we have 1 @ (x * y) = 1

case (x @ y) < 1: we have  (x @ y) @ 0 = (x @ y) (by 2)

both cases hold by 3).

5) By the completeness theorem the equation (a) follows
from the axioms of the theory,

   (intuitionistically or classically ?)

thus the equation should hold in (the internal language) for any
MV-algebra object in any Grothendieck topos ?

5) Also we can argue via the presheaf classifying topos of the theory of
MV-algebras and come to the same conclusion ?

Is 5) valid ?

Notice that, besides the use of choice in 1), if we have already a
chain, we do not need 1), but we are using an exclude middle in 4) to
prove the equation (invalid for example in the MV-chain [0, 1], the real
interval in the object of reals of the topos). Never the less, the
equation holds in [0, 1] but the proof does not ?

e.d.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]