## Types of Entailments | Inference Rules

Types of Entailments | Inference Rules

#### Which kinds of entailments yield causal invariance?

Which kinds of entailments yield causal invariance?

E.g. substitution lemmas, critical pair lemmas

Possible name: paralemma ; ? metalemma

#### An entailment is an event

An entailment is an event

## Token Models

Token Models

#### Models for tokens:

want a “math-like” model for a token

Models for tokens:

want a “math-like” model for a token

want a “math-like” model for a token

An expression

#### In an expression, there are variables and there are operators

In an expression, there are variables and there are operators

Constants are like operators with arity 0

In the rulial limit, we introduce all possible operators

WPP: what should the data structure be? The ruliad doesn’t care...

#### Special types of expressions

Special types of expressions

lhs->rhs

### Limiting Processes

Limiting Processes

#### “Molecular scale” is axiomatic formalized math

“Molecular scale” is axiomatic formalized math

The only aspect that may go “lower” than usual is to do variable naming / operator persistence

In doing math, one application of an inference rule is atomic ... but we have subparts of inference rule application

#### Multiway molecular structure

Multiway molecular structure

In a TEG, an instantaneous state of “all possible math” is some time slice that picks up a certain set of propositions

#### Continuum limit

Continuum limit

[ Many hyperedges are equivalenced ]

Equivalencing different versions of the Pythagorean theorem

[ Not just different proofs, but a different statement of the theorem ]

E.g. with different axioms for the reals, you can still get a “Pythagorean” theorem

## Mathematical Observers

Mathematical Observers

#### Narrowest [“single-minded”] observer: follows a single path in the multiway system [whose rules are rules of inference]

Narrowest [“single-minded”] observer: follows a single path in the multiway system [whose rules are rules of inference]

In the multiway system, we’ve already done equivalencing relative to the TEG

Different paths are like building up math with different textbooks

With confluence/causal invariance they’ll both be able to do the same exam ... but the intermediate theorems proved were different

#### Mathematical communities are laid out in branchial space

Mathematical communities are laid out in branchial space

A given community has enough common ancestry to be close in branchial space

Is the math genealogy database like a map of branchial space?

### Given two different axiom systems, can we determine whether two differently-stated theorems are “the same”

Given two different axiom systems, can we determine whether two differently-stated theorems are “the same”

In group theory, each group is like a different axiom system ;; even each presentation of the group (e.g. choice of generators)

[ cf representation theory ]

What results are there in group theory that are “continuum limit” results, independent of which group you’re talking about ...

[ There are results in pure group theory like this ... But what about results which are “roughly” true for any big group / big representation ]

[ There are results in pure group theory like this ... But what about results which are “roughly” true for any big group / big representation ]

#### Type theory

Type theory

Equivalence of types ?

### Why is undecidability uncommon in math?

Why is undecidability uncommon in math?

?? For the same reason that gas molecules usually have a short mean free path

Computation [e.g. ruliology] is like free-streaming molecules ; whereas human-processed math is like a gas

### In physical space ... consider Euclid

In physical space ... consider Euclid

Different underlying hypergraphs all limit to satisfying (approximately) Euclid’s axioms + Euclid’s theorems

### [ Mathematicians don’t “live in the mathematics” ... unlike for physics ]

[ Mathematicians don’t “live in the mathematics” ... unlike for physics ]

Possible claim: The only math that we think of doing is math informed by our experience in the actual universe

[ E.g. claim: numbers are inevitable given basic physical consciousness ]

[ E.g. geometry is a consequence of our consciousness / character as observers ]

[ E.g. geometry is a consequence of our consciousness / character as observers ]

#### Claim: we end up with comprehensible physics for the same reason as we end up with comprehensible mathematics

Claim: we end up with comprehensible physics for the same reason as we end up with comprehensible mathematics

### Is the notion of the continuum deeply related to the character of us as observers?

Is the notion of the continuum deeply related to the character of us as observers?

The observer has continuity / persistence between moments in time

“It’s the same ‘me’ at different moments in time”

#### Persistence of the observer perception of a continuum

Persistence of the observer perception of a continuum

Otherwise, there would be a discontinuity

#### Our perception is that time is a continuum ; there are no discrete “not us” steps

Our perception is that time is a continuum ; there are no discrete “not us” steps

### The observer typically cares about phenomena that persist

The observer typically cares about phenomena that persist

A detail of some automated proof that has no persistence is not going to be “noticed”

From an automated proof, can we recognize something that’s a bigger picture?

Persistent homology??

### Is metamathematical space like swiss cheese ... with many topological obstructions?

Is metamathematical space like swiss cheese ... with many topological obstructions?

#### Does computational irreducibility that this has to be the case?

Does computational irreducibility that this has to be the case?

?? Rulial space for Turing machines

### Calculus is the “linguistic construct” that connects observers like us with physical reality

Calculus is the “linguistic construct” that connects observers like us with physical reality

## [Things to look up]

[Things to look up]

#### Lindenbaum–Tarski algebra

Lindenbaum–Tarski algebra

## Traphs

Traphs

#### We want to use a structure that looks like traditional math

We want to use a structure that looks like traditional math

so that we can compare with empirical metamathematics

[Need an empirically recognizable structure]

((a_·c_)·a_)·((((b_·c_)·a_)·(b_·((b_·a_)·b_)))·(((((b_·c_)·a_)·(b_·((b_·a_)·b_)))·a_)·(((b_·c_)·a_)·(b_·((b_·a_)·b_)))))a_

#### [ Using TwoWayMultiReplace.nb ]

[ Using TwoWayMultiReplace.nb ]

In[]:=

TwoWayMultiReplace[{f[a_]<->f[1]},"SubstitutionLemmas"->True,"CriticalPairLemmas"->False,"Deduplicate"->False]

Out[]=

{{1,1},None,{},1,0}f[a_]f[1],{{1,1},Right,{1},1,1}f[1]f[1],{{1,1},Right,{2},1,0}f[a_]f[1],{{1,1},Left,{2},1,1}f[a_]f[b_]

In[]:=

substitutionLemmas[f[a],f[x_]<->g[x_]]

Out[]=

{Right,{},1}g[a]

This canonicalizes in for the scope of this computation:

In[]:=

substitutionLemmas[f[a],f[x_]<->g[y_]]

Out[]=

{Right,{},1}g[a_]

In[]:=

substitutionLemmas[{f[a],f[z]},f[x_]<->g[y_]]

Out[]=

{Right,{1},1}{g[a_],f[z]},{Right,{2},1}{f[a],g[a_]}

In[]:=

ResourceFunction["TokenEventGraph"][{ww_}:>Values[substitutionLemmas[ww,f[x_]<->g[y_]]],{f[a]},2]

Out[]=

#### First, re-use a fixed proposition

First, re-use a fixed proposition

#### Operating with the vat on the vat

Operating with the vat on the vat

Pure semigroup theory, with pure substitution, can reach only a finite number of results....

#### Now introduce a↔a as an axiom

Now introduce a↔a as an axiom

#### Now try critical pair rule

Now try critical pair rule

#### Substitution lemmas are basically like ReplaceAll

Substitution lemmas are basically like ReplaceAll

#### What is the meta-idea of all symbolic rules of inference?

What is the meta-idea of all symbolic rules of inference?

Variables can be replaced by expressions ... Then one uses the rule to say what the transformation is.

Do this replacement everywhere; then go from LHS to RHS of the rule

This is the general notion of a pattern ... together with the general notion of a transformation

[For strings, it’s confusing ... because it looks like we’re just replacing with literals]

Choose:

Now use rule #2 to get

Now use this to replace a_

#### In substitution, you are replacing matching subtrees according to some rule

In substitution, you are replacing matching subtrees according to some rule

This will work for one-way rules

#### When there are two-way rules,

When there are two-way rules,

Instantiate the variable with:

f[b_] matches a_

Now use rule #2 in rule #1:

Now rule #2 is

this is valid, but it’s just a substitution rule

now replace a_ with f1[b_]

### Basic concept of axioms/propositions/math/rules/....

Basic concept of axioms/propositions/math/rules/....

The rules give templates for what should happen, that can be applied in many contexts...

E.g. string substitution: “wherever ABA occurs, replace it” [[ and copy the unchanged parts of the string ]]

E.g. cellular automata : “wherever 101 occurs, replace it”

E.g. combinators: “wherever this ‘top of tree occurs’ replace it copying the subtrees”

E.g. cellular automata : “wherever 101 occurs, replace it”

E.g. combinators: “wherever this ‘top of tree occurs’ replace it copying the subtrees”

#### substitution lemma: find where this a match, and copy subtrees [[ and the supertree ]]

substitution lemma: find where this a match, and copy subtrees [[ and the supertree ]]

(The supertree is your context .... just like the “residue” of the unaffected part of a string)

(this works just like combinators)

#### Key new idea: x_ and x_ are the same

Key new idea: x_ and x_ are the same

This goes beyond combinators

Insists that two subtrees are the same...