1
$\begingroup$

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.

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, \ldots z),\; q(x, y, \ldots 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.

2) $x \oplus y < 1 \Rightarrow x \odot y = 0$ holds in any MV-chain (very easy, [CDM] 1.6.1 page 27).

3) $x \oplus 0 = x$ (axiom, [CDM] page 7), $\hspace{2ex}$ $1 \oplus x = 1$ (very easy, [CDM] page 9).

4) The equation (a): $(x \oplus y) \oplus (x \odot y) = x \oplus y$ holds in any MV-algebra.

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

case $(x \oplus y) = 1$, we have $(1 \oplus (x \odot y) = x \oplus y$

case $(x \oplus y) < 1$, we have $(x \oplus y) \oplus 0 = x \oplus y$

both cases hold by 3).

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

(intuicionistically 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), we are using an exclude middle in 4) (invalid for example in the MV-chain [0, 1], the real interval in the object of reals of the topos).

$\endgroup$
3
  • $\begingroup$ If you know that the classifying topos is of presheaf type, then yes, all theorems (in geometric logic) can be transferred from $\mathbf{Set}$ – as Simon Henry explained in the answer to your previous question. $\endgroup$
    – Zhen Lin
    Apr 27, 2014 at 21:56
  • $\begingroup$ arguing in geometric logic includes the excluded middle ?. Does the equation (a) whose proof uses "x = 1 or x < 1" hold in the real unit interval [0, 1] $\endgroup$ Apr 27, 2014 at 22:30
  • 1
    $\begingroup$ I didn't say that the proof can be transferred. A corollary of the completeness theorem says that uses of excluded middle and even the axiom of choice can be eliminated, but it doesn't really tell you how. $\endgroup$
    – Zhen Lin
    Apr 27, 2014 at 23:00

0

Your Answer

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

Browse other questions tagged or ask your own question.