• First-order Categorical Logic with quantifiers that respects duality?

    From rockbrentwood@gmail.com@21:1/5 to All on Tue Aug 23 10:21:40 2016
    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.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)