# Π₁

Paradigm(s) | Declarative |
---|---|

Designed by | User:Hakerh400 |

Appeared in | 2022 |

Computational class | Category:Turing complete |

Major implementations | Implementation in Haskell |

File extension(s) | `.txt` |

**Π₁** is a dependently typed set-theoretic declarative programming language with inductive constructions.

## Overview

In this language, everything is a **class**. A class is either a **proper class**, or a **set**.

A set is a collection of (countably or uncountably many) other sets. A set can be empty. Every set has an ordinal rank. Two sets are equal iff they contain the same elements.

## Constructing sets

There are several ways to make a set.

### Literal

The simplest way is to explicitly provide its elements. For example, is the set that contains exactly , and (assuming they are sets that we have already defined). The empty set is represented as .

### Union

If is a set, then is the union of all elements of .

### Powerset

If is a set, then is the set of all subsets of .

### Choice function

To pick an element from a nonempty set, we prepend question mark before it.

If is a nonempty set, then `?A`

is an element of . If is the empty set, the result is implementation-dependent. The choice function always returns the same result for the same set.

### λ-functions

An **ordered pair** of two sets and is defined as . Set is called **the first element**, and is called **the second element**.

Let be a set and be a function (in an informal sense) that maps each element of to some set. In other words, .

A **function** that maps each to an element of set is a set of ordered pairs such that for each pair :

Additionally, each appears in exactly one pair as the first element.

Example of a function:

```
λ (x ∈ A),
```

Expression constructs a set and may contain as a free variable.

Each λ-function is a set.

### Π-functions

Example:

```
Π (x ∈ A),
```

Expressions constructs a set and may contain as a free variable. A Π-function is the minimal set satisfying

(λ (x ∈ A), ) ∈ (Π (x ∈ A), )

Basically, Π-function is the of a lambda function.

Each Π-function is a set.

### Non-dependent function type

If and are sets, then `A → B`

is a syntactic sugar for . In general, if does not appear free in , then

### Application

Let be a set and for some .

Expression represents function application (parentheses around are optional). It satisfies the following condition: .

### Comprehension

Let be a set and for some .

is the set of exactly the elements for which is nonempty.

### Map

Let be a set and for some .

is the set that contains if and only if .

### Inductive constructions

We introduce yet another syntax for making sets:

Note that every lambda expression must have the membership () defined for each parameter. Here, we don't have the membership for , so actually represents any element of the set being defined. Expression constructs a set and may appear free in . The result is the smallest set (with the smallest number of elements) that contains all the constant terms , plus all elements that can be inductively constructed using the lambda expression provided.

## Definitions

To define a set, write an identifier followed by `:=`

and then the definition. For example:

A := {} B := {A} C := {A, B}

We defined three sets. Set is empty. Set is a singleton set that contains . Set is equal to .

To define a proper class, we add set parameters to the left. For example:

my_class S := {S}

This can be understood as a meta function that takes a set and makes a singleton set that contains . Note that `my_class`

is not a set, so in a set expression it must always be supplied with enough arguments.

## Basic examples

First, we can make the empty set:

emp := {}

Then we can make propositions `false`

and `true`

false := emp true := {false}

Proposition `false`

is the empty set. Proposition `true`

is the singleton set that contains the empty set. We can make the set of all propositions:

prop := {false, true}

It has exactly two elements. Now we want to define a function that can tell us whether the given set is empty. If the set is empty, it should return `true`

, and otherwise it should return `false`

. But, if we want it to work for any set, then that function itself cannot be a set. It must be a proper class:

is_empty S := λ (a ∈ S), a → false

So, what did we do here? We defined a proper class `is_empty`

, which is a meta function parametrized with some set . Let be some set. Then `is_empty S`

is a function that takes an element and returns `(a → false)`

(if the supplied argument is not a member of , the result if implementation-dependent). Now, what does `(a → false)`

mean? It is a syntactic sugar for `(Π (x ∈ a), false)`

, which represents the set of all functions from elements of `a`

to elements of `false`

. Since `false`

is the empty set, if `a`

is nonempty, then there is no such function, so `(a → false)`

is the empty set. However, if `a`

is empty, then there exists a single function (function from the elements of the empty set to the elements of the empty set), which is represented as the empty set itself, so the result of `(a → false)`

is the set that contains the empty set (which is `true`

by definition).

Note that, despite the fact that `is_empty`

is a proper class, `is_empty S`

is a set, so `is_empty X (is_empty S)`

is a valid expression. But in order to guarantee a valid result, we must provide as `X`

a set that contains `is_empty S`

, which can be `{is_empty S}`

. So, `is_empty {is_empty S} (is_empty S)`

is a valid set and it is equal to `false`

.

Another way to write `is_empty`

is_empty S (a ∈ S) := a → false

It is equivalent to the previous definition. Whenever the right-hand-side starts with a lambda expression, we can move the argument to the left-hand-side and remove lambda. Note that the definition does not change. `is_empty S`

is still a set (function) for any set . However, if we removed `∈ S`

, then it would become a two-parameter proper class `is_empty S a := a → false`

(in that case, `is_empty S`

would still be a proper class).

Next, we can define logical negation:

not := is_empty prop

It is basically `is_empty`

specialized to work on propositions. Now, we define `nonempty`

, which returns `true`

iff the given set is nonempty:

nonempty S (a ∈ S) := not (is_empty S a)

Note that `nonempty`

can be used to convert any set to a proposition. The next thing we want to define are logical operators. Let's start with implication. For any two propositions `a`

and `b`

, implication `imp a b`

is true iff `a`

is false, or `b`

is true. But how to define it?

There are multiple ways, but we define it like this:

imp (a b ∈ prop) := nonempty (⋃ {prop {true → true}}) (a → b)

Explanation: we defined set `imp`

, which is a function that takes two propositions `a`

and `b`

and returns the result of `a`

implies `b`

. Expression `(a → b)`

is a syntactic sugar for `(Π (x ∈ a), b)`

. It is the set of all function from the elements of `a`

to the elements of `b`

. If `a`

is false, then for any `b`

there exists a unique function from the elements of `a`

to the elements of `b`

, so the set of all such functions is the set that contains only the empty set, which is definitionally equal to `true`

. If `a`

is true and `b`

is false, the set of all such functions is empty (the result is equal to `false`

).

However, if both `a`

and `b`

are true, there exists a single function from the elements of `true`

to the elements of `true`

(the only element of `true`

is `false`

), but the problem is that such function (which is a set) is not a proposition. We solve that problem by calling `nonempty`

, which converts the given set to a proposition. But, since `(true → true)`

itself is not a proposition, we must parametrize `nonempty`

with propositions plus that additional set. That's why we have `nonempty (⋃ {prop {true → true}})`

. If we just had `nonempty prop`

, then `imp true true`

would be underspecified (because `(true → true) ∉ prop`

).

Another way to define it:

imp (a b ∈ prop) := nonempty {a → b} (a → b)

It is equivalent to the previous definition. Since functions are sets, functional equivalence is extensional.

Next, let's define disjunction and conjunction:

or (a b ∈ prop) := imp (not a) b and (a b ∈ prop) := not (or (not a) (not b))

Iff and xor:

iff (a b ∈ prop) := and (imp a b) (imp b a) xor (a b ∈ prop) := not (iff a b)

We can also define the identity function:

id S (a ∈ S) := a

### Inspecting sets

Before we proceed to more advanced examples, let's take a look at how the sets (functions) from the *Basic examples* section look like from inside. Since all those sets are finite, we can inspect them using the `#print`

command:

#print emp -- {} #print false -- {} #print true -- {{}} #print prop -- {{}, {{}}} #print is_empty prop -- {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}} #print not -- {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}} #print nonempty prop -- {{{}, {{}}}, {{{}}, {{{}}}}} #print imp -- {{{}, {{}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}} #print or -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}} #print and -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}} #print iff -- {{{}, {{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}} #print xor -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}} #print id prop -- {{{}, {{}}}, {{{}}, {{{}}}}}

We parametrized each proper class with `prop`

for simplicity (we cannot print proper classes).

We can also print more complex constructions like

#print nonempty (id and) -- {{{{{}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}}}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}}}}, {{{{}}, {{{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}}}, {{{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}}}}

which may be hard to comprehend. Note that it is not what it might look like. Set `nonempty (id and)`

is not equal to the result of calling `nonempty`

with the result of calling `id`

with argument `and`

. It is actually a function, which is the result of parametrizing proper class `nonempty`

with the set `(id and)`

, while `(id and)`

is the result of parametrizing proper class `id`

with the set `and`

(`and`

is a set, not a proper class). Note the difference:

#print nonempty {id {and} and} (id {and} and) -- {{}}

For convenience, we introduce `f! x`

as a syntactic sugar for `f {x} x`

. The above expression can be written as `nonempty! (id! and)`

## Quantifiers

After defining propositional logic, we can now define the universal and the existential quantifier:

forall S (P ∈ S → prop) := nonempty! (Π (x ∈ S), P x) exists S (P ∈ S → prop) := not (forall S (λ (x ∈ S), not (P x)))

Here is how they look:

#print forall prop -- {{{{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}} #print exists prop -- {{{{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}

The universal quantifier on set and unary predicate is true iff there exists a function that maps each element to an element of proposition . Such function exists iff none of the propositions is false. In other words, the quantifier checks whether is true for each . That's why we have `nonempty`

- we check whether there exists at least one such mapping.

The existential quantifier is defined using de Morgan laws. We can now define `forall'`

in terms of `exists`

forall' S (P ∈ S → prop) := not (exists S (λ (x ∈ S), not (P x)))

And, of course, we can print it:

#print forall' prop -- {{{{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{}}}, {{{}}, {{{}}}}}}, {{{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}

It is exactly the same as `forall`

. It doesn't matter how we define a function. It only matters what the function does. Consider also this example:

my_func (a ∈ prop) := forall prop (λ (b ∈ prop), imp a b)

What computation does this function perform? Clearly, it is a unary function from `prop`

to `prop`

. But what does it actually do? We can print it:

#print my_func -- {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}

Now, we observe that this is the same output as we get for `not`

, so `my_func`

is equal to `not`

. It actually makes perfect sense: we defined `my_func a`

as a proposition which is true iff `a`

implies any proposition `b`

, which is true iff `a`

is false, so `my_func`

inverts the proposition.

## Equality

We define equality using surjection from an unordered pair to `prop`

surj_prop S := exists (S → prop) λ (P ∈ S → prop), and (exists S λ (x ∈ S), P x) (exists S λ (x ∈ S), not (P x)) eq S (x y ∈ S) := not (surj_prop {a, b})

Explanation: Given some set and two elements , we put them in an unordered pair and then check whether there exists a surjection from it to `prop`

. If there exists a surjection, it means that and are not the same. The existence of a surjection implies that the cardinality of the unordered pair is at least , so if and are equal, the pair reduces to only one element.

We can print the equality on propositions:

#print eq prop -- {{{}, {{}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}

As we can see, it is identical to `iff`

. We can also define the not equals operator:

neq S (x y ∈ S) := not (eq S x y) #print neq prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{}, {{}}}}}}}}

## Set operations

### Union

Union of two sets:

union S (x y ∈ S) := ⋃ {x, y}

Union on props:

#print union prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}, {{}}}}, {{{}}, {{{}}}}}}}}

It is the same as `or`

, so we could define `or`

as:

or (x y ∈ prop) := union prop x y

### Remove an element

Remove element from set :

remove S (x y ∈ S) := {z ∈ y | neq {x, z} x z}

It would be interesting to see what `remove`

does when specialized to propositions:

#print remove prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}

We can clearly see that it is equivalent to `and`

, but why? We can manually check each possible combination:

`remove prop false false`

- Since`false`

is empty, removing anything from it remains`false`

`remove prop true false`

- Ditto`remove prop false true`

- Since`true`

contains`false`

as its only element, removing`false`

from`true`

makes`true`

become`false`

`remove prop true true`

-`true`

does not contain`true`

, so it remains unchanged

So, we can confirm that this function is equivalent to `and`

when specialized on propositions. But, of course, it can work on any set `S`

.

### Set membership

Return `true`

iff :

mem S (x y ∈ S) := neq {remove S x y, y} (remove S x y) y

Set is a member of set iff with removed is not equal to . If we specialize it on propositions, we get the following result:

#print mem prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}}

It is none of the function we have defined on propositions. So what it actually is? It is a function that returns `true`

iff the first argument is `false`

and the second argument is `true`

. That is the case because `(false ∈ true)`

is true, while it is false for all other combination of propositions.

### Intersection

Intersection of two sets:

inter S (x y ∈ S) := {z ∈ x | mem {z, y} z y}

When specialized to props, it is equal to `and`

, as expected.

#print inter prop -- {{{}, {{}, {{{}, {{}}}, {{{}}, {{}, {{}}}}}}}, {{{}}, {{{}}, {{{}, {{}}}, {{{}}, {{{}}}}}}}}

## Natural numbers

We can construct the set of the natural numbers, represented as the von Neumann ordinal :

0 := emp nat := {0, λ x, ⋃ {x, {x}}}

It represents the least fixed point. It contains (which is defined to be the empty set) and whenever it contains set , it also contains .

We cannot print infinite sets:

#print nat -- Segmentation fault (core dumped)

## Arithmetic operations

### Successor

succ (x ∈ nat) := ⋃ {x, {x}}

## Implementation

Implementation in Haskell - It is not an interpreter, but just a small utility for evaluating set expressions.