A Bicycle for Your Mathematical Mind

Cite as: https://doi.org/10.47757/practal.1

July 17th, 2021

This is a ﬁrst sketch of the design of Practal, an interactive theorem proving system for practical logic.

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 suﬃcient for purposes of program veriﬁcation, and astonishingly versatile [3]. But the simple types of HOL do not allow for dependent typing; the type of real square matrices with $n$ 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:

- Pick a book or paper, and formalize its ideas within the ITP system to build and further my understanding.
- Formalize my own notions and ideas (e.g. Local Lexing [7]) for the same reasons.

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 ﬁll 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 diﬃculty 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 ﬁxed 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 ﬁnd ingenious solutions to their formalization needs!

In the rest of this paper I will examine ﬁrst use cases, and outline initial design decisions for Practal.

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 deﬁnition 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 deﬁnition 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.

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 deﬁne f x to be equal to nil, where nil is the only value of type Nil. We also deﬁne 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 deﬁned, 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 undeﬁnedness or optionality. We will say more about this in a later section →.

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 undeﬁnedness 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 deﬁned or not, because we could have x : A but ¬(x : C) (or the other way around).

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.

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 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.

In Farmer’s *traditional approach to undeﬁnedness* [10], terms can be undeﬁned, but propositions are always deﬁned by considering atomic propositions containing undeﬁned 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 justiﬁcation 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 deﬁne our logical connectives on ℙ ∪ Nil instead of just on ℙ: $\begin{array}{c|c}
{\includegraphics[height=0.5em]{78AD553E-B6C9-4623-8F65-28E62DB66680}} & {\includegraphics[height=0.5em]{FC0E3982-7D72-45EE-8A51-92242274AF55}} \\[0.1em]\hline
{\includegraphics[height=0.5em]{0033B724-2355-494A-8FED-ED68407D8940}} & {\includegraphics[height=0.5em]{B08C9ED3-7AF4-4067-B336-5ADBB61CE7DD}} \\
{\includegraphics[height=0.5em]{88C8144D-5A0B-4B56-9B7D-21ACB3516089}} & {\includegraphics[height=0.5em]{87AD87C5-013D-4E67-8013-8DA5100601A2}} \\
{\includegraphics[height=0.5em]{F0DAF4A8-1224-496A-AB84-1C3D2097ACC4}} & {\includegraphics[height=0.5em]{485D62E0-9EE0-4AF8-B5CF-5078FD2CDE9D}} \\
{\includegraphics[height=0.5em]{CA5E20FA-1663-427E-A6B2-CD9A195169E1}} & {\includegraphics[height=0.5em]{96C07DB7-9874-4B8D-81B1-912C040196C7}} \\
{\includegraphics[height=0.5em]{D144E5A7-8E8D-4450-96BF-8C9F81D9C860}} & {\includegraphics[height=0.5em]{22E02A89-F7C4-4850-9831-0C30D4D7B700}} \\
\end{array}$ Our strategy for deﬁning 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]{93ACABC8-8599-45FA-90D3-8B3D8BB87644}} & {\includegraphics[height=0.5em]{A9B178DA-366D-4877-879F-B4F0ABFA8ED8}} & {\includegraphics[height=0.5em]{C600294B-27E7-4D14-A660-AF468E21186E}} & {\includegraphics[height=0.5em]{88D64C3C-2255-4036-B76F-2F097ECF664F}} \\[0.1em]\hline
{\includegraphics[height=0.5em]{85DC1936-B091-4E99-9696-AA76D2E9BFF6}} & {\includegraphics[height=0.5em]{DA8635CD-D50F-46DF-9684-0B2C25807EC2}} & {\includegraphics[height=0.5em]{01E44637-6860-4B18-BF12-4DFFFBB51646}} & {\includegraphics[height=0.5em]{DC1F6E0C-49E6-42E0-A6D1-6B9A97DBC234}} \\
{\includegraphics[height=0.5em]{5314DA7F-22DB-4A3B-919F-7F5BF7542194}} & {\includegraphics[height=0.5em]{C7D88F69-81BF-4804-8C29-11AA3D1AD92F}} & {\includegraphics[height=0.5em]{F40A37B1-DD7E-4DC3-B3DC-C141B61C901C}} & {\includegraphics[height=0.5em]{988AC53E-647F-49E2-A6A3-336B5AAA6C41}} \\
{\includegraphics[height=0.5em]{49B11D0B-ADB9-4E59-B56B-5ACB42E63C2A}} & {\includegraphics[height=0.5em]{EEC84E65-863D-48A6-AC8C-AAA242143D70}} & {\includegraphics[height=0.5em]{A2C22251-D8F7-459F-A61C-1F97073F8A57}} & {\includegraphics[height=0.5em]{E0A9341E-9660-430C-880E-5DB40CE5E071}}
\end{array}
&
\begin{array}{c|ccc}
{\includegraphics[height=0.5em]{3378DC23-ECD1-4A9F-B18D-A3FED967EC6F}} & {\includegraphics[height=0.5em]{704E56DD-3974-4DC3-8A86-D1CFFAD8443E}} & {\includegraphics[height=0.5em]{DADEA718-55AD-4FF5-AE23-A3535AC40CE3}} & {\includegraphics[height=0.5em]{8BA58B0B-0EED-4B17-871A-DB8D2EDC740F}} \\[0.1em]\hline
{\includegraphics[height=0.5em]{2A3443E0-5560-42A1-BE34-AB938E258E3A}} & {\includegraphics[height=0.5em]{DF94BB76-93BD-4278-9537-24E84CF82D1B}} & {\includegraphics[height=0.5em]{C15E8AA3-3482-40D6-91AD-C450E719EC32}} & {\includegraphics[height=0.5em]{B17F4DA5-F5FD-45CF-932F-2DCDE0C06FE6}} \\
{\includegraphics[height=0.5em]{15635DB6-B823-465E-B3CE-81B405F201F2}} & {\includegraphics[height=0.5em]{16FB133D-9A22-4E23-AB25-727B080DF017}} & {\includegraphics[height=0.5em]{C6377144-A188-4650-8AFB-524011A93816}} & {\includegraphics[height=0.5em]{9F20A3FE-99D8-4309-91AD-1569932D1B2E}} \\
{\includegraphics[height=0.5em]{D5DD2D72-79D0-40FA-A98F-053BB8313113}} & {\includegraphics[height=0.5em]{8852E61C-C0CD-40FE-B36A-39CFC0CE5EC5}} & {\includegraphics[height=0.5em]{B4825E89-7DA0-4FBB-8AF0-09B386FCE9D7}} & {\includegraphics[height=0.5em]{F3779708-016B-4883-A528-AF680567C375}}
\end{array} \\
&\\
\begin{array}{c|ccc}
{\includegraphics[height=0.5em]{19F3F537-6EF1-472F-9381-DFF175EA12B9}} & {\includegraphics[height=0.5em]{FD9261AE-C360-41C4-8BFF-5BC81F5B82A3}} & {\includegraphics[height=0.5em]{2019AA30-2A5C-4BBD-A282-13E21F7AF53E}} & {\includegraphics[height=0.5em]{B1836794-FE79-4CA1-8771-130CEC78CB92}} \\[0.1em]\hline
{\includegraphics[height=0.5em]{57EF280F-6178-48EB-BAFC-C1887A2E0EB6}} & {\includegraphics[height=0.5em]{574DA145-95CB-4763-B09C-9E88EDFC3150}} & {\includegraphics[height=0.5em]{765D29E5-7AD6-43FA-85A8-998F484E81B3}} & {\includegraphics[height=0.5em]{7B830D85-A3C3-44C7-A52C-2E85E4CC534A}} \\
{\includegraphics[height=0.5em]{83B53D0F-76B9-458F-B7CF-0A506CE34C52}} & {\includegraphics[height=0.5em]{72072F26-C0B3-4B85-A4D9-55DDAA54F9A5}} & {\includegraphics[height=0.5em]{22CA59A2-0E99-4077-A4E4-AE724FD3B794}} & {\includegraphics[height=0.5em]{20436C78-4078-44B4-9142-9488C89DEE97}} \\
{\includegraphics[height=0.5em]{C60CD302-7B6D-4CD1-9BE3-BE7B041BB508}} & {\includegraphics[height=0.5em]{171A4D68-91FB-42A2-B64F-BC145A0F4006}} & {\includegraphics[height=0.5em]{2BD1F7A9-B222-43EA-9CE3-59ACD91F876E}} & {\includegraphics[height=0.5em]{2E76B043-634B-4DF7-8BDC-9E5E7102BCF0}}
\end{array}
&
\begin{array}{c|c}
{\includegraphics[height=0.5em]{435634FF-246A-4966-9231-A82EEA8FDF8C}} & & & \\[0.1em]\hline
{\includegraphics[height=0.5em]{6C521DF0-4B04-42E5-A8EB-DB300A30F257}} & {\includegraphics[height=0.5em]{66C434AC-BFFA-4CD3-ADC4-00266C97209B}} \\
{\includegraphics[height=0.5em]{B9C2225D-93CA-4FE6-836C-E45A83C49B12}} & {\includegraphics[height=0.5em]{02ACF113-67C5-4594-BD71-A88D41DBCA38}} \\
{\includegraphics[height=0.5em]{E9D2C0CA-B388-49FD-9008-8025718F3FA3}} & {\includegraphics[height=0.5em]{6E9B617F-5ECB-474D-8EFE-97054965976A}}
\end{array}
\end{array}$ Equivalence ⟷ is deﬁned as follows, and contrasted with equality: $\begin{array}{c|ccc}
{\includegraphics[height=0.5em]{5B97C335-EBE6-4065-90C0-F3258FF77726}} & {\includegraphics[height=0.5em]{BF6735C7-5EDD-438E-B253-7E41E8859451}} & {\includegraphics[height=0.5em]{7ED40DBE-C726-49ED-9DB4-1F6B6F442B15}} & {\includegraphics[height=0.5em]{45A9E5E3-1784-4389-B1CD-B81E50C245D7}} \\[0.1em]\hline
{\includegraphics[height=0.5em]{B0A98A0A-B393-4669-8912-8494974C823A}} & {\includegraphics[height=0.5em]{A2CB4F6C-02B0-4A38-B612-E5F2DE3557A2}} & {\includegraphics[height=0.5em]{83F9036E-7D3F-4ABA-BF86-10B46DDB2EA5}} & {\includegraphics[height=0.5em]{F354E297-CFB3-44A4-85E5-4DFB68BA784F}} \\
{\includegraphics[height=0.5em]{1DEC8EA5-727B-4698-A648-3A48C99C56C3}} & {\includegraphics[height=0.5em]{B66D37B0-38D1-43D9-996A-C7B260095299}} & {\includegraphics[height=0.5em]{DBC8229D-9976-4782-87A0-7DF5A2DE0C9B}} & {\includegraphics[height=0.5em]{DD3DA033-4AFC-4B97-86AE-CF2A9C68AEBA}} \\
{\includegraphics[height=0.5em]{1FC2AC15-0142-491A-A05E-4D8F94C4535E}} & {\includegraphics[height=0.5em]{4CAE447C-68E8-495F-84B4-7A327B5669D6}} & {\includegraphics[height=0.5em]{E544D279-08E3-4D43-9C76-47B400ADE8D6}} & {\includegraphics[height=0.5em]{FD6469C7-E5BB-4F89-B77A-6A0CEB3A7E82}}
\end{array}
\quad
\begin{array}{c|ccc}
{\includegraphics[height=0.5em]{D8C41C6A-6FF0-4EA1-810F-FC3FFB156CD4}} & {\includegraphics[height=0.5em]{89D96F7C-77D6-4763-AC8B-62ACB5786F47}} & {\includegraphics[height=0.5em]{CDD26F6F-A11C-4BA2-A99B-BB0A03012634}} & {\includegraphics[height=0.5em]{5D9B15E0-A055-45BE-AB5E-2A047B8F94B3}} \\[0.1em]\hline
{\includegraphics[height=0.5em]{6C83132A-5B57-4002-9260-16FB6E9B0D34}} & {\includegraphics[height=0.5em]{8D0E1089-18A4-4D0A-9FAE-429B179C718D}} & {\includegraphics[height=0.5em]{D025F9B1-2712-4FF4-B697-D6006C9BD924}} & {\includegraphics[height=0.5em]{C8F9027F-3A60-4CD7-8028-61AECD9DA45F}} \\
{\includegraphics[height=0.5em]{59F590A3-657E-41ED-82AF-4D86A8894AB1}} & {\includegraphics[height=0.5em]{9DA65BDD-DF96-46FF-904A-C43D170FBA41}} & {\includegraphics[height=0.5em]{9B669B91-F64F-4FD3-BC2D-0C04B537563E}} & {\includegraphics[height=0.5em]{E4252FC8-4884-4C94-971F-A35E4308C8A0}} \\
{\includegraphics[height=0.5em]{6BDFDB9A-900F-4FB1-83F3-5C49F5C895D6}} & {\includegraphics[height=0.5em]{91994C97-5CAE-4665-9F84-CA035D6BA5DC}} & {\includegraphics[height=0.5em]{A91506B9-3084-46D3-8A58-8FE3EB8BFAF2}} & {\includegraphics[height=0.5em]{6AA03534-2122-4BEB-80B2-497770163E8F}}
\end{array}$

Similarly, quantiﬁers ∀ and ∃ work on *partial predicates*. They both have type

(α : Type) → (α ↪ ℙ) → ℙ

Assume P : α ↪ ℙ. We deﬁne ∀ and ∃ as follows:

- If for all x : α we have P x = true then (∀ x : α. P x) = true, otherwise (∀ x : α. P x) = false.
- If there is x : α such that P x = true then (∃ x : α. P x) = true, otherwise (∃ x : α. P x) = false.

Furthermore, the Hilbert choice operator ε has type

(α : Type) → (α ↪ ℙ) ↪ α

and we deﬁne 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 undeﬁned 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 undeﬁnedness and optionality for their own particular use case. For example, for deﬁning partial recursive functions you might want to deﬁne and use the logical operators from strong Kleene logic [11] as well.

There are various ways to deﬁne new types:

- via structure
- via typealias
- via typedef

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 ﬁelds, fulﬁlling the given axioms, and tagged with the name Category to distinguish it from all other records.

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))

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 $(\text{tag}, f)$ where $\text{tag}$ is Partial-Function, and $f$ has the type A → (B ∪ Nil). In particular, the following inequality would then be true:

∀ A B : Type. (A ↪ B) ≠ (A → (B ∪ Nil))

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

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 deﬁned 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 mathoverﬂow 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 ﬂexibility 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.

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.

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 ﬁnd 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.

Considering the most impressive strides that artiﬁcial 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 certiﬁable. 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.

About seventeen years ago I was told that asking questions is easy, but providing answers is diﬃcult. 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!

[8](1998). Subtypes for specifications: predicate subtyping in PVS, https://doi.org/10.1109/32.713327.

[10](2004). Formalizing Undefinedness Arising in Calculus, https://doi.org/10.1007/978-3-540-25984-8_35.

[11](1952). Introduction to Metamathematics, §64: The 3-valued logic, https://www.elsevier.com/books/introduction-to-metamathematics/kleene/978-0-7204-2103-3.

[12](1994). A mechanization of strong Kleene logic for partial functions, https://doi.org/10.1007/3-540-58156-1_26.

[14](2020). Formalising Ordinal Partition Relations Using Isabelle/HOL, https://doi.org/10.17863/CAM.70018.

[15](2019). Higher-Order Tarski Grothendieck as a Foundation for Formal Proof, https://doi.org/10.4230/LIPIcs.ITP.2019.9.

[16](2016). Paraconsistent Logic: Consistency, Contradiction and Negation, https://doi.org/10.1007/978-3-319-33205-5.