#### I could choose to “contextualize” my math experiments by adding a bunch of data to each end of each string....

I could choose to “contextualize” my math experiments by adding a bunch of data to each end of each string....

#### Theorems in math A turns into B: physics A evolves to B

Theorems in math A turns into B: physics A evolves to B

#### Each “theorem path” is like a transition amplitude for QM

Each “theorem path” is like a transition amplitude for QM

mw=UndirectedGraph[ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},"A",8,"StatesGraph"]]

Out[]=

ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},"A",8,"BranchialGraph"]

In[]:=

Out[]=

#### What is the analog in math of coarse graining in physics?

What is the analog in math of coarse graining in physics?

Nearby theorems: corollaries....

Some theorems are shortly provable from others; start with a bundle of “nearby terms”

Powerful theorem: big backbone in the graph

Powerful theorem: big backbone in the graph

#### In actually doing math, you don’t go on a long path; you use theorems you already have, and go on a fairly short path.

In actually doing math, you don’t go on a long path; you use theorems you already have, and go on a fairly short path.

#### The refactoring of axioms : what is the relation to abstraction?

The refactoring of axioms : what is the relation to abstraction?

#### Speciation in math: event horizons in the MW graph might correspond to the breaking off of different fields of math...

Speciation in math: event horizons in the MW graph might correspond to the breaking off of different fields of math...

Note: vertex list is different in this case:

mwr=SimpleGraph[UndirectedGraph[ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&[{"A""AB","BB""A"}],"A",8,"StatesGraph"]]]

In[]:=

Out[]=

If we are tracing all possible paths, which lemma is most worth introducing to shorten the average path?

Histogram[GraphDistance[mw,#[[1]],#[[2]]]&/@Tuples[VertexList[mw],2]]

In[]:=

Out[]=

Histogram[GraphDistance[mwr,#[[1]],#[[2]]]&/@Tuples[VertexList[mwr],2]]

In[]:=

Out[]=

Mean[GraphDistance[mwr,#[[1]],#[[2]]]&/@Tuples[VertexList[mwr],2]]//N

In[]:=

3.86028

Out[]=

Want to find most common subsequence in here:

FindShortestPath[mw,#[[1]],#[[2]]]&/@Tuples[VertexList[mw],2]

In[]:=

Function[newax,With[{mw=SimpleGraph[UndirectedGraph[ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&[Join[{"A""AB","BB""A"},newax]],"A",8,"StatesGraph"]]]},Mean[Flatten[GraphDistanceMatrix[mw]]]//N]][{}]

In[]:=

3.86028

Out[]=

[[[ could prune possible lemmas by a factor of 2 ]]]

[[ Also get too far out in metamathematical space .... ]]

ResourceFunction["ParallelMapMonitored"][Function[newax,With[{mw=SimpleGraph[UndirectedGraph[ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&[Append[{"A""AB","BB""A"},Rule@@newax]],"A",8,"StatesGraph"]]]},Mean[Flatten[GraphDistanceMatrix[mw]]]//N]],Tuples[VertexList[mwr],2]]

In[]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

During evaluation of In[2]:=

### Introducing a lemma is like changing your foliation

Introducing a lemma is like changing your foliation

# Axiom Systems

Axiom Systems

### 3.6 Euclidean Plane Geometry

3.6 Euclidean Plane Geometry

The axioms of Euclidean plane geometry are the axioms of predicate logic together with the thirteen axioms below. This formulation of the axioms is taken from Tarski's paper "What is elementary geometry?". As is mentioned in his paper, these axioms are complete (syntactically) and consistent. Tarski claims in his book A Decision Method for Elementary Algebra and Geometry that these axioms describe essentially the same geometry as Hilbert (who first formalized Euclid's axioms).

The sets and for Euclidean plane geometry are defined as follows.