## Idealizations of mathematics

Idealizations of mathematics

### Equational logic

Equational logic

exprs + two-way rules

### Theorem network

Theorem network

lemma

### Multiway systems

Multiway systems

exprs + one-way rules

### Inference systems

Inference systems

modus ponens : A , A B / B

{x,xy}y

propositions + parametrized propositions (AKA axiom schemas)

For strings, we are asserting S

Our axioms are all just string assertions X

Our axioms are all just string assertions X

Module[{a},With[{t=a⊼(a⊼a),i=#1⊼(#2⊼#2)&},Join[Thread[axiomst],{i[t⊼(b⊼c),c]t,i[t,b]b,i[i[a,b],b]i[i[b,a],a]}]]]

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

In[]:=

{((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))}

Out[]=

BooleanMinimize[a⊼(a⊼a)]

In[]:=

True

Out[]=

## Examples

Examples

ResourceFunction["MultiwaySystem"][{"A""AB","BB""A"},{"A"},5,"StatesGraph"]

In[]:=

Out[]=

ResourceFunction["MultiwaySystem"][Join[#,Reverse/@#]&@{"A""AB","BB""A"},{"A"},5,"StatesGraph"]//LayeredGraphPlot

In[]:=

Out[]=

Is a one-way multiway system an idealization of modus ponens?

## “Modus Ponens” Multiway System

“Modus Ponens” Multiway System

"ABBAAAAA"

{{"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

Encoding logic

nand expr nand expr

BooleanTable[Nand[Nand[a,b],Nand[a,b]],{a,b}]

In[]:=

{True,False,False,False}

Out[]=

BooleanTable[a,{a,b}]

In[]:=

{True,True,False,False}

Out[]=

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)(*???*)

Nand[False,True]

In[]:=

True

Out[]=

FalseTrue

In[]:=

True

Out[]=

Nand[True,True]

In[]:=

False

Out[]=

Claim: does work for Equal; doesn’t work for Implies

#### Conversion from modus ponens to equational

Conversion from modus ponens to equational

Assuming :

https://www.wolframscience.com/nks/p803--implications-for-mathematics-and-its-foundations/

Then

yields

### Picture of idealized math

Picture of idealized math

expressions are propositions

arrows are “follows from” (which might be implication) [ nothing but substitutions ]

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)