Metamath
Metamath
http://us.metamath.org/mpeuni/mmset.html#proofs
Statements
Definitions : gives a name to a statement
Functions / Constants / Variables
Definitions : gives a name to a statement
Functions / Constants / Variables
A well-formed statement is associated with the wff constant
⊢ is also a constant
Workflow: define possible symbolic expressions
Then see how some expressions can be derived from others by repeated substitution
Workflow: define possible symbolic expressions
Then see how some expressions can be derived from others by repeated substitution
Then see how some expressions can be derived from others by repeated substitution
Start with a giant ocean of syntactic expressions .... then see what chains of substitution there are within these....
Then there is some connected component that contains axioms we like
Then there is some connected component that contains axioms we like
Substitution is 2 inputs, 1 output
Substitution is 2 inputs, 1 output