12,140
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 12:42, 26 March 2009
, 12:42, 26 March 2009→Basic Concepts from Lambek and Scott (1986): segment
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:
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===
<pre>
<pre>
| Definition 1.1. A 'concrete category' is a collection of two kinds
| Definition 1.1. A 'concrete category' is a collection of two kinds
| of entities, called 'objects' and 'morphisms'. The former are sets
| of entities, called 'objects' and 'morphisms'. The former are sets
| We shall now progress from concrete categories
| We shall now progress from concrete categories
| to abstract ones, in three easy stages.
| to abstract ones, in three easy stages.
</pre>
Graph
===Graph===
<pre>
| Definition 1.2. A 'graph' (usually called a 'directed graph') consists
| 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 two classes: the class of 'arrows' (or 'oriented edges') and the class
| A graph is said to be 'small' if the classes of objects and
| A graph is said to be 'small' if the classes of objects and
| arrows are sets.
| arrows are sets.
</pre>
Deductive System
===Deductive System===
<pre>
| A 'deductive system' is a graph in which to each object A there
| 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
| is associated an arrow 1_A : A -> A, the 'identity' arrow, and to
|
|
| as a 'rule of inference'.
| as a 'rule of inference'.
</pre>
Category
===Category===
<pre>
| A 'category' is a deductive system in which the following equations hold,
| A 'category' is a deductive system in which the following equations hold,
| for all f : A -> B, g : B -> C, and h : C -> D.
| for all f : A -> B, g : B -> C, and h : C -> D.
|
|
| (hg)f = h(gf).
| (hg)f = h(gf).
</pre>
Functor
===Functor===
<pre>
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
| Definition 1.3. A 'functor' F : $A$ -> $B$ is
| first of all a morphism of graphs (see Example C4),
| first of all a morphism of graphs (see Example C4),
|
|
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
| for all objects A of $A$ and all arrows f : A -> A' in $A$.
</pre>
Natural Transformation
===Natural Transformation===
<pre>
| Definition 2.1. Given functors F, G : $A$ -> $B$,
| Definition 2.1. Given functors F, G : $A$ -> $B$,
| a 'natural transformation' t : F -> G is a family
| a 'natural transformation' t : F -> G is a family
|
|
| G(f)t(A) = t(B)F(f).
| G(f)t(A) = t(B)F(f).
</pre>
Graph
===Graph (Review)===
<pre>
| We recall (Part 0, Definition 1.2) that, for categories,
| We recall (Part 0, Definition 1.2) that, for categories,
| a 'graph' consists of two classes and two mappings
| a 'graph' consists of two classes and two mappings
| look at graphs with additional structure which are
| look at graphs with additional structure which are
| of interest in logic.
| of interest in logic.
</pre>
Deductive System
===Deductive System===
<pre>
| A 'deductive system' is a graph with a specified arrow
| A 'deductive system' is a graph with a specified arrow
|
|
| gf
| gf
| A ----> C
| A ----> C
</pre>
Conjunction Calculus
===Conjunction Calculus===
<pre>
| A 'conjunction calculus' is a deductive system dealing with truth and
| A 'conjunction calculus' is a deductive system dealing with truth and
| conjunction. Thus we assume that there is given a formula 'T' (= true)
| conjunction. Thus we assume that there is given a formula 'T' (= true)
| <f, g>
| <f, g>
| C --------> A & B
| C --------> A & B
</pre>
Positive Intuitionistic Propositional Calculus
===Positive Intuitionistic Propositional Calculus===
<pre>
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
| with an additional binary operation '<=' (= if). Thus, if A and B are formulas,
| with an additional binary operation '<=' (= if). Thus, if A and B are formulas,
| C ----> A <= B
| C ----> A <= B
|
|
</pre>
Intuitionistic Propositional Calculus
===Intuitionistic Propositional Calculus===
<pre>
| An 'intuitionistic propositional calculus' is more than a
| An 'intuitionistic propositional calculus' is more than a
| positive one; it requires also falsehood and disjunction,
| positive one; it requires also falsehood and disjunction,
| !z!^C_A,B
| !z!^C_A,B
| R6c. (C <= A) & (C <= B) -----------> C <= (A v B).
| R6c. (C <= A) & (C <= B) -----------> C <= (A v B).
</pre>
Classical Propositional Calculus
===Classical Propositional Calculus===
<pre>
| If we want 'classical' propositional logic, we must also require:
| If we want 'classical' propositional logic, we must also require:
|
|
| R7. F <= (F <= A) -> A.
| R7. F <= (F <= A) -> A.
</pre>
Category
===Category===
<pre>
| A 'category' is a deductive system in which
| A 'category' is a deductive system in which
| the following equations hold between proofs:
| the following equations hold between proofs:
|
|
| for all f : A -> B, g : B -> C, h : C -> D.
| for all f : A -> B, g : B -> C, h : C -> D.
</pre>
Cartesian Category
===Cartesian Category===
<pre>
| A 'cartesian category' is both a category
| A 'cartesian category' is both a category
| and a conjunction calculus satisfying the
| and a conjunction calculus satisfying the
|
|
| for all f : C -> A, g : C -> B, h : C -> A & B.
| for all f : C -> A, g : C -> B, h : C -> A & B.
</pre>
Cartesian Closed Category
===Cartesian Closed Category===
<pre>
| A 'cartesian closed category' is a cartesian category $A$ with
| A 'cartesian closed category' is a cartesian category $A$ with
| additional structure R4 satisfying the additional equations:
| additional structure R4 satisfying the additional equations: