© 2021 Steven Obua

Practal — Practical Logic

A Bicycle for Your Mathematical Mind
by Steven Obua
Cite as: https://doi.org/10.47757/practal.1
July 17th, 2021
Abstract
This is a first sketch of the design of Practal, an interactive theorem proving system for practical logic.

Introduction

The foundation of many popular interactive theorem proving (ITP) systems [1] (e.g. Isabelle, HOL Light, Coq, Lean, PVS) is a logic based on types. These types include at least a type of propositions, and a type α → β of functions, where α and β are themselves arbitrary types.
I agree with the importance of types for ITP, especially for the formalization of mathematics. Ganesalingam [2] discusses in detail the role of type in mathematics. Nevertheless it seems to me that popular ITP systems do not capture the notion of type in quite the right way to accommodate common mathematical use. Isabelle/HOL and HOL Light for example are based on simply-typed higher-order logic (HOL), which is often sufficient for purposes of program verification, and astonishingly versatile [3]. But the simple types of HOL do not allow for dependent typing; the type of real square matrices with nn rows and columns cannot be expressed in HOL as a type in a straightforward way (although Harrison did it anyway [4]). On the other hand, dependent types [5] as implemented in Coq or Lean bestow a lot of power onto types via the proposition as types [6] paradigm (see also the Xena blog for a discussion), but do not even allow for the common mathematical practice of subtyping (neither does HOL). Instead, coercions are used to emulate some of the advantages of subtyping.
Impressive results have been obtained with current ITP technology, a recent one being the Liquid Tensor Experiment, a formalization in Lean based on ideas of Fields medallist Peter Scholze.
Still, in my opinion, ITP technology has not yet progressed as far as one could reasonably hope for. Among other things, there are two things I would like to do with an ITP system:
Both of these things are already possible with current ITP systems. But there is a caveat: It takes too much time and effort to do so. I want the ITP system to be a true bicycle for my mind that sharpens and accelerates my thinking, not a heavy boulder that I need to roll up a hill, consuming all of my energy. This also implies that the results of the formalization, including the proofs it contains, are in close correspondence with how I actually think about the notion at hand. I want a system for practical logic. I want Practal.
So how to get there? In the end, an ITP system is just software. So all the usual advice for making software applies. Probably the most important such advice is to gather requirements and feedback from actual and prospective users. As a start, I will fill this user role myself. But you are invited to become a user of Practal as well!
My design methodology will be to just do with Practal what I would like to do with an ITP system. The difficulty is of course that Practal does not exist yet, but I will just pretend that it does. Concretely, I will write down formalizations that I wish Practal would understand. Of course I will also have in mind what I believe Practal will be able to do, but a major driver will be what I want it to do.
In particular, I will not start from a particular logic and type system, and then build everything around it. Instead, I will let use cases shape both. This might lead to intermediate inconsistencies, which can hopefully be fixed along the way. Note that this approach is the opposite to how ITP systems are usually designed: First comes the logic / type system as a given, and then users are invited to find ingenious solutions to their formalization needs!
In the rest of this paper I will examine first use cases, and outline initial design decisions for Practal.

Use Case: Category Theory

In my opinion, the ability to apply both dependent typing and subtyping together is essential to a natural formalization of mathematics. Let’s consider the following hypothetical definition of categories in Practal:
structure Category =
  type Object 
  type Arrow  
  let dom : Arrow → Object
  let cod : Arrow → Object
  def HomSet(A : Object, B : Object) = 
    { f : Arrow | dom f = A ∧ cod f = B }
  let id : (x : Object) → HomSet(x, x)
  let then : (f : Arrow) → (g : Arrow | dom g = cod f) → 
             { h : Arrow | dom h = dom f ∧ cod h = cod g } 
  axiom identity : ∀ x : Arrow. (x then id (cod x)) = (id (dom x) then x) = x
  axiom associativity : ∀ e f g : Arrow. ((e then f) then g) = (e then (f then g)) 
end  
Just for this simple example we are already heavily using dependent types in the form of dependent ordered pairs to form the structure itself, and dependent function types for elements of the structure like then. These are combined with predicate subtypes [8] as
{ f : Arrow | dom f = A ∧ cod f = B }
for the definition of HomSet(A, B). It is a term of type Arrow → ℙ and can itself be viewed as a type, in particular a subtype of Arrow.
The notation (g : Arrow | dom g = cod f) in the declaration of then is short for
(g : { g : Arrow | dom g = cod f })
Note that the axiom for associativity does not include the precondition
cod e = dom f ∧ cod f = dom g
This is because if this condition is not met, then both (e then f) then g = nil holds as well as e then (f then g) = nil, which makes (e then f) then g = e then (f then g) true anyway.
Note that equality is a special operator. It takes two arguments, and returns whether they are equal or not. Its type would be = : Any → Any → ℙ, but because there is no Any type in Practal, equality does not have a type.

Nil Type For Expressing Undefinedness

In the above use case, why does (e then f) then g = nil hold when the precondition is not met?
It is because for any function f : A → B and an argument x such that ¬(x : A), i.e. not x : A, we define f x to be equal to nil, where nil is the only value of type Nil. We also define that nil applied to any argument x yields nil, that is nil x = nil.
So assume cod e ≠ dom f. This implies e then f = nil, because ¬(f : { g : Arrow | dom g = dom e}). Thus ((e then f) then g) = (nil then g). Now, we would certainly think that ¬(nil : Arrow), and therefore furthermore (nil then g) = nil. We can arrange for this indeed being the case by letting the declaration type Arrow being an abbreviation for
let Arrow : Type
axiom ¬(nil : Arrow)
Similarly, assume now cod f ≠ dom g. If e then f is defined, then cod (e then f) = cod f and therefore (e then f) then g = nil.
In our approach, nil is just a normal value; there is nothing special about it except for a few conventions that make it easy for nil to represent undefinedness or optionality. We will say more about this in a later section .

Function Subtyping

Given that Practal supports predicate subtyping, it is natural to ask which other subtyping relationships exist. In particular, given two function types A → B and C → D, when do we consider A → B to be a subtype of C → D, in symbols A → B ≤ C → D?
A natural convention, for example used by Aspinall and Compagnoni [9], would be to treat A → B ≤ C → D as being equivalent to
C ≤ A ∧ B ≤ D
This is problematic. Consider two functions floor : ℝ → ℤ and ceiling : ℝ → ℤ which round down and round up, respectively, a real number to an integer. Clearly floor ≠ ceiling. But if we allowed above subtyping convention, then floor and ceiling would both also have type ℤ → ℤ. But floor : ℤ → ℤ is just the identity, and ceiling : ℤ → ℤ is just the identity as well, so we would now have to conclude floor = ceiling!
The problem here is that in a logic we are often interested in whether two functions f and g are equal, i.e. whether f = g holds. In a programming language, this is usually not something we are interested in, as f = g is generally not computable anyway, and therefore of no interest. But in our logic, two functions f : A → B and g : A → B are equal iff
∀ x : A. f x = g x 
holds. Therefore, in order to talk consistently about function equality, we need to be able to uniquely determine the domain A of any function f. We therefore treat A → B ≤ C → D as being equivalent to
A = C ∧ B ≤ D
instead. While somewhat unconventional, it is in line with how the PVS system treats function subtyping [8].
Note that this is also in line with our notion of undefinedness for function application. If a function f : A → B could also have type f : C → B with A ≠ C, then there would be no consistent answer to the question if f x is defined or not, because we could have x : A but ¬(x : C) (or the other way around).

Union, Intersection and Difference Types

Given that we allow subtypes, it makes sense to also allow both union types A ∪ B and intersection types A ∩ B. Naturally, we have
A ≤ A ∪ B ∧ B ≤ A ∪ B
for unions, and
A ∩ B ≤ A ∧ A ∩ B ≤ B  
for intersections. An intersection can be empty, of course, and there is a type Null to accommodate this fact, i.e.
¬ (∃x : Null. true)
Unions and intersections can be characterized as follows:
∀ A B : Type. ∀ a : A. (a : B) = (a : A ∩ B)
∀ A B : Type. ∀ b : B. (b : A) = (b : A ∩ B)
∀ A B : Type. ∀ a : A. a : A ∪ B
∀ A B : Type. ∀ b : B. b : A ∪ B
Similarly, it is also possible to form the difference A \ B of two types.

Type Extensionality

An obvious question is, when are two types equal? The logical answer seems to be to treat types just like you would treat sets: They are equal if they have the same members:
∀ A B : Type. (A = B) = ((∀ a : A. a : B) ∧ (∀ b : B. b : A))

Partial Functions

Partial functions can be modelled as total functions which can also return nil:
typealias A ↪ B = A → (B ∪ Nil)
Note that we have
A → B ≤ A ↪ B
because function subtyping is covariant in the codomain.

Traditional Approach to Undefinedness

In Farmer’s traditional approach to undefinedness [10], terms can be undefined, but propositions are always defined by considering atomic propositions containing undefined terms to be false.
Farmer’s approach avoids three-valued truth values as in strong Kleene logic [11]. This is certainly a good thing as our goal is to emulate mathematical practice. Therefore in Practal, values in are also just true or false. But when considered in a truth context, we treat nil the same way as false. That makes sense, because just as we cannot prove a theorem false we neither can prove a theorem nil. This justification might sound silly; after all we also cannot prove a theorem 3, yet we do not consider 3 to mean false. But it is the pragmatic answer to the fact that nil can show up in a truth context, while 3 will not. For example, consider the formula
1/0 < 2
Is this a theorem? No, of course it is not. But then, because of (1/0 < 2) = nil, nil is not true, i.e. nil is false.
Therefore we utilise Practal’s support for subtyping and simply define our logical connectives on ℙ ∪ Nil instead of just on : \begin{array}{c|c} {\includegraphics[height=0.5em]{7B7C3EB6-AC40-4275-BE01-497A995FDCDE}} & {\includegraphics[height=0.5em]{E89F7C3F-7800-44EF-9F4E-F745D4734965}} \\[0.1em]\hline {\includegraphics[height=0.5em]{F1967534-3246-4366-861D-5F341BA7ACDE}} & {\includegraphics[height=0.5em]{4E5D70F3-5E60-454F-BF1F-40F4772BDBDA}} \\ {\includegraphics[height=0.5em]{A7D19650-8AFF-4236-9D87-545DA369D876}} & {\includegraphics[height=0.5em]{950D88DE-E9B7-4E6E-8D19-13146680937C}} \\ {\includegraphics[height=0.5em]{3CE6D199-F98F-466D-8D41-89674D71AF0A}} & {\includegraphics[height=0.5em]{F0853D72-06C0-4AD6-A7F9-C60F55BCED63}} \\ {\includegraphics[height=0.5em]{0AF1F272-9AF3-4A00-BE1F-FFE3DFB81411}} & {\includegraphics[height=0.5em]{9EB8479F-A706-4777-9A2D-BF9AF7306FBD}} \\ {\includegraphics[height=0.5em]{A17EA37B-B031-4E24-977D-EA5EEE714747}} & {\includegraphics[height=0.5em]{82D55405-BD0C-4723-8074-52F93E692946}} \\ \end{array} Our strategy for defining the connectives is simple; because we consider nil and false from a truth perspective to be the same, we convert all nil arguments to false before computing the result. Proceeding in this way, we obtain the following tables for , , and ¬: \begin{array}{cc} \begin{array}{c|ccc} {\includegraphics[height=0.5em]{74762B22-4F8E-4E15-958E-46C0D3FB8FC5}} & {\includegraphics[height=0.5em]{FCD3E81F-7C70-444B-8A9D-F294A0C08F7F}} & {\includegraphics[height=0.5em]{11055DFC-BB31-4063-921A-8EB1E688D544}} & {\includegraphics[height=0.5em]{57AC549F-26DB-4ED9-8C7D-22772D171689}} \\[0.1em]\hline {\includegraphics[height=0.5em]{BEDDC431-04D7-4CBB-9B45-7FA43D3EAEB5}} & {\includegraphics[height=0.5em]{54CDCF71-A34D-4DDE-BCE2-6C952500ED74}} & {\includegraphics[height=0.5em]{CF8C3D69-5C40-42B9-887F-4821056793B1}} & {\includegraphics[height=0.5em]{0DBB405A-4E0D-48E7-8BF2-24341496D4B6}} \\ {\includegraphics[height=0.5em]{5E7A653D-A2B6-4E22-9875-E32620FDDC81}} & {\includegraphics[height=0.5em]{EC434957-0821-44AF-BEFA-16E3ACAE332A}} & {\includegraphics[height=0.5em]{A6D64D46-2851-4CE1-A956-DA7A3EB66957}} & {\includegraphics[height=0.5em]{7D4B835B-0AE9-4AFE-9F99-764A035E6B20}} \\ {\includegraphics[height=0.5em]{0366F702-0BA7-4C4C-A7ED-4B3BF77D0A52}} & {\includegraphics[height=0.5em]{C48FDB9B-5EF9-4CA8-8985-A7B989748644}} & {\includegraphics[height=0.5em]{379F6F4D-78B2-4500-8F2F-403376DE6CF0}} & {\includegraphics[height=0.5em]{A88F2BB2-0448-4B8F-8EE9-08DE0DFBF2B4}} \end{array} & \begin{array}{c|ccc} {\includegraphics[height=0.5em]{59174FEB-4F99-44A8-9A8B-4B7B9B535BA0}} & {\includegraphics[height=0.5em]{7B1B1A71-E10C-40B1-A7EB-2F41D3049A1B}} & {\includegraphics[height=0.5em]{70EE3EEA-B8FB-44C6-8CE8-67C9645C43F6}} & {\includegraphics[height=0.5em]{DBDBB5FA-DBAE-4B52-91EF-F90E119203DC}} \\[0.1em]\hline {\includegraphics[height=0.5em]{AE8AA7C8-F752-4E49-867D-2AC2C82BAA5F}} & {\includegraphics[height=0.5em]{81407D6E-27ED-44EF-9CF4-9A22C2331A22}} & {\includegraphics[height=0.5em]{8780487F-E91C-4F15-B778-A1B124117457}} & {\includegraphics[height=0.5em]{9454E8B0-E82B-41C6-9739-3F379F9D4D63}} \\ {\includegraphics[height=0.5em]{39F7EFDF-3FD6-433F-9ACE-E6AEB0B59F22}} & {\includegraphics[height=0.5em]{0BF3498A-98F3-4DFC-BC2F-DB3222348DF3}} & {\includegraphics[height=0.5em]{BAD9E2C4-CC64-476E-83F3-DA628938522B}} & {\includegraphics[height=0.5em]{8E754E1C-C677-437B-8B0C-E6A8CB84585C}} \\ {\includegraphics[height=0.5em]{872EFF32-13EA-4703-A7FC-FE3770027DBA}} & {\includegraphics[height=0.5em]{64D8271E-9E6F-49E0-8BB1-218E20375F6F}} & {\includegraphics[height=0.5em]{E2512451-3C86-4523-B79C-8B2DE8E85D51}} & {\includegraphics[height=0.5em]{EEADA137-63D4-46B1-8B35-E750819EBC90}} \end{array} \\ &\\ \begin{array}{c|ccc} {\includegraphics[height=0.5em]{48AC73F3-A7A3-4621-90EA-4D8D7D0D4B84}} & {\includegraphics[height=0.5em]{66FAD80A-61E7-4EE4-B85B-0E86D31FDDE4}} & {\includegraphics[height=0.5em]{98A5031A-4D61-46BF-8AC2-779673110657}} & {\includegraphics[height=0.5em]{11157837-8BCF-40C6-A8E4-5C01C62AE357}} \\[0.1em]\hline {\includegraphics[height=0.5em]{A013BD01-4207-4C6F-A7E6-345983D8438D}} & {\includegraphics[height=0.5em]{0F17C23D-CD1F-4AB8-A32C-156C5EF8794A}} & {\includegraphics[height=0.5em]{24E89B6A-1F8C-4F2C-AE8D-7436E906017D}} & {\includegraphics[height=0.5em]{F34DD212-517D-403C-B5AC-C6D315BF3593}} \\ {\includegraphics[height=0.5em]{7188AE65-97B1-4135-9E79-BA21D670100A}} & {\includegraphics[height=0.5em]{22824FA7-ECF8-46CA-A62F-464B54565B83}} & {\includegraphics[height=0.5em]{2D7DC7F8-9666-46C3-8168-E7A5AC238C82}} & {\includegraphics[height=0.5em]{162861DF-7B41-45F7-BDEA-1DBA6FCF28AA}} \\ {\includegraphics[height=0.5em]{FAB69E60-F5DC-4BCB-AE74-B08FA1FB5A47}} & {\includegraphics[height=0.5em]{DCFF29E9-E5B2-41E1-A29D-51241F0246E4}} & {\includegraphics[height=0.5em]{F6FB61C9-D425-4010-B0F7-E21A89413621}} & {\includegraphics[height=0.5em]{8592FB05-D2C8-4567-A771-079CE8596A6C}} \end{array} & \begin{array}{c|c} {\includegraphics[height=0.5em]{C066953C-92F8-41AC-86D5-0C6F21F90AE7}} & & & \\[0.1em]\hline {\includegraphics[height=0.5em]{8A8B8DA9-4F90-44CD-BBAE-8A7A0710DD79}} & {\includegraphics[height=0.5em]{DC0E350C-DC49-4826-9E15-8BA03DDB27B2}} \\ {\includegraphics[height=0.5em]{707FE9CB-04E0-42AE-9B19-D3D3D098EE39}} & {\includegraphics[height=0.5em]{2D3DF82A-DE79-4D6C-94D8-0F8B81D55100}} \\ {\includegraphics[height=0.5em]{3EF80BDF-3155-4132-84F5-40AFBAD48031}} & {\includegraphics[height=0.5em]{831730AD-E414-4FC0-AFA8-ED98391BB010}} \end{array} \end{array} Equivalence is defined as follows, and contrasted with equality: \begin{array}{c|ccc} {\includegraphics[height=0.5em]{458BBC1B-7E54-4DD6-B289-B7558F0125A1}} & {\includegraphics[height=0.5em]{9CCFB9A2-A503-413D-9341-5D10C876EB60}} & {\includegraphics[height=0.5em]{F4B0C6F6-E835-4AA8-A372-649D6627C9B5}} & {\includegraphics[height=0.5em]{62859054-6C8A-453E-B633-9E50D56A8FF8}} \\[0.1em]\hline {\includegraphics[height=0.5em]{F558329E-6E6B-400B-A391-674C6F093924}} & {\includegraphics[height=0.5em]{C15959B2-5FB4-487F-B9AD-4E3C1AA7FDDC}} & {\includegraphics[height=0.5em]{33FA52DB-7EA2-4503-92CF-39BFC30F61C3}} & {\includegraphics[height=0.5em]{10BD8975-8578-4776-9722-383ECCED1424}} \\ {\includegraphics[height=0.5em]{8ADF0E6F-69B6-4D2E-919D-5F990E60E018}} & {\includegraphics[height=0.5em]{34CC0E8D-BFDF-45F4-9207-34F19C03B2B8}} & {\includegraphics[height=0.5em]{55A50BF3-FE69-4C43-96AD-3ECBC753B65E}} & {\includegraphics[height=0.5em]{D606282A-8558-4E03-A115-CFFE327A1F41}} \\ {\includegraphics[height=0.5em]{E239CBEB-BABA-4F75-9C55-F22B1B5BC5A9}} & {\includegraphics[height=0.5em]{DD9A84CC-72B0-45E4-874B-369DE5E41EB8}} & {\includegraphics[height=0.5em]{1DAD12AF-503C-4C13-8A99-96C8BB5CD9F3}} & {\includegraphics[height=0.5em]{0DDEC1BC-AC8F-45AC-A9B4-95B2594485A6}} \end{array} \quad \begin{array}{c|ccc} {\includegraphics[height=0.5em]{435DED15-2529-47EC-BE73-BC1C0F459631}} & {\includegraphics[height=0.5em]{BF4BC4BD-0C35-4E21-A083-DBBACABB70DE}} & {\includegraphics[height=0.5em]{7B04B324-9C22-4F03-BA42-6BD9E005E483}} & {\includegraphics[height=0.5em]{EA50674C-5BB3-424D-9296-86556A056E5B}} \\[0.1em]\hline {\includegraphics[height=0.5em]{F0B4B5D9-9F41-4AB7-93CC-076CA4EF9B76}} & {\includegraphics[height=0.5em]{C6D3775E-848B-44AA-A541-5398EEF649CA}} & {\includegraphics[height=0.5em]{A15AE56F-6C18-4B80-8E6E-06004BB56F88}} & {\includegraphics[height=0.5em]{BE0FD19D-9969-4D04-83C2-FEAD12E105E1}} \\ {\includegraphics[height=0.5em]{FA572A2C-2463-4ABA-877B-5E83BDC18AA9}} & {\includegraphics[height=0.5em]{DAA70499-B124-4426-9FE0-C47528A5527E}} & {\includegraphics[height=0.5em]{121B8E3E-37B3-435C-936D-311A87725E6A}} & {\includegraphics[height=0.5em]{023F9BE8-9C28-44B8-A2C6-D6FAAA4F7683}} \\ {\includegraphics[height=0.5em]{5F1EF87B-B27B-4A9E-AE6C-71A115BD9B35}} & {\includegraphics[height=0.5em]{6C9BAFFE-38E2-4647-93BE-D0BAA23C2216}} & {\includegraphics[height=0.5em]{F7192A3E-DB95-4141-8B27-9DCDAB1FED97}} & {\includegraphics[height=0.5em]{8B7C4B98-EEB7-4231-BA50-F41399E80C92}} \end{array}
Similarly, quantifiers and work on partial predicates. They both have type
(α : Type) → (α ↪ ℙ) → ℙ
Assume P : α ↪ ℙ. We define and as follows:
Furthermore, the Hilbert choice operator ε has type
(α : Type) → (α ↪ ℙ) ↪ α
and we define it such that if there is x : α with P x = true, then P (ε x : α. P x) = true, otherwise (ε x : α. P x) = nil.
Kerber and Kohlhase [12] argue that the formula
∀ x y z : ℝ. z = x / y ⟶ z ⋅ y = x
should not be a theorem because y = 0 provides a counter example. I don’t agree. The assumption is that for real numbers x,y and z we have z = x / y. This also implies that y cannot be zero, because otherwise x / y would not be a real number.
In Farmer’s approach as well as in Practal above formula is a theorem, albeit for a different reason. While Farmer’s approach and Practal’s approach are closely related, they are not the same. Consider again the formula 1/0 < 2. In Farmer’s approach (1/0 < 2) = false, but in Practal (1/0 < 2) = nil holds. A bigger deviation can be observed for the formula 1/0 = 2/0. This formula is false in Farmer’s approach because the binary predicate = is applied to undefined terms. In Practal this formula is a theorem, because 1/0 = nil and 2/0 = nil both hold.
One of the advantages of nil being specially treated in some situations, but otherwise being a normal value, is that users of Practal can customize undefinedness and optionality for their own particular use case. For example, for defining partial recursive functions you might want to define and use the logical operators from strong Kleene logic [11] as well.

Defining Types

There are various ways to define new types:

structure

For example, in the category use case a new type called Category is introduced. Each instance of the type can be thought of as a record with the corresponding fields, fulfilling the given axioms, and tagged with the name Category to distinguish it from all other records.

typealias

Another way to introduce a new type is via typealias, but the newly introduced type is not really new, but just an abbreviation for the original type. For example, we have
∀ A B : Type. (A ↪ B ) = (A → (B ∪ Nil))

typedef

A third way of introducing a new type is via typedef. We could have also introduced the type of partial functions as follows:
typedef A ↪ B = A → (B ∪ Nil)
The difference to the typealias version is that this type of partial functions consists of entirely new elements. A way to think of the elements of the new type conceptually is as pairs (tag,f)(\text{tag}, f) where tag\text{tag} is Partial-Function, and ff has the type A → (B ∪ Nil). In particular, the following inequality would then be true:
∀ A B : Type. (A ↪ B) ≠ (A → (B ∪ Nil))

Quotient Types

A most common tool employed by mathematicians is the forming of quotients, i.e. forming a new type from an existing type by identifying elements based on an equivalence relation. Also, often when creating quotients one will want to inject existing types into it. We can accommodate both by augmenting a typedef with identify clauses, for example when creating the rational numbers from the integers :
typedef ℚ = ℤ ⨯ (ℤ \ {0}) 
  identify (a, b) in ℚ with (c, d) in ℚ where a ⋅ d = c ⋅ b 
  identify z in ℤ with (z, 1) in ℚ
This results in the rational numbers such that ℤ ≤ ℚ holds, i.e. the integers form a subtype of the rational numbers. We can leave out the in ℚ phrases for the sake of more concise notation and write:
typedef ℚ = ℤ ⨯ (ℤ \ {0}) 
  identify (a, b) with (c, d) where a ⋅ d = c ⋅ b 
  identify z in ℤ with (z, 1)
Similarly, could have been constructed from via
typedef ℤ = ℕ ⨯ ℕ 
  identify (a, b) with (c, d) where a + d = c + b 
  identify n in ℕ with (n, 0)
and thus both ℕ ≤ ℤ and ℕ ≤ ℚ would hold.
One can see now that typealias is really just a special case of typedef. Instead of
typealias B = A
one could also write
typedef B = A 
  identify a in A with a in B

Use Case: Set Theory

When asked what the foundation of mathematics is, most mathematicians will answer "set theory". But it is clear that most mathematicians will not reduce the math they do to set theory, and that concepts from orthodox set theory like ordinal numbers do not play a role in their practice.
In my opinion, types as proposed for Practal are closer to mathematical practice than normal set theory. Practal types are really sets in (not much of a) disguise. The type of sets with elements from A can be modelled often satisfactorily by
typealias Set (A : Type) = A → ℙ
On the other hand, if a mathematician wants to use full Zermelo-Fraenkel set theory, then they should be able to do so in Practal. A simple way to achieve this is to declare a structure that captures the axioms of ZF set theory:
structure ZF = 
  type Set
  let ∈ : Set → Set → ℙ
  let ∅ : Set
  let Un : Set → Set
  let Pow : Set → Set 
  let Repl : Set → (Set → Set) → Set 
  let Sep : Set → (Set → ℙ) → Set
  let Inf : Set 
  axiom Empty: ∀ x : Set. ¬ (x ∈ ∅)
  axiom Extensionality: ∀ x y : Set. (x = y) = (∀ z : Set. (z ∈ x) = (z ∈ y))
  axiom Union: ∀ z x : Set. (z ∈ Un x) = (∃ y : Set. z ∈ y ∧ y ∈ x)
  axiom Power: ∀ x y : Set. (y ∈ Pow x) = (∀ z : Set. z ∈ y ⟶ z ∈ x)
  axiom Replacement: ∀ f : Set → Set. ∀ y X : Set. y ∈ (Repl X f) = (∃ x : Set. x ∈ X ∧ y = f x) 
  axiom Separation: ∀ f : Set → ℙ. ∀ x X : Set. x ∈ (Sep X f) = (x ∈ X ∧ f x) 
  axiom Regularity: ∀ X : Set. X ≠ ∅ ⟶ (∃ x : Set. x ∈ X ∧ (∀ y : Set. y ∈ x ⟶ ¬ (y ∈ X))) 
  def UPair(x : Set, y : Set) = Repl (Pow (Pow ∅)) (λ z. if z = ∅ then x else y)
  def Singleton(x : Set) = UPair(x, x)
  def union(x : Set, y : Set) = Un (UPair(x, y))
  def Suc(x : Set) = union x (Singleton x)
  axiom Infinity: ∅ ∈ Inf ∧ (∀ x : Set. x ∈ Inf ⟶ Suc x ∈ Inf)
end
We then presume the existence of an instance of this structure:
let 𝕌 : ZF
This approach has been used before to work with ZF set theory in higher-order logic. A discussion can be found in my paper about formalizing Partizan Games [13]. More recently, the approach has been used for formalizing ordinal partition relations [14]. Also, one doesn’t need to stop with Zermelo-Fraenkel set theory, but could add further axioms, for example for Grothendieck universes [15].
A set s : 𝕌.Set can be viewed as a type via
{ x : 𝕌.Set | x ∈ s }
and is therefore tightly integrated with other formalizations in Practal. For example, one should be able to prove in Practal that the subsets of a ZF set together with their set-theoretic functions form a category as defined via the Category structure.
I believe that this way of approaching normal set theory is superior to solutions internal to set theory, like for example the one based on urelements I outlined in a mathoverflow post. But both approaches have a lot in common, so it might make sense to combine them somehow.
Harrison makes an emphatic case for the use of sets in ITP instead of types. I think Practal types provide the flexibility that Harrison calls for. In particular, it is not necessary to decide between formalizing a concept as a predicate or as a type, because in Practal, a predicate can also be used as a type without friction.

Controlled Natural Language

Hales has made an argument for the use of controlled natural language in mathematics. I fully agree with it. There will be a controlled natural language for Practal as its topmost user interaction layer.

Paraconsistency

I just recently learnt about paraconsistent logics [16], so my excitement about it is fresh and untainted. The idea behind paraconsistent logics is to prevent the phenomenon of explosion that occurs in classical logic when both H and ¬H can be proven for some proposition H. Because in classical logic H and ¬H together imply false, any proposition G can now be proven although it might have nothing to do with H.
I don’t know whether supporting paraconsistency would make using Practal awkward. It is intriguing that paraconsistency can be considered a dual notion to intuitionism, which is very popular in ITP circles.
What I find interesting about supporting paraconsistency is that it might make playing around with possibly inconsistent objects possible without infecting otherwise supposedly consistent theories. But maybe providing a "Practal playground" where users can assume arbitrary axioms without endangering the consistency of other formalizations is an easier solution for this.
Finally, what if the features of Practal that I have outlined cannot be implemented in a consistent way? There are many gotchas in logic, like Russell’s paradox or Girard’s paradox [17]. I don’t believe that this is the case for Practal, but if indeed a practical logic as envisioned cannot be consistent, maybe paraconsistency is the solution.

Automation

Considering the most impressive strides that artificial intelligence has taken in the last decade or so, Practal is being designed under the assumption that powerful automation can be achieved. This assumption has already been partially validated by projects like Isabelle/Sledgehammer that are based on classical automated theorem proving. Current AI projects like Github Copilot only provide more evidence to support this assumption. In particular, type checking does not have to be decidable; it just has to be certifiable. The assumption of strong automation being achievable frees us from many design constraints that would hinder us in making Practal as useful and pleasant to use as possible.

Conclusion

About seventeen years ago I was told that asking questions is easy, but providing answers is difficult. That is true. What is also true is that if you don’t ask the right question, then the answer does not really matter.
When it comes to Practal, I believe the right question is the following: How do we build an ITP system that is a true bicycle for the mathematical mind? Achieving this goal would mean mathematically inclined people using Practal willingly and happily; because it helps them to think better and faster, instead of slowing them down and hindering their creativity.
If you have any comments, questions, and/or want to share your ideas for Practal, please visit Practal’s discussion forum!

References

[1]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel. (2019). From LCF to Isabelle/HOL, https://doi.org/10.1007/s00165-019-00492-1.
[2]Mohan Ganesalingam. (2013). The Language of Mathematics, https://doi.org/10.1007/978-3-642-37012-0.
[3]William M. Farmer. (2008). The seven virtues of simple type theory, https://doi.org/10.1016/j.jal.2007.11.001.
[4]John Harrison. (2005). A HOL Theory of Euclidean Space, https://doi.org/10.1007/11541868_8.
[5]David Aspinall, Martin Hoffman. (2004). Dependent Types, https://doi.org/10.7551/mitpress/1104.003.0004.
[6]Philip Wadler. (2015). Propositions as types, https://doi.org/10.1145/2699407.
[7]Steven Obua. (2021). A New Semantics for Local Lexing, https://doi.org/10.47757/obua.ll.1.
[8]J. Rushby, S. Owre, N. Shankar. (1998). Subtypes for specifications: predicate subtyping in PVS, https://doi.org/10.1109/32.713327.
[9]David Aspinall, Adriana Compagnoni. (2001). Subtyping dependent types, https://doi.org/10.1016/S0304-3975(00)00175-4.
[10]William M. Farmer. (2004). Formalizing Undefinedness Arising in Calculus, https://doi.org/10.1007/978-3-540-25984-8_35.
[11]Stephen Cole Kleene. (1952). Introduction to Metamathematics, §64: The 3-valued logic, https://www.elsevier.com/books/introduction-to-metamathematics/kleene/978-0-7204-2103-3.
[12]Manfred Kerber, Michael Kohlhase. (1994). A mechanization of strong Kleene logic for partial functions, https://doi.org/10.1007/3-540-58156-1_26.
[13]Steven Obua. (2006). Partizan Games in Isabelle/HOLZF, https://doi.org/10.1007/11921240_19.
[14]Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. (2020). Formalising Ordinal Partition Relations Using Isabelle/HOL, https://doi.org/10.17863/CAM.70018.
[15]Chad E. Brown, Cezary Kaliszyk, Karol Pak. (2019). Higher-Order Tarski Grothendieck as a Foundation for Formal Proof, https://doi.org/10.4230/LIPIcs.ITP.2019.9.
[16]Walter Carnielli, Marcelo Esteban Coniglio. (2016). Paraconsistent Logic: Consistency, Contradiction and Negation, https://doi.org/10.1007/978-3-319-33205-5.
[17]Thierry Coquand. (1986). An analysis of Girard's paradox, https://hal.inria.fr/inria-00076023.