Constructive Operational Type Theory (COTT) is a work-in-progress theory of mathematics, wherein operations are recognised as the primitive objects of math, and numbers as merely representations. It's a combination of theories including Principled Emergence Metatheory, Traction Theory, and Mirror Calculus.
Principled Emergence Metatheory (PEM) is intended to be a formalization of elegance applied to mathematics, a set of criteria by which elegance can be measured and quantified, and a set of guidelines for developing elegant theories. PEM emphasizes developing theories with fewer axioms, justifying axioms from core principles, and re-using structure from existing theories ("reframing"). PEM encourages the development of theories for the sake of making mathematics more broadly approachable, applicable, and inclusive, even if it sacrifices some level of precision or rigor.
Traction Theory is intended to be the algebra without limits (pun intended). Following the guidelines of PEM, traction algebra is driven by a core principle of totality (all operations are always defined for all values) and reversibility (no information loss). This results in a "maximally tractable" algebra, wherein nothing is undefined, any expression may be rewritten, and invariants are contextual.
Mirror Calculus is intended to be the calculus of zero and its reciprocal. Under this theory, 0 represents differentiation, its reciprocal ω represents integration, and their composition 0ω=1. It emphasizes the utility of differentials over derivatives, the non-nilpotence of zero, and how 0 and ω behave as boundary operators.
This document serves as a notebook for me to keep track of all the work I've done so far in a clear, concise format. It's a workbook for experimentation, and a reference book for everything COTT. It may contain incorrect, outdated, or speculative details.
Unary operations do not conserve information, they either create or extract information. Therefore, they exist outside an information-conservative type.
This doesn't imply that their use is off-limits, however. It only means that their employment must be separated from the symbolic manipulations of an information-conservative type.
The most primitive elements of COTT are number generators. There are four primitive number generators: 1, -1, 0, and ω.
These generators are defined as a formalization, to emphasize how operations are more primitive than numbers, because operations are required to construct numbers. It's like Peano arithmetic, but with four generators instead of one.
Given n is a positive integer:
|
1(n)
|
-(n)
|
0(n)
|
w(n)
|
The 1-generator generates successively larger numbers. For convenience of notation, 1(n) may be written as simply n.
The negative-generator generates successively smaller numbers. All negative numbers are smaller than any positive number. For convenience of notation, -(n) may be written as simply -n.
The zero-generator generates zero-magnitude numbers. All zero numbers are larger than any negative number and smaller than any positive number, but they all have identical magnitude. Unlike in classic arithmetic, equal magnitude does not necessarily mean equal value.
The ω-generator generates infinite-magnitude numbers. All ω numbers are larger than all positive, negative, and zero numbers, but similar to zero numbers, they all have identical magnitude.
Projections extract information from an expression, erasing invariants.
Magnitude measures an expression as a positive 1-generator, 0, or ω, whichever is largest.
Projections to classic types are useful for taking measurements and comparing results between COTT and more traditional techniques.
Or, for ad-hoc or contextual projections without a formal meaning, one may also use:
Or, the more informal:
Other projections such as sign, phase, residual, and equivalence class may be defined, alongside any other ad-hoc or contextual projections as necessary, as they don't carry the burden of totality and reversibility.
Binary operations must be total and reversible under COTT. In classic algebraic theories, reversal operations (such as subtraction and division) would be derived rather than defined. But since reversibility is a requirement under COTT, we define both simultaneously as a single operation.
We define addition and subtraction mutual inverses.
Given any terms a, b, and c:
Subtraction is addition of the inverse:
Subtraction recovers addition:
Addition is associative:
A zero displacement has no change in magnitude:
Subtraction of a term from itself results in erasure:
Adding one always results in a greater value.
We define multiplication and division as mutual inverses.
Given any integers p and q, and terms a, b, and c:
Dividing 1 by any term produces its reciprocal. Dividing any term by itself produces unity.
Multiplication is associative:
Multiplication is distributive over addition:
Multiplication mixes equivalence classes:
| ↓ × → | 1 | 0 | -1 | ω |
|---|---|---|---|---|
| 1 | 1 | 0 | -1 | ω |
| 0 | 0 | 0^2 | -0 | 1 |
| -1 | -1 | -0 | 1 | -ω |
| ω | ω | 1 | -ω | w^2 |
Division mixes equivalence classes:
| ↓ ÷ → | 1 | 0 | -1 | ω |
|---|---|---|---|---|
| 1 | 1 | ω | -1 | 0 |
| 0 | 0 | 1 | -0 | 0^2 |
| -1 | -1 | -ω | 1 | -0 |
| ω | ω | w^2 | -ω | 1 |
The analytic extensions of exp and log are broadly understood. Those details will not be duplicated here. Instead, this section focuses on their extension into base-0 and base-ω.
For base v∈{0,ω} and all terms a,b,c:
| | Exponentiation | | | Logarithm | |
|---|---|
|
---
v^{log_{v}{a}}=a
|
log_{v}{v^a}=a
|
|
---
v^a * v^b = v^{a+b}
|
log_{v}{a*b}=log_{v}{a}+log_{v}{b}
|
|
---
{v^a}/{v^b}=v^{a-b}
|
log_{v}{a/b}=log_{v}{a}-log_{v}{b}
|
|
---
(v^a)^b=v^{a*b}
|
b*log_{v}{a}=log_{v}{a^b}
|
|
---
v^a=v^b <=> a=b
|
log_{v}{a}=log_{v}{b}<=>a=b
|
Given any integer n:
0^a = b |
log_{0}{b} = a |
|---|---|
|
0^0 = 1
|
log_{0}{1}=0
|
|
0^1 = 0
|
log_{0}{0}=1
|
|
0^n = 0 * 0·...
|
log_{0}{0^n}=n
|
|
0^{0^n} = n
|
log_{0}{n}= 0^n
|
|
0^{-n}=w^n
|
log_{0}{w^n}=-n
|
|
0^{w^n}=-n
|
log_{0}(-n)=w^n
|
Given any integer n:
w^a = b |
log_{w}{b} = a |
|---|---|
|
w^0 = 1
|
log_{w}{1}=0
|
|
w^1 = w
|
log_{w}{w}=1
|
|
w^n = w * w·...
|
log_{w}{w^n}=n
|
|
w^{w^n} = 1/{-n}
|
log_{w}{1/{-n}}= w^n
|
|
w^{-n}=0^n
|
log_{w}{0^n}=-n
|
|
w^{0^n}=-n
|
log_{w}(-n)=0^n
|
This theory starts with a simple goal: a total, reversible algebra. The intent is to make the fewest changes necessary to achieve this goal. However, every aspect of classic mathematics fights against totality and reversibility. Undefinedness and erasure are so deeply rooted, that a complete overhaul was necessary.
Every design choice of this theory will be justified on the basis of supporting totality and reversibility. Any design choice that does not directly support the stated goal is considered a mistake.
Number generators were chosen due to the need for different equivalence classes when defining the operations. Traditionally, two numbers are considered equal if they have the same magnitude. Complex numbers break this pattern, as phase determines equality regardless of magnitude. Number generators are a generalization of this concept: values are constructed by an operational history, with invariants defined by known equivalences, identities, and rewrite rules. Context-specific and informal invariants may be defined by projections - this is no different from what is practiced classically: we're just saying the quiet part out loud.
The intent is for addition and subtraction to work exactly the same as before, but without 0 being an absorbing element. Classically, the additive identity forces all structure to collapse when in multiplicative associativity with 0. So the only change here is to make the additive identity apply only to magnitude, and to limit erasure to x-x expressions.
This is where the major changes begin to occur. Zero now has a reciprocal, expressions like 2*0 don't collapse, and we begin to see why types are defined as the closure of operations rather than as collections of numbers - because many of these expressions cannot be evaluated numerically.
This section is where the real work happens. Let's walk through it step by step.
For any base x, we know x^0=1. Therefore, 0^0=1 and w^0=1.
And, x^1=x. Therefore, 0^1=0 and w^1=w.
We've defined 1/0=w, and we know x^{-1}=1/x. Therefore, 0^{-1}=w and w^{-1}=0.
This leaves only 0^{w} and w^{w}, so to complete the image we define them both as 0^{w}=-1 and w^{w}=-1.
These identities appear to be forced, once totality and reversibility are required, and no additional structure is permitted for definition. Therefore, it is a minimal and emergent structure.
We started with a simple principle: a total, reversible algebra. Every aspect of classic mathematics fought against us. We had to essentially reinvent everything from the ground up, just to remove the restrictions on zero. But, we didn't contrive any new structure - we merely took existing structure and reframed it. Addition, subtraction, multiplication, division, exponentiation, and logarithm are still the same as they were before, but extended to a framework that allows zero-magnitude displacement and a reciprocal of zero. Beyond this, we didn't invent anything new.
And now, we shall discover the fruit of our labor: the emergence of zero-magnitude algebra.
Derivation:
Derivation: