This notion shares a quality with the Church-Turing hypothesis. Both of these ideas have escaped mathematical characterization of their essential content. In the case of the Church-Turing hypothesis we have lots of instances of encoding one model of computation into another (such as the λ-calculus into Turing machines, or π-calculus into λ-calculus) but we have as a community been unable to formulate a statement of the idea as a provable (or refutable) statement. Likewise, there are lots of instances of the proposition-as-types paradigm and lots of connected phenomena but not statement of the idea underlying all these mathematical observations in an unequivocally provable or refutable fashion. As such the notion is particularly attractive to me -- elusive and deep.

Now, i believe i have a proposal in hand for a statement of the essential mathematical content. What's at stake here is the relationship between collectivity -- groups, populations, entities in which multiplicity and containment are explicit acknowledged and modeled -- and property -- some declarative or intensional description of a quality or aspect of observable form. That's what's going on in all these instances. i submit that a genuine understanding of this relationship has practical implications for technology, science and society -- which i will enumerate below. i also feel that -- like most deep concepts -- the formal content is profoundly simple.

So, without further preamble, i will state it now. We start with the following data.

- A monad for a term language (data structure, record structure, program structure).
- A monad for a notion of collection (sets, lists, destructively modifiable stores, ...).

- Monad for a free monoid
- Monad for sets

- m ::= e | g1 | ... | gN | m*m
- This grammar generates "monoid expressions" in N generators
- If we impose the relation(s) (which we will call structural equivalence in the sequel) m*e = m = e*m, then we get the free monoid

- unit(x) = { x }
- mult = flatten

- [| true |] = L(m)
- [| ~φ |] = L(m) \ [| φ |]
- [| φ & ψ |] = [| φ |] ∩ [| ψ |]

- [| e |] = { m ∈ L(m) | m = e }
- [| gi |] = { m ∈ L(m) | m = gi }
- [| φ * ψ |] = { m ∈ L(m) | m = m1*m2, m1 ∈ [| φ |] m2 ∈ [| ψ |] }

- What happens when you use different term languages and different collection monads? Brilliant question, grasshopper. i can see you will go far; but, let us proceed slowly.
- Curry-Howard is not just about formulae; it is about the correspondence of formulae and types and proofs and programs. How do you extend this approach to include morphisms? Further, when the term language is for program terms, how does all this work? To this i must say: well observed, grasshopper; and in time all will be revealed. In the interim look at Caires' recent CALCO paper.
- How is this math related to practical issues in technology and science? To this i must also say: excellent question, grasshopper; patience is the mother of enlightenment.

i want to propose that the logics that arise from this operational view of the content of the Curry-Howard isomorphism are a family of natural candidates for such a language. If you were looking for a good fishing spot to catch such a fish, i'd advise you to fish there. And, now for the really radical proposal... (drum roll please)... Beyond the fact that these logics provide a means by which to describe qualities or aspects shared by members of the collective there is the possibility that the intention of the collective -- what brings them together as a collective -- might be identified with the logical, intensional description that picks out just that collective. In the formal language described above, i am suggesting that intention of the extension (the meaning, semantic denotation) of a given formula is the formula. Let me say it another way, the collective of individuals that may be described by a given formula intends that formula. What the group, the state, the electorate or the market says to (whoever's listening) is the formulae that picks out that group.

In terms of technical considerations like many formulae have the same extension, you can resolve this by composition (conjunction, disjunction, ...). This comment is designed primarily to keep focus on this very strange, but intriguing idea that what the collective says is what the formula that picks out that very collective means. To sloganize just a little, 'what brings us together is what we intend.' (And this is the other source for the choice of title for this posting, we are finding a way to 'confuse' intension with intention.) If this idea is more than just a crazy idea of a mad (computer) scientist, it means that individual and collective, voter and electorate, shareholder and corporation can sit down over a cup of coffee and have a conversation in a language as detailed and rich as the one employed to write this blog entry. That changes the game entirely -- at just the time when we have the technology -- the Internet -- to actually build that coffee shop and make the Berlitz "tapes" for that language widely available.

## 4 comments:

I don't think this makes sense. Social groups have a dynamic extension and so any intension should be dynamic too. I don't think there is a property as such. There may be family resemblances within vague groupings such as "liberal". Are you suggesting that a process can stand in place of a property and be used to represent dynamic social intention, intension, and extension?

Alexis,

Excellent comment. Actually, we get this sort of dynamism when we apply the procedure in the following ways.

1. Our term language includes behavior. As i pointed out, this is a generalization of the process by which we get spatial logic. Thus, our term language can be processes. Thus, we can get properties of processes -- including extensions in time. i have discovered that the Hennessy-Milner trick of treating actions as modalities can be generalized by the Sewell-Milner-Leifer trick of labeling transitions with contexts. This allows us to use contexts as modalities which in turn allows us to express dynamic properties and properties with dynamic extension.

2. We recognize that the process is iterable -- the logic is also a term language through which we can pull collectivity.

3. We can also model the process of agents uttering (in a language like one of these logics) across scale. boundaries.

Well 2 and 3 are all very well but 1 is where you may get traction. For any given HM property P, and any single observer (process?), there exists a set of processes observed to realize P. Now you get social groups but they are only 'objects' if everyone can agree on what property they realize ;-)

Very funny! The whole point is -- of course -- the proposal that the meaning of the extension is the formula that picks it out.

Now, the reason that 2 & 3 are important is that you need to be able to 'go meta' to talk about that meaning. The facility of 2 & 3 are exhibited to show that we can use the process as is to climb up to the meta level.

Post a Comment