2
$\begingroup$

For algebraic theories how relevant is the underlying logic? Is it possible that two terms $s$ and $t$ can be shown to be equal with respect to one set of logical axioms but not necessarily so with another set of logical axioms? From my limited knowledge it seems that the logical axioms shouldn't matter much since playing with terms only requires substitution and reduction using the axioms of the theory.

My question is motivated by the syntactic category construction. I'm reading some notes on categorical logic and the syntactic category has a notion of morphism equality that depends on the theory but no mention is made of the underlying logic and I'm wondering why.

For example: Take the empty theory. The only terms are just variables so the objects of the syntactic category will be contexts and the morphisms will be tuples of variables, e.g. $x_1:[x_1,x_2]\to[x_1], x_2:[x_1,x_2]\to[x_1,x_2], (x_1,x_2):[x_1,x_2]\to [x_1,x_2]$, etc. Now what can I claim about the arrows $x_1:[x_1,x_2]\to[x_1]$ and $x_2:[x_1,x_2]\to[x_1]$? Is it true that $x_1 = x_2$? If I assume the law of excluded middle then I should be able to claim something about $x_1 = x_2$ but if I don't assume the law of the excluded middle then it seems that I can't make a positive or negative claim about the status of $x_1 = x_2$ since the theory doesn't imply $x_1 = x_2$ so can I infer from this that $x_1 \neq x_2$? I'm probably over-thinking it.

$\endgroup$
4
  • $\begingroup$ What do you mean by underlying logic? Does it include how the generating relations are presented? $\endgroup$ Jan 27, 2010 at 19:33
  • $\begingroup$ No, the generating relations are part of the theory and not part of the logical axioms. At least that's how I understand it. $\endgroup$
    – user577
    Jan 27, 2010 at 20:12
  • $\begingroup$ The primitive recursive operations are mostly immune to whether the logic used is classical or intuitionistic, as in topoi. However, you might run into trouble if your symbol object does not have decidable equality, which is why I was concerned about presentations. $\endgroup$ Jan 27, 2010 at 21:13
  • $\begingroup$ That clears up some of my confusion. I'll just forge ahead with the notes and see if I'm just worried about nothing. $\endgroup$
    – user577
    Jan 27, 2010 at 21:20

1 Answer 1

3
$\begingroup$

Whether a particular equation is a consequence of other given equations won't depend on the logic, as long as the logic stays within reasonable bounds. The lower bound is that the logic should include substituting terms for variables in equations and should prove that equality is an equivalence relation; let me call this minimum M for brevity. The upper bound is soundness: from premises true in some structure, the logic should infer only conclusions that are also true in that structure.

Now suppose an equation E is deducible from a set S of identities in some sound logic; I claim E is also deducible from S using just the minimum M described above. The key to this is the free algebra F, built using the function symbols in E and S (including constants as 0-ary functions) and the variables in E, subject to the identities in S. This algebra F can be explicitly described as consisting of equivalence classes of terms, under the equivalence relation of M-provable equality. (M is rigged to ensure that this is an equivalence relation and the operations are well-defined on equivalence classes.) By construction, F satisfies S, so by soundness it also satisfies E. In fact, it satisfies E when the variables are assigned arbitrary values in F; I care only about the assignment that gives each variable x the value equivalence-class-of-x. Truth of E under this assignment means precisely that E was deducible from S in the logic M.

As far as I can see, this argument survives even if we work in an intuitionistic meta-theory and we cannot assert for each pair of function symbols that they are equal or not. In fact, I tried to express the proof so as to avoid any use of non-equality.

$\endgroup$
2
  • $\begingroup$ I think your system M is sometimes named after Birkhoff, who proved their completeness in the 30's. $\endgroup$ Jul 5, 2010 at 21:58
  • $\begingroup$ Correction: M should also include a rule allowing substitution of equals for equals. That's needed to ensure that F is well-defined. $\endgroup$ Aug 21, 2010 at 20:04

Your Answer

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