Types of Entailments | Inference Rules

Which kinds of entailments yield causal invariance?

E.g. substitution lemmas, critical pair lemmas
Possible name: paralemma ; ? metalemma

An entailment is an event

https://en.wikipedia.org/wiki/List_of_rules_of_inference

Token Models

Models for tokens:
want a “math-like” model for a token

An expression

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

lhs->rhs

Limiting Processes

“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

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

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

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

A given community has enough common ancestry to be close in branchial space
Is the math genealogy database like a map of branchial space?
https://blog.wolfram.com/2018/08/02/computational-exploration-of-the-mathematics-genealogy-project-in-the-wolfram-language/

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 ]

Type theory

Equivalence of types ?

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

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

[ 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 ]

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?

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

Otherwise, there would be a discontinuity

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

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?

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

[Things to look up]

Lindenbaum–Tarski algebra

Traphs

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 ]

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

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 try critical pair rule

Substitution lemmas are basically like ReplaceAll

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

This will work for one-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/....

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”

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

This goes beyond combinators
Insists that two subtrees are the same...