Syntax of category theory
Syntax of category theory
Generalization of the syntax
Morphism; functors [ multimorphisms ; operads (n inputs; 1 output) ]
Without transitive closure: have path dependence
Relationship to type theory
Relationship to type theory
Arrows in type theory are functions
type constructors are rules in WM
Propositions as Types
Types as mw systems
Spatialization of limiting versions [?]
Spatialization of limiting versions [?]
Hierarchy
breaking down universal computational into a geometrical hierarchy
Rulial multiway system
Rulial multiway system
{a->b->c,a->d->c}
In[]:=
Graph[{a->b,b->c,a->d,d->c},VertexLabelsAutomatic]
Out[]=
In[]:=
Graph[{a->b,b->c,a->d,d->c,b->d,d->b},VertexLabelsAutomatic]
Out[]=
Necessarily, we’ve defined a face here...
Given a triangle in any graph, it could be a face. [[But ... many cycles in a graph aren’t naturally faces.]]
1 morphism : joins 2 objects [ maps from 0-morphisms to 0-morphisms ]
2 morphism : maps from 1-morphisms to 1-morphisms
2 morphism : maps from 1-morphisms to 1-morphisms
operad : n-ary function mapping from n 0-morphisms to 1 0-morphisms [?]
Space of all symbolic transformation rules
Space of all symbolic transformation rules
Can be decomposed into transformation for things without , and things with
Correspondence with type theory
Correspondence with type theory
A multiway system is like a type; the rules are the type constructor ; the terms of the type are states of the multiway systems ;; paths are proofs of equality
inhabitation of a type: multiway system has at least one state
multiway systems that are not inhabited:
In[]:=
ResourceFunction["MultiwaySystem"][{"x"->"x"},{},4]
Out[]=
{{},{},{},{},{}}
In[]:=
WolframModel[{{1}->{}},{}]["AllExpressions"]
Set theory
Set theory
Only possible base is {}
ur-element : has base elements other than { }
Analog of consciousness constraint for math:
Analog of consciousness constraint for math:
Think only in terms of n-categories for small n....
Light cones: provability cone
Within the coordinate system defined by the slice
Within the coordinate system defined by the slice
“Faster than proof travel”: have to go outside of a given mathematical framework
e.g. Goodstein needs ZFC
e.g. Goodstein needs ZFC
Foundations of mathematics
Foundations of mathematics
Axioms are transformations for symbolic expressions
two interpretations of mw graphs:
i) expression to expression (expressions are propositions)
ii) nodes are propositions
the act of doing mathematics is the act of coarse-graining...
a mathematician is a coarse-grainner
models are labels the mathematical observer is using
axiomatic carving of rulial space is the multiway graphs
A model of a mathematical observer...
category theory is like axiomatic systems, GR is like our models of physics
The foliation of an algebraic system & Cayley graphs
two interpretations of mw graphs:
i) expression to expression (expressions are propositions)
ii) nodes are propositions
the act of doing mathematics is the act of coarse-graining...
a mathematician is a coarse-grainner
models are labels the mathematical observer is using
axiomatic carving of rulial space is the multiway graphs
A model of a mathematical observer...
category theory is like axiomatic systems, GR is like our models of physics
The foliation of an algebraic system & Cayley graphs