SUO: Lamina Calculus
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
In most mathematical namespaces, a "module" is a structure like a vector space,
but defined over a "ring" instead of a "field" -- there are times when I think
I can even see some sort of a connection to the kinds of "modules" that we all
know and that some of us love here, but not at the moment -- so I frequently
find myself having to think up other ways to express the design protocols
of stepwise refinement and top-down programming that go under the name
of "modularity". Very often it happens that the image of "layers"
or "lamina" are even more apt for expressing the relevant forms
of structured development, and that is how I am seeing it now.
Aside from its inherent interest and its ontological applications,
anybody who wishes to consider a genuine case of axiomatic Aufbau
might well take a look at the development of category theory that
Jim Lambek & Phil Scott present in the following "modern classic":
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
I have been posting excerpts to the ONT List, between note_01 & note_30:
note_01 = http://suo.ieee.org/ontology/msg03373.html
note_30 = http://suo.ieee.org/ontology/msg03418.html
Here is a synopsis, exhibiting just the layering of axioms --
notice the technique of starting over at the initial point
several times and building up both more richness of detail
and more generality of perspective with each passing time:
Concrete Category
| Definition 1.1. A 'concrete category' is a collection of two kinds
| of entities, called 'objects' and 'morphisms'. The former are sets
| which are endowed with some kind of structure, and the latter are
| mappings, that is, functions from one object to another, in some
| sense preserving that structure. Among the morphisms, there is
| attached to each object A the 'identity mapping' 1_A : A -> A
| such that 1_A(a) = a for all a in A. Moreover, morphisms
| f : A -> B and g : B -> C may be 'composed' to produce
| a morphism gf : A -> C such that (gf)(a) = g(f(a))
| for all a in A.
| We shall now progress from concrete categories
| to abstract ones, in three easy stages.
Graph
| Definition 1.2. A 'graph' (usually called a 'directed graph') consists
| of two classes: the class of 'arrows' (or 'oriented edges') and the class
| of 'objects' (usually called 'nodes' or 'vertices') and two mappings from
| the class of arrows to the class of objects, called 'source' and 'target'
| (often also 'domain' and 'codomain').
|
| o--------------o source o--------------o
| | | ----------------> | |
| | Arrows | | Objects |
| | | ----------------> | |
| o--------------o target o--------------o
|
| One writes "f : A -> B" for "source f = A and target f = B".
| A graph is said to be 'small' if the classes of objects and
| arrows are sets.
Deductive System
| A 'deductive system' is a graph in which to each object A there
| is associated an arrow 1_A : A -> A, the 'identity' arrow, and to
| each pair of arrows f : A -> B and g : B -> C there is associated
| an arrow gf : A -> C, the 'composition' of f with g. A logician
| may think of the objects as 'formulas' and of the arrows as
| 'deductions' or 'proofs', hence of
|
| f : A -> B g : B -> C
| ---------------------------
| gf : A -> C
|
| as a 'rule of inference'.
Category
| A 'category' is a deductive system in which the following equations hold,
| for all f : A -> B, g : B -> C, and h : C -> D.
|
| f 1_A = f = 1_B f,
|
| (hg)f = h(gf).
Functor
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
| first of all a morphism of graphs (see Example C4),
| that is, it sends objects of $A$ to objects of $B$
| and arrows of $A$ to arrows of $B$ such that, if
| f : A -> A', then F(f) : F(A) -> F(A'). Moreover,
| a functor preserves identities and composition;
| thus:
|
| F(1_A) = 1_F(A),
|
| F(gf) = F(g)F(f).
|
| In particular, the identity functor 1_$A$ : $A$ -> $A$ leaves
| objects and arrows unchanged and the composition of functors
| F : $A$ -> $B$ and G : $B$ -> $C$ is given by:
|
| (GF)(A) = G(F(A)),
|
| (GF)(f) = G(F(f)),
|
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
Natural Transformation
| Definition 2.1. Given functors F, G : $A$ -> $B$,
| a 'natural transformation' t : F -> G is a family
| of arrows t(A) : F(A) -> G(A) in $B$, one arrow for
| each object A of $A$, such that the following square
| commutes for all arrows f : A -> B in $A$:
|
| t(A)
| F(A) o------------------>o G(A)
| | |
| | |
| F(f) | | G(f)
| | |
| v v
| F(B) o------------------>o G(B)
| t(B)
|
| that is to say, such that
|
| G(f)t(A) = t(B)F(f).
Graph
| We recall (Part 0, Definition 1.2) that, for categories,
| a 'graph' consists of two classes and two mappings
| between them:
|
| o--------------o source o--------------o
| | | ----------------> | |
| | Arrows | | Objects |
| | | ----------------> | |
| o--------------o target o--------------o
|
| In graph theory the arrows are usually called "oriented edges"
| and the objects "nodes" or "vertices", but in various branches
| of mathematics other words may be used. Instead of writing
|
| source(f) = A,
|
| target(f) = B,
| f
| one often writes f : A -> B or A ---> B. We shall
| look at graphs with additional structure which are
| of interest in logic.
Deductive System
| A 'deductive system' is a graph with a specified arrow
|
| 1_A
| R1a. A -----> A,
|
| and a binary operation on arrows ('composition')
|
| f g
| A ---> B B ---> C
| R1b. ----------------------
| gf
| A ----> C
Conjunction Calculus
| A 'conjunction calculus' is a deductive system dealing with truth and
| conjunction. Thus we assume that there is given a formula 'T' (= true)
| and a binary operation '&' (= and) for forming the conjunction A & B of
| two given formulas A and B. Moreover, we specify the following additional
| arrows and rules of inference:
|
| O_A
| R2. A -----> T,
|
| p1_A,B
| R3a. A & B --------> A,
|
| p2_A,B
| R3b. A & B --------> B,
|
| f g
| C ---> A C ---> B
| R3c. ----------------------.
| <f, g>
| C --------> A & B
Positive Intuitionistic Propositional Calculus
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
| with an additional binary operation '<=' (= if). Thus, if A and B are formulas,
| so are T, A & B, and A <= B. (Yes, most people write B => A instead.) We also
| specify the following new arrow and rule of inference:
|
| !e!_A,B
| R4a. (A <= B) & B ---------> A,
|
| h
| C & B ---> A
| R4b. ----------------.
| h*
| C ----> A <= B
|
Intuitionistic Propositional Calculus
| An 'intuitionistic propositional calculus' is more than a
| positive one; it requires also falsehood and disjunction,
| that is, a formula 'F' (= false) and an operation 'v' (= or)
| on formulas, together with the following additional arrows:
|
| []_A
| R5. F ------> A,
|
| k1_A,B
| R6a. A --------> A v B,
|
| k2_A,B
| R6b. B --------> A v B,
|
| !z!^C_A,B
| R6c. (C <= A) & (C <= B) -----------> C <= (A v B).
Classical Propositional Calculus
| If we want 'classical' propositional logic, we must also require:
|
| R7. F <= (F <= A) -> A.
Category
| A 'category' is a deductive system in which
| the following equations hold between proofs:
|
| E1. f 1_A = f,
|
| 1_B f = f,
|
| (hg)f = h(gf),
|
| for all f : A -> B, g : B -> C, h : C -> D.
Cartesian Category
| A 'cartesian category' is both a category
| and a conjunction calculus satisfying the
| additional equations:
|
| E2. f = O_A, for all f : A -> T.
|
| E3a. p1_A,B <f, g> = f,
|
| E3b. p2_A,B <f, g> = g,
|
| E3c. <p1_A,B h, p2_A,B h> = h,
|
| for all f : C -> A, g : C -> B, h : C -> A & B.
Cartesian Closed Category
| A 'cartesian closed category' is a cartesian category $A$ with
| additional structure R4 satisfying the additional equations:
|
| E4a. !e!_A,B <h* p1_C,B, p2_C,B> = h,
|
| E4b. (!e!_A,B <k p1_C,B, p2_C,B>)* = k,
|
| for all h : C & B -> A, k : C -> (A <= B).
|
| Thus, a cartesian closed category is
| a positive intuitionistic propositional
| calculus satisfying the equations E1 to E4.
| This illustrates the general principle that
| one may obtain interesting categories from
| deductive systems by imposing an appropriate
| equivalence relation on proofs.
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤