July 29th, 2021

These are preliminary notes about Practal’s logic and its system of *practical types*. This is ongoing research, and I expect updates to this document over time. *Practal Light* is a research prototype implementing (part of) what is presented in this document.

I have outlined in the initial design document for Practal [1] how I expect *types* to work in Practal. The basic idea is that they should be similar to sets; but unlike sets, they should support data abstraction.

Types in Practal are designed to be *extensional*. That is, two types are the same if they have the same members. This is the same as in set theory. But unlike in standard set theory, the members of a type do not need to be sets or types themselves, and do not expose structure beyond what is required to make them proper citizens of their type.

(A ⊆ B) = (∀ x : A. x : B)

Equality between two types A and B is thus characterized by

(A = B) = (A ⊆ B ∧ B ⊆ A)

An often posed question is, what is wrong with *coercions* [2]? Why not just use *them* instead of subtyping? There is a simple argument *for* subtyping, and another simple argument *against* coercions:

- Firstly, subtyping is just a natural consequence of type extensionality, and it would be strange to have type extensionality, but not subtypes.
- Secondly, the basic idea of coercions is that in a function application f u, where f is a function from V to W, u an argument of type U, and U ≠ V, we can replace the illtyped term f u by the welltyped term f (c u), where c is a coercion from U to V. But in Practal, f u is not an illtyped term, but will have either type W in case of u : U ∩ V, or type Nil if ¬(u : V).

The system of *practical types* I propose for Practal is not a type system in the conventional sense. In fact, there are *no* illtyped terms in Practal, just illformed terms and wellformed terms. All wellformed terms have a type, although you might not be able to determine or prove what it is.

Practal’s logic is new territory for me, and *Practal Light* is an ITP prototype I am implementing in Swift to test ideas. I will use source code excerpts from Practal Light to introduce and explain concepts. The full source code of Practal Light is available at https://github.com/practal/practal-light under an MIT license.

An important choice is to decide what the terms of Practal’s logic look like. I have ﬁnally arrived at the following design I am very pleased with:

enum Term { case variable(Var, params: [Term]) case constant(Const, binders: [Var], params: [Term]) }

Here Var represents variable names, and Const constant names. A Term is either

- a
*variable*; if it is free, it may depend on parameters; - a
*constant*binding variables and being applied to parameters.

For example, a lambda term is represented as

.constant("abs", binders: ["x"], params: [.variable("T", params: []), .variable("P", params: ["x"])])

We use the more concise abstract syntax (abs x. T P[x]) instead, or rather the concrete syntax λ x : T. P[x].

Every term, type or formula is represented in Practal Light via this minimalistic Term data structure. I call this way of representing terms **ﬁrst-order abstract syntax**.

A term is **wellformed** if the following conditions are true:

- All constants appearing in the term conform to their introduced abstract syntax.
- Each free variable has a ﬁxed arity of parameters throughout the term.
- Only bound variables in scope are accessed.

A wellformedness check has been implemented in Practal Light and can be examined for more detailed information.

The following code in Practal Light introduces all primitive constants that all other constants will be deﬁned in terms of:

introduce("(eq. A B)", syntax: "A = B", priority: REL_PRIO) introduce("(abs x. T B[x])", syntax: "λ x : T. `B", priority: BINDER_PRIO) introduce("(app. A B)", syntax: "`A B", priority: APP_PRIO) introduce("(in. A T)", syntax: "A : T", priority: REL_PRIO) introduce("(all x. P[x])", syntax: "∀ x. `P", priority: BINDER_PRIO) introduce("(choose x. P[x])", syntax: "ε x. `P", priority: BINDER_PRIO) introduce("(imp. A B)", syntax: "A ⟶ `B", priority: LOGIC_PRIO + IMP_RPRIO) introduce("(false.)", syntax: "⊥") introduce("(Prop.)", syntax: "ℙ") introduce("(Fun. U V)", syntax: "U → `V", priority: TYPE_PRIO + FUN_RPRIO) introduce("(Pred x. T P[x])", syntax: "{ x : T | P }") introduce("(Type. i)", syntax: "Type i", priority: TYPE_PRIO + TYPE_RPRIO) introduce("(Union i. I T[i])", syntax: "⋃ i : I. `T", priority: TYPE_PRIO + UNION_RPRIO) introduce("(Nat.)", syntax: "ℕ") introduce("(Nat-zero.)", syntax: "0") introduce("(Nat-succ.)", syntax: "succ")

The constants are introduced by specifying their abstract and their concrete syntax. The concrete syntax can have optional priority and associativity annotations. From these, a pyramid grammar [3] is constructed for parsing both abstract and concrete syntax simultaneously. As an example for how this works, consider the case

theory.introduce("(app. A B)", syntax: "`A B", priority: APP_PRIO)

The priority is given as a ﬂoating point value APP_PRIO. This means that the expression A B is understood to be an expression of that priority. Without any further annotation the default assumption is that A and B are themselves expressions of the *next-higher* priority compared to APP_PRIO. But that would rule out an expression like A B C. Therefore, the actual syntax given is

`A B

where the tick in front of A signiﬁes that A has priority APP_PRIO as well. Therefore the expression A B C is parsed as (A B) C. Note that A (B C) is ruled out, because B C has priority APP_PRIO, but is required to have a priority *just higher* than APP_PRIO. So effectively the tick in front of A speciﬁes *left associativity*.

The following table summarizes the introduced primitive constants: $\begin{array}{c||c|c}
\text{concept} & \text{concrete syntax} & \text{abstract syntax} \\
\hline
{\includegraphics[height=0.5em]{32041C4F-3CBF-4E52-9EF5-B52C847F57CD}} & {\includegraphics[height=0.5em]{05DF480E-1973-4DE7-914A-8B70E56CF11C}} & {\includegraphics[height=0.5em]{CB19EC3E-989E-40AB-B7C8-1EE0F117FD22}} \\
{\includegraphics[height=0.5em]{21705554-047F-495A-80E0-F86ED9696635}} & {\includegraphics[height=0.5em]{68748805-8D4C-46F4-BBA9-4EFE9E0E37EA}} & {\includegraphics[height=0.5em]{DFE2C24E-1C19-4487-93A9-6338D63E01E6}} \\
{\includegraphics[height=0.5em]{7D2A5F3C-C058-4CDD-BF27-A5ECAD27F4BD}} & {\includegraphics[height=0.5em]{4865DFE6-454E-4FD0-9A11-127D3F2B3A79}} & {\includegraphics[height=0.5em]{807B8600-1B50-4684-8A44-BD83593B7C11}} \\
{\includegraphics[height=0.5em]{A8601889-FC1E-468F-A066-047B75153490}} & {\includegraphics[height=0.5em]{2BEDF05B-0D74-4FA2-8CD7-86DE967C3774}} & {\includegraphics[height=0.5em]{9A26DFBD-5426-4C89-9F69-698E6AA21075}} \\
{\includegraphics[height=0.5em]{79672DD9-D649-4400-B67F-8BE2A14BE42A}} & {\includegraphics[height=0.5em]{552ED394-C43C-45BE-8638-2A4D9FFC228E}} & {\includegraphics[height=0.5em]{6FF8B99A-CCAE-4F75-9B9D-BAA4964F0CE7}} \\
{\includegraphics[height=0.5em]{DBBB6966-92B3-434C-B640-63EF02B23591}} & {\includegraphics[height=0.5em]{236B4CBC-C897-40BF-9520-A6C35F64D505}} & {\includegraphics[height=0.5em]{D563EF4B-0D5B-454B-B2E6-7B2C3A6883B5}} \\
{\includegraphics[height=0.5em]{00D383D0-865E-48B7-BF44-25D7C28FF116}} & {\includegraphics[height=0.5em]{7BC178B6-9163-44C3-9810-6FE036AECA2A}} & {\includegraphics[height=0.5em]{F8572C14-05BB-4E1E-8921-D308EB9AADE6}} \\
\hline
{\includegraphics[height=0.5em]{C2F9DCA5-0BED-4C03-90E8-0426D8C1CDCD}} & {\includegraphics[height=0.5em]{0E31E269-9392-4CB0-A767-B4E0918BE68B}} & {\includegraphics[height=0.5em]{0415B1D4-A70D-4B02-A782-018633B50F01}} \\
{\includegraphics[height=0.5em]{0494D510-156B-4146-A729-997F55FA6C82}} & {\includegraphics[height=0.5em]{E1882D7A-55A3-4BC4-8DC7-597BA50D5716}} & {\includegraphics[height=0.5em]{E2EC19C3-715E-41A0-B685-52012219439F}} \\
{\includegraphics[height=0.5em]{455EEAD9-EC12-41B6-956F-3C8646A9F0F2}} & {\includegraphics[height=0.5em]{123FC04D-34D4-4239-B2BC-480199FDD613}} & {\includegraphics[height=0.5em]{BA3F0630-568B-4F74-B8FD-3DD1D43021EA}} \\
\hline
{\includegraphics[height=0.5em]{0A7D7DED-8069-4676-A4B6-4483A0358629}} & {\includegraphics[height=0.5em]{E37C5891-88DC-487C-9F03-97A101A1EC2B}} & {\includegraphics[height=0.5em]{365971AE-22E3-40E0-B1DC-CC42762E6297}} \\
{\includegraphics[height=0.5em]{F342D793-2813-4A95-91C5-6719D18DD55F}} & {\includegraphics[height=0.5em]{9ECAD747-5992-41B0-955F-6ACF3B2F85A5}} & {\includegraphics[height=0.5em]{726C7144-30AA-4B0C-A808-B5B50FC1E855}} \\
{\includegraphics[height=0.5em]{E2430E13-915E-42A0-9001-25DD91E61F5A}} & {\includegraphics[height=0.5em]{1346B3F6-6FE3-4897-B965-D2D17194551C}} & {\includegraphics[height=0.5em]{BAAF63EF-7A30-4FD4-9779-0CA7CE87708C}} \\
\hline
{\includegraphics[height=0.5em]{91551A0D-54FC-4EB0-85EF-56179B2255DD}} & {\includegraphics[height=0.5em]{60502242-2EFB-4069-ABE5-CCDB9BE13B2E}} & {\includegraphics[height=0.5em]{7B79ED15-CD5E-4FB3-B361-7BA379B7AFB2}} \\
{\includegraphics[height=0.5em]{596B3760-F4EF-4B35-8636-156A0F2822BC}} & {\includegraphics[height=0.5em]{FD50014A-0017-4458-A0E9-74FCF32472D1}} & {\includegraphics[height=0.5em]{BC22142F-B909-4668-B109-CA7CAC0DB968}} \\
{\includegraphics[height=0.5em]{133F1938-FCA9-4D82-B701-77263EB2D3CD}} & {\includegraphics[height=0.5em]{8EA4ECF6-B948-4DAF-BA4D-C8E272B11E86}} & {\includegraphics[height=0.5em]{8AD209B7-1D2C-4D42-996C-F9A70ED8C223}} \\
\end{array}$

Practal Light has no theorems or rules of inference implemented yet. There will be basic axioms like

⊢ a = a

and

⊢ (a = b) : ℙ

and primitive inference rules like modus ponens, $\alpha$-equivalence, $\beta$-reduction, and instantiation of free variables.

Note that practical types are completely governed by theorems, i.e. a typing judgement is a normal theorem. That means that initially, type checking will possibly be harder compared to other ITP systems, as there is no built-in automation for proving typing judgements. But it also means that practical types have unparalleled ﬂexibility. Furthermore, as the general support for automation in Practal gradually increases, this wave of automation will also lift type checking.

Practal Light follows the LCF approach [4]. After initial primitive constants and axioms have been introduced, all other theory development occurs by consistency-preserving deﬁnitions only.

One basic deﬁnition mechanism has already been implemented in Practal Light: Given two terms lhs and rhs, where lhs describes the abstract syntax of the new constant to be deﬁned, and rhs is the right hand side of the deﬁning equality, a new constant is deﬁned if certain side-conditions are met, such as the wellformedness of rhs, and that all free variables of rhs are among the free variables of lhs.

Using this deﬁnition mechanism, we can already deﬁne many important derived notions:

define("(not. P)", "P ⟶ ⊥", syntax: "¬`P", priority: LOGIC_PRIO + NOT_RPRIO) define("(true.)", "¬ ⊥", syntax: "⊤") define("(or. P Q)", "¬P ⟶ Q", syntax: "`P ∨ Q", priority: LOGIC_PRIO + OR_RPRIO) define("(and. P Q)", "¬(¬P ∨ ¬Q)", syntax: "`P ∧ Q", priority: LOGIC_PRIO + AND_RPRIO) define("(equiv. P Q)", "(P ⟶ Q) ∧ (Q ⟶ P)", syntax: "P ≡ Q", priority: REL_PRIO) define("(neq. P Q)", "¬(P = Q)", syntax: "P ≠ Q", priority: REL_PRIO) define("(ex x. P[x])", "¬(∀ x. ¬P[x])", syntax: "∃ x. `P", priority: BINDER_PRIO) define("(all-in x. T P[x])", "∀ x. x : T ⟶ P[x]", syntax: "∀ x : T. `P", priority: BINDER_PRIO) define("(ex-in x. T P[x])", "∃ x. x : T ∧ P[x]", syntax: "∃ x : T. `P", priority: BINDER_PRIO) CONTROL_PRIO)

The above deﬁnitions are summarized in the following table: $\begin{array}{c||c|c|c}
\text{concept} & \text{concrete syntax} & \text{lhs} & \text{rhs}\\
\hline
{\includegraphics[height=0.5em]{F4D1DA34-D211-4AED-BDEC-138F36CA1F2B}} & {\includegraphics[height=0.5em]{8F93A553-3A4F-47C2-9BB1-4D85FEC7A0D2}} & {\includegraphics[height=0.5em]{908289B3-3A04-4EE9-B8F9-450C42167B66}} & {\includegraphics[height=0.5em]{A0F78D86-7D58-4963-8399-825ECEBDC74F}} \\
{\includegraphics[height=0.5em]{058A0982-AA69-438C-A40A-8606E1CB38A0}} & {\includegraphics[height=0.5em]{656B2B73-777A-483E-8845-D307FE188858}} & {\includegraphics[height=0.5em]{F86F0942-D537-4DBD-8020-4FEEAB996FE3}} & {\includegraphics[height=0.5em]{991B7F3C-2E4D-4546-B7ED-6001924E7B37}} \\
{\includegraphics[height=0.5em]{6D66B78A-EFFF-4B63-89B6-C381A80ECAC6}} & {\includegraphics[height=0.5em]{A8007AA1-8682-427D-987C-FD960591F219}} & {\includegraphics[height=0.5em]{8207F7B7-0CD0-428C-BF9F-0C63E5060D93}} & {\includegraphics[height=0.5em]{E72DBFC8-F83D-4E7B-B61E-BFDCCF0DA393}} \\
{\includegraphics[height=0.5em]{BFA79927-2381-47A6-87BD-943EEDFF4716}} & {\includegraphics[height=0.5em]{B7ADEC66-33F3-4D2F-A85B-492C9C3A8C44}} & {\includegraphics[height=0.5em]{FE71BB34-0BCB-4450-8F9F-8D29DDA16FF8}} & {\includegraphics[height=0.5em]{84C47B10-0379-4E73-90BC-263182EBA4E9}} \\
{\includegraphics[height=0.5em]{5924EEB3-B26F-4E9E-9768-408E4E1BD6C2}} & {\includegraphics[height=0.5em]{2CED1911-22F2-43BC-AA56-801DC49001AC}} & {\includegraphics[height=0.5em]{2310C970-2E60-44F1-8E02-E01B7857F6AA}} & {\includegraphics[height=0.5em]{B3129A1B-1502-42A8-9810-6B398CE027D1}} \\
{\includegraphics[height=0.5em]{62FBCB54-A600-4C15-9BD1-E7212576CE53}} & {\includegraphics[height=0.5em]{71A39495-04C5-4FC6-87F4-8BFA3D21D231}} & {\includegraphics[height=0.5em]{46CFDF2A-EBC6-4EDC-B525-7F97ECFE1A29}} & {\includegraphics[height=0.5em]{3022CFFD-59CC-4883-AC32-889794AE45E1}} \\
{\includegraphics[height=0.5em]{CDE234EB-D2EC-4A54-A062-A3464C3B3BAC}} & {\includegraphics[height=0.5em]{BA12582D-402C-4A34-AC26-3FDC8056B4CE}} & {\includegraphics[height=0.5em]{98C36BD9-3E37-482C-8B07-8B5ACB230267}} & {\includegraphics[height=0.5em]{84741954-6019-4E1C-850D-C5B6673B8DA0}} \\
{\includegraphics[height=0.5em]{24682E05-E7D6-47CB-BC2E-3B1ACA11F9EC}} & {\includegraphics[height=0.5em]{7C0497F2-78BE-4922-ACCE-600B8A9D1C67}} & {\includegraphics[height=0.5em]{7FD49FDC-C5C8-4C3A-AE48-55F2C51B292C}} & {\includegraphics[height=0.5em]{86CA6A18-9A66-4ED9-9B48-CE3B8ECF636E}} \\
{\includegraphics[height=0.5em]{8A5C916A-4F06-48A6-9F8C-F1AC3B2FAA2F}} & {\includegraphics[height=0.5em]{4F2CCB2B-12E5-406C-B080-4453F63C4A60}} & {\includegraphics[height=0.5em]{6D138FDB-422E-4A8B-A118-CE8BC42CB754}} & {\includegraphics[height=0.5em]{8B3A2306-B131-4E94-AC4E-91A8450A87F9}} \\
\end{array}$

In the following we write deﬁnitions in an abbreviated notation, for example:

all-in: ⊢ ∀ x : T. P[x] ≝ ∀ x. x : T ⟶ P[x]

The following is a blueprint for the development of **practical types** in Practal Light. For each type, the following questions need to be answered:

- What are the elements of the type?
- When do we consider two elements of the type to be equal?
- Are elements of the type equal to elements of some other type?

Practal uses classical logic, and therefore the type ℙ of *propositions* consists of exactly two elements, ⊤, which denotes *truth*, and ⊥, which denotes *falsity*:

⊢ ∀ p : ℙ. p = ⊥ ∨ p = ⊤ ⊢ ⊤ ≠ ⊥

The *empty type* ∅ is the simplest possible type, as it has no members at all. It is characterized by

⊢ ∀ x : ∅. ⊥

We can actually *deﬁne* the empty type using predicate subtypes as

Empty: ⊢ ∅ ≝ { p : ℙ | ⊥ }

Given two types A and B, the type of *total functions* with domain A and codomain B is denoted by A → B. Therefore the following axiom holds:

⊢ f : A → B ⟶ (∀ a : A. f x : B)

A function is only equal to other functions. Furthermore for a function f : A → B and g : C → D to be equal, they need to be deﬁned on the same domain, i.e. A = C.

⊢ ∀ f : A → B. ∀ g : C → D. (f = g) = (A = C ∧ (∀ x : A. f x = g x))

It should therefore be possible to prove the following subtype relationship between function types for types A, B, C and D:

(A → B ⊆ C → D) = (A = C ∧ (A = ∅ ∨ B ⊆ D))

We can *deﬁne* in our logic the property of being a function, in code:

define("(is-Fun. f)", "∃ U. ∃ V. f : U → V", syntax: "f : Fun", priority: REL_PRIO)

In our abbreviated notation this reads

is-Fun: ⊢ f : Fun ≝ ∃ U. ∃ V. f : U → V

Note that Fun *is not a type*. It is just notation that allows us to pretend so in many situtations. We can extend notation for universal and existential quantiﬁcation accordingly:

all-fun: ⊢ ∀ f : Fun. P[f] ≝ ∀ f. f : Fun ⟶ P[f] ex-fun: ⊢ ∃ f : Fun. P[f] ≝ ∃ f. f : Fun ∧ P[f]

Note that for any type A ≠ ∅ we have

(A → ∅) = ∅

On the other hand, for any type B, we have

(∅ → B) = (∅ → ∅)

We therefore deﬁne

Nil: ⊢ Nil ≝ ∅ → ∅

The type Nil has exactly one element, namely the unique function nil : Nil with empty domain:

nil: ⊢ nil ≝ λ x : ∅. ⊥

We use nil to deal with undeﬁnedness. In particular, we postulate the following axiom:

⊢ f : A → B ⟶ ¬ (x : A) ⟶ f x = nil

In other words, if we apply a function to an argument outside of its domain, the result is nil. Because nil itself is a function with empty domain, we also have

⊢ nil x = nil

What does A B mean if A is not a function? The following axiom handles this case:

⊢ ¬(A : Fun) ⟶ A B = nil

Furthermore, we introduce the following notions that simplify working with undeﬁnedness:

defined: ⊢ x↓ ≝ x ≠ nil undefined: ⊢ x↑ ≝ x = nil defined-eq: ⊢ x =↓ y ≝ (x↓ ∨ y↓) ∧ x = y undefined-eq: ⊢ x =↑ y ≝ x↑ ∨ y↑ ∨ x = y

The Hilbert choice operator obeys the following axioms:

⊢ (∃ x. P[x]) ⟶ P[ε x. P[x]] ⊢ ¬(∃ x. P[x]) ⟶ (ε x. P[x]) = nil

The expression

{ a : A | P[a] }

denotes the subtype of A consisting of exactly those elements a : A for which P[a] is true.

Consequently, we postulate the following axiom:

⊢ (a : { a : A | P[a] }) = (a : A ∧ P[a])

Of course, for any type A this implies

{ a : A | P[a] } ⊆ A

We also postulate the existence of a type ℕ which represents the natural numbers. We assume the *Peano axioms*, adapted to our setting:

⊢ 0 : ℕ ⊢ succ : ℕ → ℕ ⊢ succ n ≠ 0 ⊢ succ(m) =↓ succ(n) ⟶ m = n ⊢ 0 : N ⟶ (∀ n : N. succ n : N) ⟶ ℕ ⊆ N

Given a type A, what type does A have? It would be convenient if there could be a single type Type of types, but using Russell’s paradox it is easy to see that this leads to inconsistency. Because let the type R be deﬁned via

R = { T : Type | ¬(T : T) }

Assuming R : R, it follows that ¬(R : R). On the other hand, assuming ¬(R : R) implies R : R. Thus (R : R) = ¬(R : R), an inconsistency.

We take the same way out of this dilemma as Lean does: There is not just a single type Type of types, but an inﬁnite family Type i of types of types such that

(Type 0 : Type 1) ∧ (Type 1 : Type 2) ∧ (Type 2 : Type 3) ∧ ...

We furthermore require a nesting of types such that

(Type 0 ⊆ Type 1) ∧ (Type 1 ⊆ Type 2) ∧ (Type 2 ⊆ Type 3) ∧ ...

We use 𝕋 as an abbreviation for Type 0:

Type-0: ⊢ 𝕋 ≝ Type 0

Membership to Type i is governed by the following axioms:

⊢ ℙ : 𝕋 ⊢ ℕ : 𝕋 ⊢ A : Type i ⟶ B : Type i ⟶ A → B : Type i ⊢ A : Type i ⟶ P : A → ℙ ⟶ { a : A | P a } : Type i ⊢ i : ℕ ⟶ Type i : Type (succ i) ⊢ i : ℕ ⟶ Type i ⊆ Type (succ i)

Let’s try to apply Russell’s paradox again, and form for example

S = { T : 𝕋 | ¬(T : T) }

From S : S we can still derive ¬(S : S). But the other direction doesn’t work anymore, because the assumption ¬ (S : S) is not enough to prove S : S. We also need to show S : 𝕋, but we can only prove S : Type 1. So there is no paradox here anymore, just a proof of ¬ (S : S).

Although there is no universal type of types, we can nevertheless introduce notation that emulates it in certain situations, just like we did for Fun:

is-Type: ⊢ T : Type ≝ ∃ i. T : Type i all-type: ⊢ ∀ T : Type. P[T] ≝ ∀ T. T : Type ⟶ P[T] ex-type: ⊢ ∃ T : Type. P[T] ≝ ∃ T. T : Type ∧ P[T]

sub-type: ⊢ U ⊆ V ≝ U : Type ∧ V : Type ∧ (∀ u : U. u : V)

Given x : T we could deﬁne the singleton type { x } as

{ x } = { y : T | y = x }

But what if we don’t know which type x has? Could it be that x has *no type*? That doesn’t seem to make sense, so we introduce the following axiom:

⊢ ¬ (x : Type) ⟶ (∃ T : 𝕋. x : T)

This makes sure that x : { x } actually holds, where we deﬁne { x } by

Singleton: ⊢ { x } ≝ { y : (ε T. x : T) | x = y }

We want the expression

⋃ a : A. T[a]

to denote the type formed by the union of T[a] over all a : A.

But this is a powerful operation, and we need to be careful for it not to lead to inconsistency. For example, if we allow

⋃ i : ℕ. Type i

then we have effectively constructed our type of all types, which we know leads to inconsistency.

We try to tame the union operator by deﬁning it only when all T[a] are members of Type i for some ﬁxed i. This leads to the following axioms:

⊢ (∀ a : A. T[a] : Type i) ⟶ (x : ⋃ a : A. T[a]) = (∃ a : A. x : T[a]) ⊢ (∀ a : A. T[a] : Type i) ⟶ (⋃ a : A. T[a]) : Type i ⊢ ¬(∃ i : ℕ. ∀ a : A. T[a] : Type i) ⟶ (⋃ a : A. T[a]) = nil

This still allows us to construct huge types like

⋃ T : 𝕋. T

We deﬁne the intersection of types by

Intersection: ⊢ ⋂ a : A. T[a] ≝ { x : ⋃ a : A. T[a] | ∀ a : A. x : T[a] }

We deﬁne A ∪ B and A ∩ B via

Binary-Union: ⊢ A ∪ B ≝ ⋃ p : ℙ. (if p then A else B) Binary-Intersection: ⊢ A ∩ B ≝ ⋂ p : ℙ. (if p then A else B)

The if-then-else construct is deﬁned by

if-then-else: ⊢ if p then A else B ≝ ε x. (p ⟶ x = A) ∧ (¬ p ⟶ x = B)

The lambda expression

λ x : T. B[x]

is only deﬁned if its type

T → ⋃ x : T. {B[x]}

is deﬁned:

⊢ T → (⋃ x : T. {B[x]}) ↓ ⟶ (λ x : T. B[x]) : T → (⋃ x : T. {B[x]}) ⊢ T → (⋃ x : T. {B[x]}) ↑ ⟶ (λ x : T. B[x]) = nil

Application of a lambda expression to an argument is deﬁned accordingly:

⊢ T → (⋃ x : T. {B[x]}) ↓ ⟶ x : T ⟶ (λ x : T. B[x]) x = B[x]

There is no mechanism for deﬁning new types implemented yet in Practal Light. Let us assume it would allow a type deﬁnition of pairs somewhat like this:

typedef Pair: A ⨯ B ⇄ { f : ℙ → A ∪ B | f ⊥ : A ∧ f ⊤ : B }

A member e of A ⨯ B is written (a, b) if it is represented by an f such that f ⊥ = a and f ⊤ = b. In this case we also deﬁne fst e = a, and snd e = b.

Why do we need a new type deﬁnition mechanism? Could we not just deﬁne it as:

Pair: ⊢ A ⨯ B ≝ { f : ℙ → A ∪ B | f ⊥ : A ∧ f ⊤ : B }

That would certainly be possible, but then A ⨯ B would consist of functions. We want pairs not to be equal to anything than other pairs, and thus the new mechanism is needed.

The *dependent function type* [a : A] → B[a] is deﬁned as

D-Fun: ⊢ [a : A] → B[a] ≝ { f : A → (⋃ a : A. B[a]) | ∀ a : A. f a : B[a] }

D-Pair: ⊢ [a : A] ⨯ B[a] ≝ { p : A ⨯ (⋃ a : A. B[a]) | snd p : B[fst p] }

There have been a few assumptions left unsaid and implicit, and it is now time to spell them out explicitly.

Propositions, natural numbers, functions, pairs and types are disjoint:

⊢ ℙ ∩ ℕ = ∅ ⊢ ℙ ∩ (A → B) =↑ ∅ ⊢ ℙ ∩ (A ⨯ B) =↑ ∅ ⊢ ℙ ∩ Type i =↑ ∅ ⊢ ℕ ∩ (A → B) =↑ ∅ ⊢ ℕ ∩ (A ⨯ B) =↑ ∅ ⊢ ℕ ∩ Type i =↑ ∅ ⊢ (A → B) ∩ (A ⨯ B) =↑ ∅ ⊢ (A → B) ∩ Type i =↑ ∅ ⊢ (A ⨯ B) ∩ Type i =↑ ∅

The =↑ operator is used instead of just = because operands might be undeﬁned:

⊢ ¬ (A : Type) ∨ ¬ (B : Type) ⟶ (A → B) = nil ⊢ ¬ (A : Type) ∨ ¬ (B : Type) ⟶ (A ⨯ B) = nil ⊢ ¬ (i : ℕ) ⟶ Type i = nil

Similarly, we need to be clear for all remaining primitive constants when they are deﬁned or otherwise undeﬁned. This will then ripple through derived notions, often without any further need to specify deﬁnedness / undeﬁnedness.

⊢ ¬ (T : Type) ⟶ (x : T) = ⊥ ⊢ ¬ (T : Type) ⟶ { x : T | P[x] } = nil

Logical operators are deﬁned on ℙ ∪ Nil, and the nil value is taken to mean false:

¬ (P : ℙ ∪ Nil) ⊢ (¬ P)↑ ¬ (P : ℙ ∪ Nil) ⊢ (P ⟶ Q)↑ ¬ (Q : ℙ ∪ Nil) ⊢ (P ⟶ Q)↑ ⊢ ¬ nil ⊢ (¬ ⊤) = ⊥ P : ℙ ∪ Nil ⊢ nil ⟶ A P : ℙ ∪ Nil ⊢ ⊥ ⟶ A ⊢ ⊤ ⟶ ⊤ ⊢ (⊤ ⟶ ⊥) = ⊥ ⊢ (⊤ ⟶ nil) = ⊥

Universal quantiﬁcation ∀ x. P[x] is deﬁned as follows:

- If there is an a such that ¬ (P[a] : ℙ ∪ Nil), then (∀ x. P[x]) = nil.
- If P[x] = ⊤ for all x, then (∀ x. P[x]) = ⊤.
- If P[x] : ℙ ∪ Nil for all x, but there is an a with ¬ P[a], then (∀ x. P[x]) = ⊥.

What just happened here? I am actually not quite sure. I really see only two possibilities:

- This is all some inconsistent bullshit.
- Practical Types can serve as the new and improved foundations of interactive theorem proving, and mathematics in general.

Maybe you have an opinion which one of the two it is, or want to offer a third option? If you have any comments, questions, and/or want to share your ideas for Practal, please visit Practal’s discussion forum!

[1](2021). Practal — Practical Logic: A Bicycle for Your Mathematical Mind, https://doi.org/10.47757/practal.1.