### Code

Code

### Results

Results

For Boolean algebra, there are immediately truth values defined:

MultiwayOperatorSystem[{And[a_,b_]And[b,a],Or[a_,b_]Or[b,a],And[a_,Or[b_,Not[b_]]]a,Or[a_,And[b_,Not[b_]]]a,a_Module[{b=Unique[]},And[a,Or[b,Not[b]]]],a_Module[{b=Unique[]},Or[a,And[b,Not[b]]]],And[a_,Or[b_,c_]]Or[And[a,b],And[a,c]],Or[And[a_,b_],And[a_,c_]]And[a,Or[b,c]],Or[a_,And[b_,c_]]And[Or[a,b],Or[a,c]],And[Or[a_,b_],Or[a_,c_]]Or[a,And[b,c]]},{And[a,b]},1,"StatesGraph"]

In[]:=

Out[]=

MultiwayOperatorSystem[{And[a_,b_]And[b,a],Or[a_,b_]Or[b,a],And[a_,Or[b_,Not[b_]]]a,Or[a_,And[b_,Not[b_]]]a,a_Module[{b=Unique[]},And[a,Or[b,Not[b]]]],a_Module[{b=Unique[]},Or[a,And[b,Not[b]]]],And[a_,Or[b_,c_]]Or[And[a,b],And[a,c]],Or[And[a_,b_],And[a_,c_]]And[a,Or[b,c]],Or[a_,And[b_,c_]]And[Or[a,b],Or[a,c]],And[Or[a_,b_],Or[a_,c_]]Or[a,And[b,c]]},{And[a,b]},3,"StatesGraphStructure"]

In[]:=

Out[]=

#### Operator-implemented pattern strings

Operator-implemented pattern strings

"A#B""#AB#"

MultiwayOperatorSystem[{CircleDot[a_,CircleDot[b_,c_]]CircleDot[CircleDot[a,b],c],CircleDot[CircleDot[a_,b_],c_]CircleDot[a,CircleDot[b,c]],CircleDot[a,CircleDot[x_,b]]CircleDot[x,CircleDot[a,CircleDot[b,x]]]},{CircleDot[a,CircleDot[CircleDot[x,y],b]]},3,"StatesGraph"]

In[]:=

Out[]=

MultiwayOperatorSystem[{Equal[a_,b_]Equal[b,a],CircleDot[a_,CircleDot[b_,c_]]CircleDot[CircleDot[a,b],c],CircleDot[CircleDot[a_,b_],c_]CircleDot[a,CircleDot[b,c]],aCircleDot[a,b]},{CircleDot[a,a]CircleDot[a,CircleDot[CircleDot[a,b],b]]},1,"StatesGraph"]

In[]:=

Out[]=

mwo=MultiwayOperatorSystem[{Equal[a_,b_]Equal[b,a],CircleDot[a_,CircleDot[b_,c_]]CircleDot[CircleDot[a,b],c],CircleDot[CircleDot[a_,b_],c_]CircleDot[a,CircleDot[b,c]],aCircleDot[a,b]},{CircleDot[a,a]CircleDot[a,CircleDot[CircleDot[a,b],b]]},2,"StatesGraph"]

In[]:=

Out[]=

(Internally, everything is a string, so there is no evaluation)

## Interpretation

Interpretation

#### Axioms

Lemmas

Theorems

Rule of inference

Axioms

Lemmas

Theorems

Rule of inference

Lemmas

Theorems

Rule of inference

### In traditional math, distinguish axioms from rules of inference

In traditional math, distinguish axioms from rules of inference

Fundamental rule is: ab, a gives b

### Case 1 (NKS): axioms are the same as rules of inference

Case 1 (NKS): axioms are the same as rules of inference

I.e. axioms are S S multiway rules

Math starts from “True”, and deduces other true statements

Each state is then a proposition of mathematics

Theorem: a state that is derived from True

Lemma: also derived from True, but is S1 S2

Combination rules for applying axioms/lemmas inside other states [things have subparts that are like themselves] [substitute wherever you feel like]

(“Substitution” in first-order logic)

https://en.wikipedia.org/wiki/First-order_logic#Rules_of_inference

#### Case 1a: generative mathematics [start from True; prove everything]

Case 1a: generative mathematics [start from True; prove everything]

#### Case 1b: proofial mathematics: start from a proposition, and reduce it to True [ this isn’t obviously possible, unless the arrows go both ways ]

Case 1b: proofial mathematics: start from a proposition, and reduce it to True [ this isn’t obviously possible, unless the arrows go both ways ]

Or rather, get to something we already know is true (e.g. to prove BA axioms, go from the statement of axioms to a known axiom system statement)

A typical practical theorem is hypothesis assertion (i.e. conclusion) ; something considered free-floating (e.g. an axiom) is True conclusion

Process of going down the multiway system is “entailment” ( https://en.wikipedia.org/wiki/Logical_consequence )

[[[ To get False results, negate after the fact ;;; probably cannot “prove from False” ]]]

### Case 2 (traditional) : rules of inference are separate from axioms

Case 2 (traditional) : rules of inference are separate from axioms

Axioms are initial conditions

Law of inference: basically the time evolution operator

Sequent operator:

## FindEquationalProof

FindEquationalProof

#### Case 1: equational

Case 1: equational

#### Case 2: unidirectional

Case 2: unidirectional

(Mostly need axioms for And and Not etc.)

Claim is that each expression contains e.g. both a and ab

## Group theory multiway system

Group theory multiway system

#### “Algebraic theory” ~~ equality is the top-level predicate

“Algebraic theory” ~~ equality is the top-level predicate

Fields are the cross-over from algebra to analysis

#### Algebraic theories: always 2-way multiway systems

Algebraic theories: always 2-way multiway systems

## The “Model Tradeoff”

The “Model Tradeoff”

#### Crush every slice of the foliation to a single representative of an equivalence class; then whether something follows is a “straight shot”

Crush every slice of the foliation to a single representative of an equivalence class; then whether something follows is a “straight shot”

That you can change the foliation and get the same answer is causal invariance

Is A ⊢ B and A ⊢ C

Extensionality : means (bidirectional entailment) is equivalent to equivalence

Extensionality : means (bidirectional entailment) is equivalent to equivalence

x = y implies x ⊢ y and y ⊢ x

Univalence: homotopy equivalence is equivalent to equivalence : is directly causal invariance

A ⊢ B and A ⊢ C

Univalence IMPLIES causal invariance .... but not the other way around

Univalence is the justification for completions.

Univalence is normally used in the context of type systems.

If there is a common ancestor, then the states can be considered as equivalent

If two statements can be both be derived from a common hypothesis, then they are equivalent

[ “coarse-grainability” ] [ contractability ]

[ meta-metamathematical principle ]

[ “proof path invariance” ]

[ “ancestry is what counts” ]

[ decendency ]

[ sibling equivalence ] [ ancestral equivalence ] [ sibling indistinguishability ]

derivability implies equivalence

“If things can be derived from a common thing, then those things can be considered equivalent”

derivation identity

equivalability ;;; branchial contractibility ;;; branch contractability ;; branch condensation ;; branch conflation

branch equivalence

< Univalence: there is only one kind of equivalence >

[ meta-metamathematical principle ]

[ “proof path invariance” ]

[ “ancestry is what counts” ]

[ decendency ]

[ sibling equivalence ] [ ancestral equivalence ] [ sibling indistinguishability ]

derivability implies equivalence

“If things can be derived from a common thing, then those things can be considered equivalent”

derivation identity

equivalability ;;; branchial contractibility ;;; branch contractability ;; branch condensation ;; branch conflation

branch equivalence

< Univalence: there is only one kind of equivalence >

#### Branch equivalence

Branch equivalence

Physical space: contractability of light cones in coarse-graining

Branchial space: completability of branch pairs for measurement

Rulial space: equivalence through PCE

Metamathematical space (AKA proof space): fundamental assumption made in math

(if a single hypothesis implies two different statements, the truth values of the statements must be equivalent)

[ we don’t need such a long list of theorems, because many are equivalent ]

(Zorn’s lemma = axiom of choice = well-ordering = ..... [ many theorems are equivalent ] )

Branchial space: completability of branch pairs for measurement

Rulial space: equivalence through PCE

Metamathematical space (AKA proof space): fundamental assumption made in math

(if a single hypothesis implies two different statements, the truth values of the statements must be equivalent)

[ we don’t need such a long list of theorems, because many are equivalent ]

(Zorn’s lemma = axiom of choice = well-ordering = ..... [ many theorems are equivalent ] )

When you do coarse-graining, you’re not changing the topology .... and therefore you can still make certain coarse-grained statements (without getting into the microweeds)

You can make progress in math by keeping a limited number of theorems; or: it isn’t going to give you much more speedup to have 5 parallel freeways

You can make progress in math by keeping a limited number of theorems; or: it isn’t going to give you much more speedup to have 5 parallel freeways

“branch equivalence” is a meta-axiomatic principle: a principle about generating MW rules [AKA entailment rules]

“branch equivalence” is a meta-axiomatic principle: a principle about generating MW rules [AKA entailment rules]

By completing, you’ve reduced all proof paths to one path....

But which path depends on which foliation you picked.

But which path depends on which foliation you picked.

Physics: By using branch equivalence, you can “complete out” the irreducible details

CS: Branch equivalence is basically the statement that NDTMs (and QTMs) do the same as DTMs

You can coarse grain out the non-determinism

You can coarse grain out the non-determinism

Math: “One proof is enough” Ordinary substitution lemmas allow timelike jump-ahead;

critical pair lemmas [which rely on branch equivalence] all branchlike choices are condensed

critical pair lemmas [which rely on branch equivalence] all branchlike choices are condensed

#### Analogies

Analogies

Energy is associated with lemmas that we will reuse

(expressing things in terms of lemmas [AKA higher-order definitions] is like abstraction)

(expressing things in terms of lemmas [AKA higher-order definitions] is like abstraction)

< We can measure “abstraction towers” from towers of definitions in theorem banks >

Lemmas are a choice. I.e. you can arrange energy in metamathematical space

If you have a LOT of lemmas, some of them have to be critical pair lemmas, which will eventually force convergence [ like forming black holes ]

Lemmas are a choice. I.e. you can arrange energy in metamathematical space

If you have a LOT of lemmas, some of them have to be critical pair lemmas, which will eventually force convergence [ like forming black holes ]