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