PeanoScript tutorial

PeanoScript is an experimental proof assistant for Peano Arithmetic based on TypeScript syntax, with the goal of being easy for programmers.

Benefits from reading this page may include:

1. You will be able to formally prove mathematical statements.
2. You will be able to run your proofs as programs. For example, a proof of the infinitude of primes is also a program that takes a number n and returns a prime number greater than n .
3. You will understand why some proofs are not programs (the difference between constructive and classical logic).
4. You will learn what those "Pi types" and "Sigma types" people talk about are (it's actually simple).

Peano Arithmetic

Peano arithmetic is a mathematical system that combines first-order logic with axioms about the natural numbers. To express the axioms, it uses the symbols0 (zero), succ (the successor function a.k.a."x+1"), + (addition), and* (multiplication).

It's one of the simplest logical systems that still allows us to prove many interesting statements. In this tutorial, we will be using the above axioms, together with the rules of logic, to learn proving things to a computer.

The natural numbers

The basic kind of object we're dealing with is a natural number. These are the numbers 0, 1, 2, 3, ... . We can assign them to variables using const variableName = number;.

Every variable has a type, which can be seen by hovering it. We can optionally specify the type usingconst variableName: type = number;, though usually it will be inferred. The type of a number is just the number.

We can also print variables and expressions using console.log(thing);. Because PeanoScript doesn't have input, the results are immediately known and displayed inside the editor.

Arabic numerals in PeanoScript are actually syntax sugar for the more fundamental way of writing numbers using the successor function succ. We can write the numbers 0, 1, 2, 3, ... as 0, succ(0), succ(succ(0)), succ(succ(succ(0))), ... .

Arithmetic expressions

We can also add and multiply numbers together, forming arithmetic expressions. The value of such an expression is a number. Its type is the literal expression, for example, the type of 1+1 is 1+1.

The order of operations is meaningful: 1+2+3 is interpreted as (1+2)+3, which is different from 1+(2+3).

Equality

Another kind of object is a proposition, which is a statement about numbers. The most basic thing we can say is that two numbers are equal, which we write as a == b. When a variable has the type a == b, it means its value is a proof of a == b. For a number x, we can obtain a proof of x == x using eqRefl(x). This stands for the reflexive property of equality, that is: for all x, x equals x.

The value of an equality is displayed as (eq)

We can obtain slightly more interesting equalities using the arithmetic-defining axioms. They can be accessed as the functions addZero, addSucc, mulZero, and mulSucc.

Equality has some properties we can use:

• Symmetry: if a == b, then b == a. We can use this by calling aEqualsB.symm().
• Transitivity: if a == b and b == c, then a == c. We can use this by calling aEqualsB.trans(bEqualsC)
• If a == b and f is a function, then f(a) == f(b). We can use this by calling aEqualsB.map(f), for example aEqualsB.map(succ).

And just like that, we've breezed through the first 760 pages of Principia Mathematica!

Apologizing to the compiler

Sometimes when we write a proof, we aren't sure how to complete a given part. We can use sorry whenever we need some proposition, and it will be accepted by the compiler. sorry is like a variable of type any in TypeScript, which can be implicitly converted into any other type.

This document has some exercises so you can make sure you follow. They work by asking you to replace the sorry in some code with real proofs. Try it now!

And a bonus challenge exercise:

Functions are implications

In logic, there is an important concept of implication ("A → B"). We can prove A → B by assuming A and proving B under that assumption. Then given a proof of A → B and a proof of A, we can combine them to obtain a proof of B.

This is much like the concept of a function with a parameter of type A and return type B:

In most programming, we mostly care about the implementation of a function. The fact that a function can be used to obtain a given result type is trivial, since all types have instances: for example, we can obtain a string with "abc". In PeanoScript, a type like 0 == 1 represents a false proposition, and therefore can't be instantiated (without using sorry). That makes it interesting to explore the implications, that is functions, between types.

Like in TypeScript, we write the type of a function together with an argument name, though the name is not meaningful and might as well be "_". For example, the type of a function from A to B can be written (a: A) => B or (_: A) => B.

We write a function using arrow/lambda notation, for example (a: A) => .... The "..." can be an expression or a curly brace block with a return statement. We can optionally specify the return type like (a: A): B => ..., though usually it will be inferred.

To create a variable that is a function, we can use the shorthand syntax function funcName(a: A): B{...}.

To work with functions, we will want to make use of the type panel on the right of the code editor. The panel shows variables we have in the current context and the type we want to return from the current block or expression. Variables defined at the top level are omitted, with the hope that you write type annotations for those.

Because the type panel only works on valid code, you will want to use a lot of sorry and return sorry;, and gradually de-sorrify your code as you go.

We can also have implications where the left or right side is an implication. This corresponds to a function where the parameter or return value is a function.

Multi-argument functions and currying

PeanoScript uses currying, a technique where multi-argument functions are represented as chained single-argument functions. For example, instead of (x, y) => ..., we may have x => y => .... This is occasionally convenient because we can make use of a partially applied function:

However, defining and calling functions this way is rather un-ergonomic. For this reason, we can use the usual multi-argument syntax, it's just defined to do the same thing as the curried version.

For all n

In logic, there is a concept of the universal quantifier "∀" (for all). It can be used to express that something is true for all numbers. For example, to say that for all n, n*2 == n + n, we can write: "∀n. n*2 = n + n". In fact, we've already been using ∀: eqRefl is written as "∀n. n = n", and addSucc is written as "∀n. ∀m. n + succ(m) = succ(n + m)".

It makes sense that we can call eqRefl with some number and get the self-equality for that number. However, there is a difference with the usual functions/implications. Normally a function has some return type, and whatever we call it with, it will return that type. But what eqRefl returns depends on the argument. This is called a Pi type or a dependent function type.

In PeanoScript, we write universal statements the same way as implications. To specify that the parameter type is a natural number, we write N (for ℕ, the natural numbers). For example, the type ofeqRefl is written as (x: N) => x == x. We can even create our own version of eqRefl:

Combining this with proposition arguments, we can prove interesting statements for arbitrary numbers:

Try it in an exercise:

For manipulating types with variables in them, we can use another built-in function called replaceAll. Calling replaceAll(p, eq) where p is some proposition and eq is var == Expr will replace all occurrences of var in p with Expr.

"for" all n? 😏

For loops in programming are often used in a certain pattern: we iterate over some range of numbers, and accumulate a result in an outside variable.

The pattern is also used by the reduce function:

Given this pattern, we could imagine another version of the for loop:

1. We would declare an additional variable inside the for loop for the accumulator. (let i = 0; let sum = 0;)
2. The continue statement would take a value like continue sum + i;. The loop body would have to end in a continue, which would give the new value for the accumulator.
3. The for loop would be an expression instead of a statement, and its value would be the final value of the accumulator.

It would look like this:

It's not clear if this idea will be accepted in mainstream programming languages. However, it's very useful for us now. Consider trying to prove something for all n, for example, that 0 + n == n. This seems impossible to do with just addZero and addSucc - we would have to "move" n succs to the left of the + to use addZero(n), but we can only write a finite amount of code.

However, if we had a way to move a single succ to the left, we could apply it n times:

We write a for loop expression as:

for(let i = 0; let acc: accType = base; i < bound; i++){
    // (statements...)
    continue newAcc;
}

Where:

1. i and acc are identifiers.
2. accType is a type dependent on i, for example 0 + i == i. This represents a property of i, and acc is the proof that this property holds.
3. base is an expression which is the initial value of acc. Becuase i is initially zero, the type of base is accType, but with i replaced by 0. For example, if accType is 0 + i == i, then the type of base must be 0 + 0 == 0. This substitution is often written as accType[i:=0].
4. bound is an arithmetic expression. This is the final value of i when the for loop is completed.
5. Inside the curly braces, we have access to the number variable i and to acc of type accType, as we declared. Because i will be incremented, we need to update acc to be a valid proof of the property for the new value of i. That is, we need to use a continue newAcc; statement, where newAcc is an expression with the type accType[i:=succ(i)]. For example, if accType is 0 + i == i, then newAcc must be of type 0 + succ(i) == succ(i).

The value of the for loop expression is the value of acc after running bound iterations of the for loop. The type of this value is accType[i:=bound]. For example, if accType is 0 + i == i and bound is n, the type of the for loop expression is 0 + n == n.

If the desired type of the for expression is known and bound is a variable, accType can be guessed to be desiredType[bound:=i]. For example, in zeroAdd we return the for loop from a function with the return type annotation 0 + n == n, and the bound is n. So even without a type annotation on acc, accType would be guessed to be (0 + n == n)[n:=i] which is 0 + i == i.

Try the for loop in an exercise:

It's time to prove the commutative property of addition, a + b == b + a:

Getting help

We could continue to prove the distributivity of addition ((a+b)+c == a+(b+c)) and the same properties for multiplication. While that would be achievable, explicitly using these properties in proofs takes a lot of effort, which can be allocated to more interesting things.

We can use the ring built-in to automatically transform an equation into an equivalent equation. This will work as long as the transformation is only composed of moving things around and subtracting un-adding things from both sides.

To be precise, given a variable eq of type A == B, ring(eq) will be accepted as type C == D if A-B = C-D or A-B = D-C as polynomials.

When the sides of an equation cancel out, we can use ring() as a shorthand for ring(eqRefl(0))

With ring, we can make use of the as keyword. In TypeScript, someVar as someType is used to assert that someVar is of type someType, even if the type system can't prove it. Since we require soundness, as is more of an inline type annotation.

Try it out in an exercise:

And

Another common logical connective is the conjunction "∧" (and). We can prove that A ∧ B is true by proving A and proving B. Given A ∧ B, we can deduce A and we can also deduce B.

This is similar to a data structure that simply holds two elements, with the types A and B. For example, consider the TypeScript type type Person = {name: string; id: number}. We can create an object of this type using some string and some number, for example {name: "Alice", id: 7}. Given an object of this type, say person1 : Person, we can retrieve a string and a number using person1.name and person1.id.

TypeScript also has a suggestively named type operator &. It can merge two object types, for example, Person can also be written as {name: string} & {id: number}. However, this merging is a bit messier than the logical concept of And. If types A and B have a common property, it gets merged into one property in A & B, which means that creating an object of type A & B from a : A and b : B loses information.

In PeanoScript, we use a "tagged" version of & written as &&. In TypeScript terms, the type A && B is {left: A; right: B}, which is also the same as {left: A} & {right: B}.

We can create an object of type A && B using a : A and b : B. We write {left: a, right: b} or we can use the shorthand expression-level syntax a && b.

To retrieve the proofs from ab : A && B, we can use ab.left and ab.right.

Try it out:

Exists

In logic, there is an existential quantifier "∃" (exists). A statement like ∃n. n*n == n can be read as "there exists a number n such that n*n == n". To prove such a statement we need to present a number n and a proof that n*n == n. Thus we can think of the value as a pair of a number and a proof of some property of that number.

We already have a way to represent pairs with &&. Recall the relation between implications such as (eq: 0 == 1) => 1 == 2 and For All statements such as (n: N) => n + 0 == 0. Exists statements are a similarly "upgraded" version of And. They can also be called dependent pair types or Sigma types.

Implications take in a proposition and return another proposition, and For All statements take in a number and return a proposition about that number. "And" statements store two propositions, and Exists statements store a number and a proposition about that number.

We write the type of an Exists statement as an object where the first field has type N, and the second field expresses some property of the first field. For example, ∃n. n*n == 1 can be written as{n: N; squaresToSelf: n*n == n}. To create a value of this type, we write the object. The second field's type will have the number variable replaced with the actual number provided. For example, {n: 1, squaresToSelf: ring()} works because the required type of squaresToSelf is 1 * 1 == 1 which ring() can be converted to.

Say we have defined const myExists: {n: N; squaresToSelf: n*n == n} = {n: 1, squaresToSelf: ring()};. How can we use it? With And, we used the dot syntax. However, it's not clear how it would work here: if we write myExists.n, we won't get 1, as the type abstracts away the concrete number. So we can only get some unkown number. myExists.squaresToSelfwould give us a proposition about some number, but we wouldn't have the number itself.

We need to unpack both elements of the object at once. For this, we can use the TS/JS destructuring syntax. We write const {n, squaresToSelf} = myExists; to obtain a new number n and a propositionsquaresToSelf which expresses a property of n.

In the case that we already have one of those names in the context and don't want to overwrite it, we can use the renaming syntax from: to on one or both of the names. For example,const {n: m, squaresToSelf} = myExists; will bind the number to m instead of n.

Exists can be used to describe many useful properties. For example, to express that n is even, we can use the type{half: N; isHalf: half*2 == n}. To express a ≤ b, we can use {difference: N; isDifference: a + difference == b}.

Here is an example showing that n*(n+1) is always even:

If you look at the console.log outputs, it looks like we've created a function that returns the sum 1+2+...+n. Indeed, this is a known property of n(n+1)/2, and we can also see in the implementation that we're adding i+1 to the accumulator in each iteration.

This is how we can create interesting functions in PeanoScript - if we want a N → N function with some property, we can declare a function (n: N) => {functionResult: N; propertyOfResult: ...}. Then we just need to construct the result that we want.

We can also use this to simply mess around with console.log. Consider that a given Exists type can have many implementations, for example, {n: N; squaresToSelf: n*n == n} can also be {n: 0, squaresToSelf: ring()}. In fact, the property can be completely trivial such as {n: N; isSelf: n == n} or even {n: N; obvious: 0 == 0}. We can use this to do arbitrary computations.

Unfortunately, we can't use this for anything in our proofs, as unpacking factorial(n) we'll get an opaque number and the information that 0 is equal to 0. There is an interesting definition of a factorial in the section "Infinitude of primes", as a number that is divisible by every number less or equal to n. Note that that definition also doesn't pin down the factorial function, as it is also satisfied by n!*2 or leastCommonMultiple(1,2,..., n).

Try out the exercise:

Or and Match

Yet another logical connective is ∨ (Or). We can prove A ∨ B by proving either A or B. Given A ∨ B, we can't deduce either of them back, since we don't know which one we put in 😉. However, if we also prove A → C and B → C together with A ∨ B, we can deduce C, as we've "covered both branches".

Again, there is a similar concept in TypeScript, but we opt for a double-charactered tagged version. PeanoScript's A || B is equivalent to TypeScript's {left: A} | {right: B}, that is a value of this type is one of the objects {left: A} or {right: B}.

(in actual TypeScript, we would probably write this as {side: "left"; value: A} | {side: "right"; value: B}, but the point is that it stores either A or B, and we can tell at runtime which one)

To create a value of type A || B, we simply create one of the objects such as {left: a} or {right: b}. In contrast to most other values, the type cannot be inferred as the value doesn't have the other side of the ||. Therefore creating Or values requires either a type annotation or as expression.

To use a value of type A || B, we use a match statement. Match statements exist in languages such as Rust and Swift, and have even been proposed for JavaScript. A match statement is like a more powerful switch statement that also works on objects. Importantly, it also allows to extract values from objects, much like JavaScript's object destructuring syntax.

Here is an example of what a match statement could look like in TypeScript (if it existed):

The PeanoScript match statement looks about the same:

Since we return a == b in both branches, the match statement is valid and the function is well-typed. Note that return is part of the function syntax, if we did a match statement inside a for loop we would end our cases with continue.

Since there are no side effects, the only point of a match statement is to escape the current function or for loop body with some value. If we'd like to use match for intermediary results, we can use a match expression. The value of a match expression comes from break someValue; statements in each branch.

We are now ready for a common Hello World of computer proofs. We can prove that every number is either even or odd, that is, for any n, there exists a k such that either k*2 == n or k*2 + 1 == n.

No is-even needed! Feel free to try the exercise:

False things are never true

Another important concept in logic is negation. We write ¬p for some proposition p to say that it is false. The related laws are:

1. We prove ¬p by deriving a contradiction from p.
2. Given p and ¬p, we can derive a contradiction.

But what is a contradicion? It is simply a special proposition, commonly written as ⊥. It's a common convention to simply consider ¬p as a syntax sugar for p → ⊥, which conserves the above laws. The law of ⊥ is simple.

1. (Principle of explosion) Given ⊥, we can conclude anything.

Where can we get such a ⊥? In Peano arithmetic, we have to use an axiom, only one of which has ⊥ anywhere: ∀n. succ(n) ≠ 0, which desugars to ∀n. ¬(succ(n) = 0), which desugars to ∀n. succ(n) = 0 → ⊥.

In TypeScript, there is a type called never. It's used for values that can't exist, for example, a function that loops forever has return type never.

Given this definition, it's logical that type never has something of a principle of explosion

In PeanoScript, we write the logical ⊥ as never. We can obtain it from the axiom succNotZero of type (n: N) => succ(n) != 0 which desugars to (n: N) => !(succ(n) == 0) which desugars to(n: N) => (_: succ(n) == 0) => never. When we have a value of type never, we can obtain a value of any type usingneverElim<anyType>(neverValue). The wanted type can also be inferred, giving neverElim(neverValue).

Though type never, well, never does anything, we can use it to exclude unwanted possibilities. For example, we might wish to subtract numbers, but this is not possible in general as we're not allowed to obtain a negative number. But if we can prove that a number n is not equal to 0, we can use this to obtain its predecessor:

It's a curious case of induction where we don't use the inductive hypothesis (acc is not used in the loop body), only the fact that we need to prove the statement for succ(i).

For the exercise, we can try to prove that 1 is not an even number.

Type generics and replace

When doing math, we usually don't express everything with quantifiers over equalities between arithmetic expressions (even when we could). We use higher-level concepts, for example "a is less than b" or "p is prime". We can define such concepts using formulas such as "lessEqual(a, b) ≔ ∃k. a + k = b" or "isPrime(n) ≔ n ≠ 1 ∧ ∀a. ∀b. a * b = n → (a = 1 ∨ b = 1)". In PeanoScript, we can define such concepts as generic types.

Formulas allow us to use the deepest and most fundamental law of equality. While replaceAll lets us replace all occurrences of a variable with something else, we might want to replace only some occurrences, or replace something that is not a variable (like n*n+7). Mathematically, if we have a formula φ, and A = B for arithmetic expressions A and B, and φ(A) is true, then φ(B) is true.

To use this principle, we can define a formula Phi using a generic type type Phi<n extends N> = ...; and then write replace<Phi> to get a value of the type(L: N, R: N, eqLR: L == R, propOfL: Phi<L>) => Phi<R>.

We can use replace to replicate every other equality-related function, except for eqRefl:

For an exercise, try proving the transitivity of equality using only replace:

Constructive logic vs the excluded middle

In classical logic, we can always get p or not p for any proposition p. Constructive logic famously rejects this. Consider that p could encode famous math problems like P != NP, or the halting of an arbitrary Turing machine. It does intuitively seem that such statements are either true or false, but being able to obtain a value of the type p || !p causes some problems. If we treat our proofs as programs, it would mean we could console.log such a value and magically obtain an answer to any question.

We can access p || !p using excludedMiddle<p>, however, our code won't be runnable.

But don't we sometimes need a proposition to be either true or false?

As it turns out, the lack of excluded middle does not stop us from getting p || !p for many propositions p. It's just that we have to prove it, that is prove either p or !p. If we can do this, we say that p is decidable.

It's a curious algorithm, basically using for loops to subtract 1 until one of the numbers is 0. Here's what it would look like translated to JavaScript (x == y || x != y is represented as a boolean):

Try to prove the decidability of lessEqual<a,b>. It's similar to the decidability of equality, you don't need to use previous theorems.

Cool thing: infinitude of primes

To showcase the capabilities of PeanoScript, here is a proof of the infinitude of primes. Since sets are not supported, we use the form "for all n, there exists a prime greater than n".

What to do next

You may try things out and prove some theorems in PeanoScript. However, if you want to go deep, there are some limitations as the language is limited to first-order reasoning on natural numbers.

The good version of this is called "type theory" or "dependently typed programming". It's a bit more of a mind shift, but hopefully what you've learned will help you understand it. Full dependently typed languages allow you to do pretty much any kind of math, as well as code up pretty much any program and prove its correctness.

For a programmer-friendly introduction to dependent types, I recommend the book The Little Typer. For serious math and formal verification, the big thing seems to be Lean 4, you can see their list of resources.

Have fun!

Bonus exercises

If you're looking for inspiration, you can try these bonus exercises. They are not tested so they might be wrong and/or not humanly doable. You can paste them in the playground and solve.