Idealizations of mathematics

Equational logic

exprs + two-way rules

Theorem network

lemma

Multiway systems

exprs + one-way rules

Inference systems

modus ponens : A , A  B / B
{x,xy}y
propositions + parametrized propositions (AKA axiom schemas)
For strings, we are asserting S
Our axioms are all just string assertions X
Module[{a},With[{t=a⊼(a⊼a),i=#1⊼(#2⊼#2)&},Join[Thread[axiomst],{i[t⊼(b⊼c),c]t,i[t,b]b,i[i[a,b],b]i[i[b,a],a]}]]]
In[]:=
Module[{a},With[{t=a⊼(a⊼a),i=#1⊼(#2⊼#2)&},Join[Thread[{(a⊼(b⊼c))⊼(((d⊼c)⊼((a⊼d)⊼(a⊼d)))⊼(a⊼(a⊼b)))}t],{i[t⊼(b⊼c),c]t,i[t,b]b,i[i[a,b],b]i[i[b,a],a]}]]]
Out[]=
{((a$355592⊼(b⊼c))⊼(((d⊼c)⊼((a$355592⊼d)⊼(a$355592⊼d)))⊼(a$355592⊼(a$355592⊼b))))(a$355592⊼(a$355592⊼a$355592)),(((a$355592⊼(a$355592⊼a$355592))⊼(b⊼c))⊼(c⊼c))(a$355592⊼(a$355592⊼a$355592)),((a$355592⊼(a$355592⊼a$355592))⊼(b⊼b))b,((a$355592⊼(b⊼b))⊼(b⊼b))((b⊼(a$355592⊼a$355592))⊼(a$355592⊼a$355592))}
In[]:=
BooleanMinimize[a⊼(a⊼a)]
Out[]=
True

Examples

In[]:=
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"StatesGraph"]
Out[]=
In[]:=
ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&@{"A""AB","BB""A"},{"A"},5,"StatesGraph"]//LayeredGraphPlot
Out[]=
Is a one-way multiway system an idealization of modus ponens?

“Modus Ponens” Multiway System

"ABBAAAAA"
{{"AB","BAA"},{"BAA","AAA"}}
Say we have proved so far:
{"AB"->"BAA","BAA"->"AAA"}
Let’s imagine our axioms are:
{"A""AB","BB""A"}
What can we derive?
Can we apply these to substrings?
ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"StatesGraph"]
First step: we have a bag of transformation rules
{"A""AB","BB""A"}
Apply the transformation rules to a starting string....
This generates a bunch of derived transformation rules. Now we take each generated state, and apply not just the original rules, but also the derived transformation rules.

Encoding logic

nand expr  nand expr
In[]:=
BooleanTable[Nand[Nand[a,b],Nand[a,b]],{a,b}]
Out[]=
{True,False,False,False}
In[]:=
BooleanTable[a,{a,b}]
Out[]=
{True,True,False,False}
For equational logic, want to know for which operator tables, blah = blah
https://www.wolframscience.com/nks/p781--implications-for-mathematics-and-its-foundations/ : things equivalent to true
Can we do sub-substitution with implication:
(a.b).(b.c)(a.c)
((x.y).(y.z)).(w.x)
((x.y).(y.z)).(w.x)(x.z).(w.x)(*???*)
In[]:=
Nand[False,True]
Out[]=
True
In[]:=
FalseTrue
Out[]=
True
In[]:=
Nand[True,True]
Out[]=
False
Claim: does work for Equal; doesn’t work for Implies
​

Conversion from modus ponens to equational

Assuming :
(1)ppqq​​(2)q(pp)q​​(3)(pq)q(qp)p
https://www.wolframscience.com/nks/p803--implications-for-mathematics-and-its-foundations/
Then
{ap.p,a.bp.p}
yields
b=p.p
In[]:=
Implies[p,p]//BooleanMinimize
Out[]=
True
{b==(p.p).b}(*byaxiom2*)
{ba.b}(*byfirstassertion*)

Picture of idealized math

expressions are propositions
arrows are “follows from” (which might be implication) [ nothing but substitutions ]
“Ancient Greek ‘implication’” : “material implication”
Perhaps “intuitionistic implication”

​

In the derivation of a theorem, I might use several previous theorems, or I might just use axioms.
Theorem is a pair here. Proof is the path from one part of the pair to the other.
Given a multiplication table, I can color equal items in this picture....
I can find a multiplication table that agrees with the axioms
(Completeness : model can give everything the axioms give)