General Minimal Models for Metamathematics

Type 1: axioms are fixed, and things are being derived [the fundamental input is axioms]

[ This is like the usual formulation of the physics project ]
{{x,y},{y,z}}->{{x,x},{y,z},{y,w}}
{{2,3},XXXX}
Code ≠ data
[[ For math, this is primarily about equational axioms ]] [ cf universal algebra ]

Case 1: Data is expressions, and theorems are connected pairs of expressions [first NKS version]

“Law of entailment” is application of an axiom [this is like substitution ? ]
Here, initial conditions are whatever expressions we want, and we are forming connected graphs of things equal to them

Case 2: Data is theorems [which are also expressions] [second NKS version]

The only way to build is with raw axioms
[but this is very inefficient compared to lemmas]
Entailment is substitution using the axioms
Here, the initial condition must be something representing “true”
[To make “meaningful math”, the initial condition should be something “meaningful”]
Axioms are of the form lhs (a pattern)  rhs

[ Type theory analog ]

We start from the “always inhabited” type [“1”]
“Axioms” are type constructors

[ Type 1 subcases: reversible vs not ]

In ordinary math axioms, the rules are two-way [for equational axioms]

[ Two forms of equality ]

Within an expression ... some of its symbolic constructs could represent equality
Between expressions ... there is a built-in metalogic notion of equivalence
Negation: within an expression, it’s just some transformation on the expression represents its negation [NKS form]
Negation between expressions: “you can’t get there from here”
[i.e. negation at the metalogic level is not generally decidable]

[ Events are just edges ]

[ There are a fixed number of rules, except when we add “already proved” entailments ]

Though in practice there may be “shared-subexpression-style” optimization (which corresponds to lemmas)
Every path can be reduced to a new “axiom”. I.e. if x ⊢y ;;; x ⤳ y
[ For strings, a pattern entailment is the same as an ordinary entailment ]

Type 1a : the axioms are not purely substitutional ...

They also involve Except[ ] etc.

I.e. the patterns define metalogic
Except[ ] effectively defines a version of negation
(( FindEquationalProof[ ] allows != ... which is like having Except[ ] ))

Type 2: axioms + propositions are progressively being added

In type 2, the axioms have to be represented the same way as the rules....

Case 1: Every proposition is an ↔ statement

Then it is self-evident that a proposition can be a rule, and the entailment obtained from applying one proposition to another is (fairly) straightforward

Case 2: Proposition aren’t necessary ↔ statements

Then the entailment might be much more complicated
E.g. apply e[f[_],g[x_]] to h[g[x_],f[g[y_],x_]]
f[x_,y_],g[a_,b_]
x_↔y_,g[a_,b_]
One possibility: non ↔ propositions can never be used to be events

General case: Type 2 system maintain giant vats of true propositions

The progress of mathematics is the expansion of the contents of the vat

We can try to identify the complement, which would be the false statements

Basic assumption of Type 2:

Anything xxx is semantically equivalent to xxx ↔ True
This means that anything can become a rule that can be used for substitution
https://www.wolframscience.com/nks/notes-12-9--truth-and-falsity-in-formal-systems/
https://www.wolframscience.com/nks/notes-12-9--truth-and-incompleteness/

How do you use a statement like PrimeQ[XXXX] in another proof?

PrimeQ[f[x_,g[y_]]]<->True

I.e. in type 2, a proof is a past entailment cone for a given proposition

Actually not the whole filled cone ... instead it is just a way to form the output from its various inputs
​[ I.e. it’s a tree ]

The full cone is all possible proofs....

Entailment

https://en.wikipedia.org/wiki/Logical_consequence
https://en.wikipedia.org/wiki/List_of_rules_of_inference

Critical Pair Lemmas

{o->a,o->b}
{o<->a,o<->b}a<->b
Normally, equality is timelike separation
Enforcing all critical pairs is like compressing the branchial graph by transitive closure....

Quantum Mathematics

What experiment can you do that will detect multiple proof paths (in Type 1 metamathematics)?

[[ cf quantum switch ]]

What does a mathematical observer see?

One possibility: They only see textbook statements; no proofs
[you quote theorems not proofs]
“Classical mathematics” is a single path from theorem to theorem
Concluding that the thing you got from a proof is a theorem you’re keeping is the analog of quantum measurement

What is the relation of fuzzy logic to quantum mathematics?

This is effectively assuming a continuous branchial space ; and it doesn’t preserve “coherent threads of history”

Superposition in mathematics

Combining theorems vs. combining pieces of paths

[ Concept of measurement will be different in type 1 and type 2 ]

Virtual particles ~ generated variables

Proof Simplification

There is a geodesic proof

But a theorem prover [with e.g. unfailing completion] might not find it
What does it look like to make proof-to-proof transformations? [There are very much like applying critical pair lemmas]
We should see this in our token-event graphs
[ What is the homotopic structure of the token-event graph ? ]
A proof takes its input axioms / assertions and generates its output result [the “proved theorem”]

I.e. in type 2, a proof is a past entailment cone for a given proposition

Actually not the whole filled cone ... instead it is just a way to form the output from its various inputs
​[ I.e. it’s a tree ]

The full cone is all possible proofs....

There is a geodesic tree that is the shortest tree......
[[ ? spanning trees of past entailment cone ]]

Proof graph is the deduplicated tree