Thursday, 26 July 2012

lo.logic - term equality in algebraic theories

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. x1:[x1,x2]to[x1],x2:[x1,x2]to[x1,x2],(x1,x2):[x1,x2]to[x1,x2], etc. Now what can I claim about the arrows x1:[x1,x2]to[x1] and x2:[x1,x2]to[x1]? Is it true that x1=x2? If I assume the law of excluded middle then I should be able to claim something about x1=x2 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 x1=x2 since the theory doesn't imply x1=x2 so can I infer from this that x1neqx2? I'm probably over-thinking it.

No comments:

Post a Comment