Monday, February 04, 2008

Fusion and structure

An apparently important operation in algebraic logic is that of fusion, º. This is a binary operation which satisfies the following, where ≤ is a partial order representing implication:
aºb≤c iff b≤ a→c, and
aºb≤c iff a≤ c←b. Read more
Fusion is then instrumental in connecting the operational form of implication, → and ←, with the relational form, ≤. Fusion is glossed as a premiss combining operation. There needs to be something to combine premises since ≤ is a binary relation and often we want to talk about more than one premiss entailing others. From the definition, it appears that º can only be introduced on the left of ≤. There isn't any indication of what a º would amount to or how it would relate to → and ← on the left of ≤, which can of course happen, as in a→b≤a→b. Granted, the section in the book dealing with fusion is entirely in terms of implication, so it makes a modicum of sense to leave it at that. The question just jumps out what the relation is between ∧ and º when º is on the right of ≤. Do we get identity or does it depend of further principles?

Dunn notes that in languages with just implication and fusion, adding conditions to fusion yields algebras corresponding to different implication logics (as I mentioned before). I haven't cleared up what the sense of correspondence here is, but I have some other things to say. If Dunn is right, then conditions on fusion have a tight connection (correspondence?) to structural rules in Gentzen systems and discharge functions in natural deduction systems. If fusion can't do anything apart from associate, not even commute, then we get Lambek calculus. (I've never fiddled with a Gentzen version of the Lambek calculus, so I'm on uneasy footing there.) If stipulate fusion to have the lower bound property (aºb≤a) and commutation, then we get intuitionistic implication. No indication is given in the book what we need to add to it to get classical implication. This is odd, since it is a natural progression, going from the ueber-weak Lambek implication, to relevance implication, to intuitionistic to classical. But, it goes missing.

One idea why is that ≤, being a binary relation, only allows one element on its right. If we have a Gentzen formulation of intuitionistic logic and lift the restriction on the number of propositions in the succedent, then we get classical logic, a seemingly magical fact. I'm not sure how to develop this idea. The presentation of classical implication uses binary ≤, so that doesn't seem to be the sticking point. Another idea is that fusion can't be the classical way of combining premises. Classical logic is truth-functional, so extensional. Fusion is intensional in the sense that might discriminate equivalent elements that appear in different places in the fused element. In order to get fusion to act extensionally, it would need to behave like ∧. Could we have two distinct operations, ∧ and ∧', that are both extensional and behave like 'and'? No. Making º that much like ∧ would make it ∧.

There seems to be a bit of a difference between the proof theoretic and algebraic ways of looking at things. In proof theory, more specifically in a Gentzen formulation, we need to have multiple succedents to have classical logic (or do away with the ⇒ entirely). Merely being free in premiss manipulation and combination, what the comma does (or taking the antecedent and succedent to be multisets), only gets us to intuitionistic logic. Strictly speaking in the algebraic formulation, we are only using one premiss, the fusion (or conjunction) of the elements. Perhaps a similar case could be made for the Gentzen formulation, that only a single premiss is being used, namely the multiset (or sequence) of the premises. I feel like there is still a difference in the amount of structure being attributed to the respective sides, proof theoretic and algebraic, though. The question, then, is what is being suppressed on the algebraic side?

I had hoped to come up with something more to say about the connection between conditions on fusion and structural rules, but I don't think I have anything worthwhile to say at the moment. I have a vague idea that the conditions on fusion might make the structural rules explicit. The idea behind this is that the conditions are single statements in the language. The structural rules are inference rules, rules being different than propositions. Might fusion make structure explicit? Maybe?

No comments: