### Constants vs Variables

Constants vs Variables

Constants are transformed locally

Variables are transformed globally

Variables are transformed globally

(co)Substitutions create and destroy constants/variables

Presence of constants does not convey any information

Fermions vs bosons

The difference starts to be apparent during evolution

In[]:=

coSubstitutionLemmas[f[g[a_],b_,a_],g[a_]->h]

Out[]=

{{1,1},1}f[g[h],b_,g[a$2266_]],{{1},1}f[h,b_,a$2266_],{{2},1}f[g[a_],h,a_],{{3},1}f[g[g[a$2266_]],b_,h]

In[]:=

coSubstitutionLemmas[f[g[a],b_,a],g[a]->h]

Out[]=

{{1},1}f[h,b_,a],{{2},1}f[g[a],h,a]

Variables are equalizing parts of an expression/tree

Variables can be changed to anything (they vary) - ForAll

Constants can only be changed with the appropriate cosubstitution rule including those constans explicitly

Variables can be changed to anything (they vary) - ForAll

Constants can only be changed with the appropriate cosubstitution rule including those constans explicitly

Variables are arguments to ForAll

Constants are arguments to Exists. Skolemization introduces new constants by removing existential qualifiers.

Constants are arguments to Exists. Skolemization introduces new constants by removing existential qualifiers.

Constants are unique, conjoined.

In[]:=

AxiomaticTheory["GroupAxioms"]

Out[]=

a.⊗(b.⊗c.)(a.⊗b.)⊗c.,a.⊗a.,a.⊗

∀

{a.,b.,c.}

∀

a.

1

∀

a.

a.

1

In[]:=

AxiomaticTheoryTWP@AxiomaticTheory["GroupAxioms"]

Out[]=

{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗a_,a_⊗}

1

a_

1

substitutionLemmas[f[g[a],b_,a_],a->h]

Variables are generated and destroyed by substitutions/rules/events.

Constants are generated and destroyed by observers.

Constants are generated and destroyed by observers.

Mathematicians focus on observer events that generate constants

Universe runs on universal metamathematics rules coarse-grained into known laws of physics