Curry-Howard Isomorphism: Programs are proofs, and proofs are programs.

Axioms -> Proof (Rules of Inference) -> Theorem

Input -> Computation (Algorithmic Rules) -> Output

Physics:

Initial State -> Motion (Laws of Motion) -> Final State

Axioms -> Proof (Rules of Inference) -> Theorem

Input -> Computation (Algorithmic Rules) -> Output

Physics:

Initial State -> Motion (Laws of Motion) -> Final State

Use a modification of the “Propositions as Types” interpretation (corollary of the Curry-Howard isomorphism), as used in homotopy type theory.

Homotopy type theory: Unification of Per Martin-Lof intutitionistic/dependent type theory, with the Voevodsky’s univalence axiom.

Under this correspondence, types correspond to topological (homotopy) spaces, terms correspond to points in those spaces, proofs of equivalence between terms correspond to paths connecting the associated point, proofs of equivalence between proofs correspond to (higher) homotopies between the associated paths, etc.

Homotopy: If f:X->Y and g:X->Y (for topological spaces X and Y), a homotopy is a smooth function h:f->g.

f[x_]:=Sin[x]

In[]:=

Plot[f[x],{x,0,Pi}]

In[]:=

Out[]=

g[x_]:=Sin[x]*Cos[x]

In[]:=

Plot[g[x],{x,0,Pi}]

In[]:=

Out[]=

h[x_,t_]:=(1-t)*f[x]+t*g[x]

In[]:=

Manipulate[Plot[h[x,t],{x,0,Pi}],{t,0,1}]

In[]:=

Out[]=

Plot3D[h[x,t],{x,0,Pi},{t,0,1}]

In[]:=

Out[]=

Show[Table[Plot[h[x,t],{x,0,Pi},PlotRangeAll],{t,0,1,0.1}]]

In[]:=

Out[]=

Big picture question: Why do so many mathematical structures come equipped with a notion of space?

ZFC is a “syntactical”/”algebraic” foundation for mathematics, does not explain why there is geometry...

With[{w=ResourceFunction["WolframModel"][{{x,y,y},{x,z,u}}{{u,v,v},{v,z,y},{x,y,v}},{{0,0,0},{0,0,0}},500]},{ResourceFunction["WolframModelPlot"][w["FinalState"]],w["CausalGraph"]}]

With[{w=ResourceFunction["WolframModel"][{{x,y,x},{x,z,u}}{{u,v,u},{v,u,z},{x,y,v}},{{0,0,0},{0,0,0}},1500]},{ResourceFunction["WolframModelPlot"][w["FinalState"]],w["CausalGraph"]}]

Table[Framed[Graph[ResourceFunction["MultiwaySystem"][{"A""BB","BB""AA"},"A",t,If[t<7,"BranchialGraph","BranchialGraphStructure"],ImageSize120]],FrameStyleLightGray],{t,3,9}]

axioms=AxiomaticTheory["GroupAxioms"]

In[]:=

a.⊗(b.⊗c.)(a.⊗b.)⊗c.,a.⊗a.,a.⊗

∀

{a.,b.,c.}

∀

a.

1

∀

a.

a.

1

Out[]=

theorem=AxiomaticTheory["GroupAxioms","NotableTheorems"]["ImpliesMcCuneAxioms"]

In[]:=

a.⊗d.

∀

{a.,b.,c.,d.}

b.⊗(c.⊗)⊗⊗a.

c.

d.⊗b.

Out[]=

FindEquationalProof[ac,{ab,bc}]

In[]:=

ProofObject

Out[]=

%["ProofGraph"]

In[]:=

Out[]=

proof=FindEquationalProof[theorem,axioms]

In[]:=

ProofObject

Out[]=

proof["ProofGraph"]

In[]:=

Out[]=

Presheaf functor: Is it a mapping from a gauge choice onto a foliation? (Something to discuss...)

(if true) => Open sets are sections of the multiway system. (SW: Subsets that respect partial order).

(if true) => Open sets are sections of the multiway system. (SW: Subsets that respect partial order).

Completions (i.e. quantum mechanics) are applications of the univalence axiom.

Ability to perform quantum measurement is a statement of multiway topology (not too much “branchiness”).

Mystery: Define something set-theoretically, often a space “appears”. Why?

Define a causal network, often a spacetime “appears”.

Define a causal network, often a spacetime “appears”.

ZFC: Axiom of Extensionality - like “completions” in set theory.

It’s a StateEquivalenceFunction for set theory.

It’s a StateEquivalenceFunction for set theory.

Ultimate nature of mathematics/physics: Things that can be considered equivalent can also be considered identical.

“Cayley Graph” of a multiway system is an “infinitely completed” states graph (JG conjecture: this is a groupoid.)

Axiom of Extensions/Univalence/etc. are byproducts of us as observers choosing to model mathematics in the same way we model physics.

Ability to do mathematics arises in the same way as ability to understand physics (the existence of computational reducibility/rulial black holes/etc.)

Ability to do mathematics arises in the same way as ability to understand physics (the existence of computational reducibility/rulial black holes/etc.)

Xerxes: “Conventional” uncertainty principle is a limit on what can be measured in physics.

This formalism is constructivist by nature (because of univalence, so no axiom of choice, no law of excluded middle, etc.), so there are limits on what can be constructed in mathematics. Is this the uncertainty principle?

This formalism is constructivist by nature (because of univalence, so no axiom of choice, no law of excluded middle, etc.), so there are limits on what can be constructed in mathematics. Is this the uncertainty principle?

Grothendieck’s Hypothesis: All infinity-groupoids are topological (homotopy) spaces.

Groupoids: A category in which all morphisms are isomorphisms.

Topos: A category that “behaves like” the category of sets (i.e. “Set”).

More precisely, a category that possesses a “localization” notion.

(Analogy to commutative algebra: ring localization introduces denominators.)

More precisely, a category that possesses a “localization” notion.

(Analogy to commutative algebra: ring localization introduces denominators.)

First incompleteness theorem: If PA/ZFC is consistent, there exist propositions that are independent of PA/ZFC, i.e. propositions where neither it nor its negation are syntactically provable (in finite time).

(Proof-theoretic statement)

CH is independent of ZFC => There exist models of ZFC such that ZFC+CH is consistent <=> ZFC is consistent (Godel), and models such that ZFC+CH is inconsistent (Cohen, forcing).

(Model-theoretic implication)

(Proof-theoretic statement)

CH is independent of ZFC => There exist models of ZFC such that ZFC+CH is consistent <=> ZFC is consistent (Godel), and models such that ZFC+CH is inconsistent (Cohen, forcing).

(Model-theoretic implication)

First incompleteness theorem (WPP): Gauge-dependence in mathematics.

Proof theory: Defines a partial order on mathematics.

Model theory: Gauge choice that allows one to construct a total order.

Model theory: Gauge choice that allows one to construct a total order.

Ordinary relativity: There is a causal partial order (conformal structure of spacetime).

Timelike ordering is gauge-invariant, spacelike is gauge-dependent.

There exist propositions (defined by proof theory) whose truth is gauge-invariant (syntactically provable), and those (defined by model theory) whose truth is gauge-dependent.

Timelike ordering is gauge-invariant, spacelike is gauge-dependent.

There exist propositions (defined by proof theory) whose truth is gauge-invariant (syntactically provable), and those (defined by model theory) whose truth is gauge-dependent.

Non-constructive proofs are like boundaries of light cones (proofs that travel “at the speed of proof”), so cannot be witnessed by any “subliminal” model.

Black holes are like “inevitable non-constructivism” in mathematics.

=> (Axiom of Choice is a black hole?)

Black holes are like “inevitable non-constructivism” in mathematics.

=> (Axiom of Choice is a black hole?)

SR: Model-independence of proof theory (syntactically provable statements).

=> A model-theoretic speedup theorem (analog of Lorentz transformation).

=> A model-theoretic speedup theorem (analog of Lorentz transformation).

Inertial frames: “Free” models? (Look this up...)

Superposition in QM: There exists proof redundancy.

Godel’s speed-up theorem: “This statement is unprovable using fewer than n symbols.” (takes n symbols to prove in PA, but is trivial to prove in PA+Con(PA).)

For any pair of propositions, determining whether there exists a path between them may take an arbitrarily large amount of computational effort.

(Defining truth/falsehood in terms of consistency/inconsistency with the total/partial order.)

(Syntactical truth is consistency with partial order, semantic truth is consistency with model-induced total order.)

(Defining truth/falsehood in terms of consistency/inconsistency with the total/partial order.)

(Syntactical truth is consistency with partial order, semantic truth is consistency with model-induced total order.)

General relativity: what is the name for timelike geodesics that are so long that the endpoints appear to be spacelike-separated?

* timelike singularity!! *

* timelike singularity!! *

Connection to Malament-Hogarth spacetimes?

Mathematics is partially ordered, because mathematicians are computationally bounded?

Propositional extensionality (logic): If propositions are path-connected then they are defined to be “equivalent”.

Voevodsky’s Univalence Axiom: (If propositions are equivalent, then they are defined to be “identical”.) <- This implication is itself an equivalence.

Voevodsky’s Univalence Axiom: (If propositions are equivalent, then they are defined to be “identical”.) <- This implication is itself an equivalence.

(Xerxes): Take a multiway system, include a subobject classifier (the categorical analog of a subset identifier) as one of the type constructors, then you get an elementary topos (assuming that finite limits exist).

Interpretation of the Schwarzschild radius: There is a limit to the height of the “abstraction tower” that you can build in mathematics whilst still being a bona fide constructivist.

Increased “abstraction” (energy-momentum in “proof space”), there is gravitational lensing, creating more inequivalent proofs of the same propositions.

i.e. abstraction => (proof-theoretic) redundancy.

i.e. abstraction => (proof-theoretic) redundancy.

(Conjecture): Subobject classifiers allow you to define foliations.

(Xerxes): Such an elementary topos comes naturally equipped with a functor from the topos to the topos of sets, as well as a pair adjoint functors admitting the discrete and indiscrete topologies.

Free (and local) topoi with this collection of functors formalize the notion of a topological space.

=> Locality comes from the subobject classifier, and hence from the “locality” of foliations.

Free (and local) topoi with this collection of functors formalize the notion of a topological space.

=> Locality comes from the subobject classifier, and hence from the “locality” of foliations.

Fibration: Formalization of the idea that you can parameterize one topological space (fibre) with another one (base).

Connection: A rule allowing you to “lift” a step in the base space to a step in the fibre.

Fibration relaxes ordinary fibre bundle, since fibres don’t have to be in the same topological space (or indeed homeomorphic); you just need homotopy-equivalence (i.e. the “homotopy lifting property”).

Connection: A rule allowing you to “lift” a step in the base space to a step in the fibre.

Fibration relaxes ordinary fibre bundle, since fibres don’t have to be in the same topological space (or indeed homeomorphic); you just need homotopy-equivalence (i.e. the “homotopy lifting property”).

Categorical Quantum Mechanics (Abramsky and Coecke): Symmetric monoidal category.

Monoidal category: Category equipped with a tensor product on objects.

Symmetric monoidal category: Monoidal category where the product is “as commutative possible”.

Monoidal category: Category equipped with a tensor product on objects.

Symmetric monoidal category: Monoidal category where the product is “as commutative possible”.

(Xerxes): So long as we have a tensor product constructor, we recover categorical QM upon foliating the rulial multiway system.