Digital Miracle

Digital Miracle is yet another theorem-proving esoteric programming language invented by User:Hakerh400. This axiomatic system is a mixture of combinatory lambda calculus and inductive Peano arithmetic. Natural numbers are represented as Church numerals.

Overview

There are axioms. Each axiom can be understood as a built-in blackbox function. The type of the function corresponds to the statement that the axiom asserts.

A theorem is a function. It has a type signature and an implementation. Type signature is the proposition that the theorem aims to prove. The implementation is a combination of axioms and/or other theorems defined so far.

A function from type A to type B corresponds to an implication from proposition A to proposition B. Function application corresponds to Modus Ponens.

Combinators

A combinator represents a value in the combinatory logic. It can be understood as a function that takes an input and produces an output. Combinators are not theorems. Theorems are meta-functions that operate on propositions. Combinators are just type-level values that theorems can analyze.

There are three combinator constructors:

Name	Description
K	The K combinator from the SKI calculus
S	The S combinator from the SKI calculus
Call	Takes two combinators as arguments and produces a combinator that represents their application

The Call constructor can also be used in infix notation as (.) operator. For example, if we want to call S with argument K, we can write either Call S K, or S . K. We cannot just write S K.

Aliases

We introduce some additional combinators and their aliases:

Name	Value	Description
I	S . K . K	The identity function (Haskell equivalent: id)
D	S . (K . S) . K	The composition operator (Haskell equivalent: (.))
F	S . (D . D . S) . (K . K)	Flip arguments (Haskell equivalent: flip)
Zero	K . I	Church numeral 0
Suc	S . D	Successor of a Church numeral

Natural numbers

Natural numbers are represented as Church numerals. We have three axioms:

Axiom name	Statement	Description
NatZero	Nat Zero	Zero is a natural number
NatSuc	forall n. Nat n -> Nat (Suc . n)	Successor of a natural number is also a natural number
NatTran	forall n m. n == m -> Nat n -> Nat m	If two values are equal and the first one is a natural number, then the second one is also a natural number

Note: the dot after forall arguments is not the Call operator, but just a separator between arguments and the statement. For example:

forall n. Nat n -> Nat (Suc . n)
        ^                   ^
        Separator           Call

Equality

Finally, we have axioms regarding equality:

Axiom name	Statement	Description
Refl	forall a. a == a	Equality is reflexive
Com	forall a b. a == b -> b == a	Equality is commutative
Tran	forall a b c. a == b -> b == c -> a == c	Equality is transitive
Cong	forall f g a b. f == g -> a == b -> f . a == g . b	Function and argument congruence
Ext	forall f g. (forall a. f . a == g . a) -> f == g	Extensionality
KDef	forall a b. K . a . b == a	Definition of K combinator
SDef	forall a b c. S . a . b . c == a . c . (b . c)	Definition of S combinator
Cont	forall a b. K == S -> a == b	Contradiction elimination. It says that if we manage to prove that K and S are the same, we can prove any equality
Induct	forall f r n. f Zero == r -> (forall m. Nat m -> f m == r -> f (Suc . m) == r) -> Nat n -> f n == r	Induction over natural numbers

Syntax

Each theorem has a name, a type signature (proposition) and an implementation (proof). Recursion is strictly forbidden. A theorem cannot reference itself, or other theorems that are defined after it.

Examples

First, let's prove that $(\forall abc.a=b\to a=c\to c=b)$. It is similar to transitivity of equality, but some things are flipped. We can write a theorem for it:

tr1 :: forall a b c. a == b -> a == c -> c == b
tr1 ab ac = Tran (Com ac) ab

Explanation: The theorem takes two arguments. The first argument ab is a proof that $(a=b)$ and the second argument ac is a proof that $(a=c)$. When we apply axiom Com to ac, we get a proof that $(c=a)$. Then we apply axiom Tran to $(c=a)$ and $(a=b)$ to obtain $(c=b)$. ∎

We can also write the following theorem:

tr2 :: forall a b c. a == b -> b == c -> a == c
tr2 = Tran

It is equivalent to axiom Tran. Now, we can use these two theorems in infix notation. For example, tr2 P Q can be written as P `tr2` Q. They are left-associative when used in infix notation. Theorem tr1 modifies the left-hand side, while theorem tr2 modifies the right-hand side. We can use them to sequentially construct the statement we need based on the set of proofs we have so far.

Next, we can prove argument congruence and functional congruence:

acong :: forall f a b. a == b -> f . a == f . b
acong = Cong Refl

Explanation: Theorem acong states that if two combinators a and b are equal, we can call any combinator f with a and b and the results will be the same. We proved it by applying axiom Cong to axiom Refl. Type unifier does the magic.

And for functions:

fcong :: forall f g a. f == g -> f . a == g . a
fcong fg = Cong fg Refl

fcong2 :: forall f g a b. f == g -> f . a . b == g . a . b
fcong2 fg = fcong (fcong fg)

Now, something more interesting. Let's prove that $(\forall a.Ia=a)$. That is, the identity combinator returns the argument unchanged. Here is the theorem:

id :: forall a. I . a == a
id = Refl `tr2` SDef `tr2` KDef

Explanation: We start from Refl. Then we apply axiom SDef to the right-hand side, and then we apply axiom KDef to the right-hand side. How does it actually work? First, note that I is just an alias for S . K . K. We start from Refl, so we have S . K . K . a == S . K . K . a. Then we apply SDef to the RHS (right-hand side) obtaining S . K . K . a == K . a . (K . a). Finally we apply KDef to the RHS, obtaining S . K . K . a == a. Since I is S . K . K, it is equivalent to I . a = a. ∎

The next thing we want to prove is related to the D combinator. We want to prove that $(\forall abc.Dabc=a(bc))$. Here is the theorem:

dot :: forall a b c. D . a . b . c == a . (b . c)
dot = let
  dot_a = Refl `tr2` SDef `tr2` fcong KDef :: D . a == S . (K . a)
  in fcong2 dot_a `tr2` SDef `tr2` fcong KDef

Explanation: We use let statement to make proof more readable. We first prove dot_a, which states that $(\forall a.Da=S(Ka))$. Then we use dot_a to prove the final statement. ∎

Next, the F combinator: $(\forall abc.Fabc=acb)$. Theorem:

flip :: forall a b c. F . a . b . c == a . c . b
flip = let
  flip_a = Refl `tr2` SDef `tr2` fcong dot `tr2` acong KDef :: F . a == D . (S . a) . K
  flip_ab = fcong flip_a `tr2` dot :: F . a . b == S . a . (K . b)
  in fcong flip_ab `tr2` SDef `tr2` acong KDef

Explanation: Pretty straightforward, isn't it?

And one more thing at the end. Let's define a new combinator alias:

type FI = F . I

and prove the following theorem:

flip_id :: forall a b. FI . a . b == b . a
flip_id = Refl `tr2` flip `tr2` fcong id

We can define any alias we want. However, like theorems, aliases cannot be recursive.

Further research

This axiomatic system is probably as strong as the first-order Peano arithmetic. It cannot reason about uncomputable functions, and since the set of all computable functions is countable, it cannot represent real numbers or transfinite cardinals. It is weaker than Zermelo-Fraenkel set theory, and probably even weaker than higher-order logic.

Regarding the consistency, it seems to be consistent, unless some silly mistake has been made in the axiomatization.

There are combinators that we can prove almost nothing about them, such as S . I . I (S . I . I). However, we can construct inductive datatypes using the induction schema for natural numbers (to be precise, that's actually not an axiom schema, but just a single axiom, because it does not involve a meta-level predicate parameter). Once we construct datatypes, we can write theorems that prove certain statements as long as some combinators belong to a datatype. We can explicitly pass around proofs of datatype inhabitation. It would be more verbose than in typed higher-order logic (where types are implicit), but it would allow more freedom regarding combinator applications.

Implementation

Implementation in Haskell - It links to a specific commit to make the link permanent. Checkout the master branch for more recent updates if there are any.