## General Minimal Models for Metamathematics

General Minimal Models for Metamathematics

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

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]

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]

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]

[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”]

[To make “meaningful math”, the initial condition should be something “meaningful”]

Axioms are of the form lhs (a pattern) rhs

#### [ Type theory analog ]

[ Type theory analog ]

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

“Axioms” are type constructors

“Axioms” are type constructors

#### [ Type 1 subcases: reversible vs not ]

[ Type 1 subcases: reversible vs not ]

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

#### [ Two forms of equality ]

[ 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

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]

[i.e. negation at the metalogic level is not generally decidable]

#### [ Events are just edges ]

[ Events are just edges ]

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

[ 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 ...

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

#### They also involve Except[ ] etc.

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

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

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

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

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

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

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:

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

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

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

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 ]

[ I.e. it’s a tree ]

#### The full cone is all possible proofs....

The full cone is all possible proofs....

### Entailment

Entailment

## Critical Pair Lemmas

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

Quantum Mathematics

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

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

[[ cf quantum switch ]]

#### What does a mathematical observer see?

What does a mathematical observer see?

One possibility: They only see textbook statements; no proofs

[you quote theorems not 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?

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

Superposition in mathematics

Combining theorems vs. combining pieces of paths

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

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

### Virtual particles ~ generated variables

Virtual particles ~ generated variables

## Proof Simplification

Proof Simplification

#### There is a geodesic proof

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

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 ]

[ I.e. it’s a tree ]

#### The full cone is all possible proofs....

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

Proof graph is the deduplicated tree