Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.

Dismiss

17 views

Skip to first unread message

Aug 23, 2016, 12:21:42 PM8/23/16

to

All the approaches I've examined appear to want to codify BOUNDED

quantifiers rather than the quantifiers you see in first-order logic.

The problem with doing that is that since you're already making the

inference A |- B into a category-theoretic arrow A -> B; then the

minute you bound quantifiers you've just fed the object and morphisms

back into the term language! This, of course, leads eventually to a

formalism for "dependent types" and/or "number" or "set" objects and

suddenly you find yourself in the land of toposes and the like;

essentially trying to remake ALL the foundations of set theory and

arithemetic over into categorical form.

In addition, the approach is skewed one way only: only looking at

elements a: A of a type A which is linked to the notion of arrows of

the form p: 1 -> A; while ignoring the dual concept.

Curry's treatment of predicate logic seems to be the only comprehensive

formal approach that avoids the higher-order issue by keeping the

terms, propositions and judgements separate. But I'm not clear what

should count as a term then.

More generally, I want an approach that treats both directions of the

arrow equally.

If you have an assertional logic (where an assertion "|- A" is treated

as an arrow "1 -> A" for a terminal object 1) then there should be a

dual present for the [counter-factual] "query" B |- treating it as an

arrow "B -> 0" to the initial object 0.

Likewise if there is an "internal language" that expresses elements "a:

A" of assertions A equivalently as arrows "p = &a: 1 -> A" with inverse

a = *p and functions represented as f(a) = *(f o &a): B for f: A -> B

and a: A -- where o denotes composition -- then there should also be a

"co-language" with co-elements "b: B?" of queries B equivalently as

arrows "q = b*: B -> 0" with inverse b = q& then there should be an

internal "co-language" with "co-functions" {b}f = (b* o f)&: A? for f:

A -> B and b: B? that pulls back queries.

Corresponding to the internal lambda abstraction (lambda x)a_x: A x C

-> B for x: 1 -> C and a_x: A -> B where A x C denotes the product;

should be an internal "co-lambda" abstraction (gamma y)a_y: A -> D + B

for y: D -> 0 and a_y: A -> B where D + B denotes the co-product.

So even if you go the usual route with dependent types and/or bounded

quantifiers there should be a dual notation that binds with co-elements

rather than with elements.

0 new messages

Search

Clear search

Close search

Google apps

Main menu