Transitivity : syntactic

Extensionality

Extensionality

#### Causal invariance in metamathematics

Causal invariance in metamathematics

[ If strongly normalizing (= every rewrite sequence reaches normal form), then confluence implies: everything easy ]

FindEquationalProof :

if the system is confluent, any path in the equational multiway system will work (apart from the infinity problem)

if the system is confluent, any path in the equational multiway system will work (apart from the infinity problem)

Given confluence, algorithm to prove a theorem is trivial , but may take a long time to run

[ algorithm to find an optimal proof may be nontrivial ]

[ algorithm to find an optimal proof may be nontrivial ]

#### Representations of math

Representations of math

#### FindEquationalProof

FindEquationalProof

Is only inbuilt predicate

Predicate logic:

implies[x,y]

FindEquationalProof[implies[a,c],{ForAll[implies[