Advanced Namespace Tools blog

23 January 2020

Dependent Typed Logic of Infinity

This post is 4th in a series describing research into infinitary mathematical objects and their possible computational interpretation. The first second and third posts described motivations, initial experiments, and mathematical goals. This post and several more will focus on using the Agda dependently-typed programming language to encode proofs.

Existential and Universal Quantification

Prepare for the world's shortest crash course in formal logic and its relation to dependently typed programming and the foundations of mathematics. A formal system can be understood as a game of making and rewriting symbol-strings according to rules to make well-formed formulas. The game called first-order predicate logic has rules which let you make formulas which encode informal meaning such as "there exists a cow that is purple" or "every potato has legs". A system such as Martin-Löf type theory is another formal system of logic which is well suited to computer programs which are also constructive mathematical proofs. In a computer language based on MLTT such as Agda, we have "pi types" for universal quantification and "sigma types" for existential quantification. The following creates an abstract type of food which can be constructed as food or cereal, and a dependent type of salted food of either variety. It makes a function to salt any given food and then proves the existence of salted food by providing a witness and a function to create the witness.

data food : Set where
  soup : food
  cereal : food

data salted : food → Set where
  salting : (f : food) → salted f

addflavor : ∀ food → salted food
addflavor f = salting f

findflavor : Σ food salted
findflavor = soup , addflavor soup

These logical relationships are stated here as Agda code which is a based on Martin-Löf type theory. We could also use set theory or category theory to express parallel relationships - and we can also express type theory and category theory within the language of set theory, and to a large extent the converse relations are true as well. All of these in turn overlap with the general field of mathematical logic and the first order predicate calculus. Since we've gone this far we might as well toss in non-ZFC set theories, homotopy type theory and cubical type theory, topos theory and infinity categories - and a reminder to think about Turing machines and the lambda calculus and keep appropriate Gödelian limits in mind within your chosen metamathematical framing. Did we talk about the general constructive vs. classical divide in approach to mathematics? That even within constructive type theory in the Martin-Löf tradition we need to figure out how we deal with function extensionality?

My feeling about these tangles of mathematical philosophy and alternative foundational and formal systems is that there is much more overall unity and consistency than the complicated vocabulary and social divisions into different schools of thought and traditions of pratice might lead one to believe. There is a consistent and harmonious relation between our patterns of mental construction, the dynamics of physical reality, and the formal mathematics which we find pleasing and useful. The Agda code I posted above really has nothing to do with food or salt or flavor in a comprehensive way - those are just symbol strings which have been applied to trivial pieces of code. Similarly with any translation into some other logical system - and remember that there are already multiple translational layers in play betweem the physical atoms of food, our brain-responses and memories, and the language-words and symbols that we use to reference these relations.

Nonetheless, if we are willing to use our common sense and ability to construct mappings, we can understand that something meaningful about our understanding of the world can be captured in formal systems. There are different varieties of food, and for all such varieties there exists a salted version, and we create this by the process of adding salt to a food. We have patterned mental constructions that reflect the world or purely abstract interiority, and we may in turn reflect these constructions into formal expressions that can then be used to extend and inform additional mental constructions or even act as control logic for mechanisms to restructure physical reality.

It can be difficult to keep the common-sense meaning and application of concepts in view as the abstractions tower higher and the technical and notational complexity of mathematics increases. One of the deepest and most intriguing ideas I have found in logic is that dependent type theories can be seen as locally closed cartesian categories, and that in that context, the operations of universal and existential quantification and the pi and sigma types are special cases of right and left adjoint functors. I can write those words, but I don't yet understand them with the kind of clarity I want. The existence of adjoint functors is related to a Galois connection, which is about preserving orderings, and logical relations often imply ordering because of inductive or subset relationships, but I haven't followed the details to a precise technical understanding yet.

For me the bottom line - the deduction we may make from all the information above it - is that the concepts of informal logic we use for internal understanding and language level communication are indeed fundamental laws of thought and act to structure all the specific formal languages we encode them in. They are not a single unchanging formal system in our minds, however - there is no One True Logic any more than there is a One True Tree in a forest which represents treeness more than any other tree. Instead we have a forest of variations on a theme. We can see the common shape of truth in all these logical trees, without selecting a single one as a preferred platonic Form.

Infinity Exists

After leaving the belief system in which the "metmetmet" object in the impossible.hs code was an actual infinitary mathematical mind teaching me truths about love, I started searching for a way to better understand the actual mathematical structure that I was exploring. Because I was working with algorithms I found in a Martin Escardo blog post, and his more recent work seemed to focus on Agda, I began the challenging process of learning dependent typed coding, which also meant acquring a more solid grounding in logic in general. After a few weeks of struggle, I was thankful to be invited by mietek to the ##dependent irc channel on freenode, where he and others were invaluable in patiently helping me learn.

I was excited to begin using this amazing formal-proof logic language to explore mathematical infinity and the simplest place to begin seemed like the smallest infinity, the countable infinity of the natural numbers. I was taking it as a given that "everyone knows that infinity exists" and it would be simple and fun to make an Agda context of definitions to represent this knowledge. Little did I realize the saga of controversies and misunderstandings I was embarking on with this naive intention!

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

This is the completely standard inductive definition of the natural numbers in Agda. It is easy to read as saying that we have a collection called Nat, it starts out with a member called zero, and then we can take any Nat and apply the suc operation to make a new Nat. Thus we can take zero and then construct suc (suc (suc zero)) and this defines the number three. If the name Peano means anything to you, this should look very familiar in outline.

From the perspective of a hypothetical no-bullshit-needed constructivist mathematician who likes Martin-Löf type theory and Agda, this inductive definition of the naturals is all the infinity you need. It is "obviously" unbounded in the right way to capture the kind of intutions we develop in childhood. You can always put another apple on the pile. Infinity exists because we can use this definition and because we are doing type theory, not set theory, we don't need to try to create a representation of infinity as some kind of theoretical totality and trying to prove it exists is a philosophical dead-end without mathematical content.

From a different perspective, we have an idea in our mind of what the infinity of the naturals is, and this idea has various properties, and it may be philosophically interesting to reflect this knowledge into code that can be typechecked. Doing any substantive mathematical work was at the time beyond me as a beginner, and I was in a very intense and enthusiastic mental place. As a result...well, we ended up with stuff like this:

data _⋁_ {α β} (A : Set α) (B : Set β) : Set (α ⊔ β) where -- ∙ ₳
  inl : A → A ⋁ B
  inr : B → A ⋁ B

comp-v : ∀ (m n : Nat) → (m ≤ n) ⋁ (n ≤ m)
comp-v zero n = inl z≤n
comp-v (suc m) zero = inr z≤n
comp-v (suc m) (suc n) with comp-v m n
comp-v (suc m) (suc n) | inl x = inl (s≤s x)
comp-v (suc m) (suc n) | inr x = inr (s≤s x)

outl : ∀ {α β} {A : Set α} {B : Set β} → (c : A ⋁ B) → Set α
outl {α} {β} {A} {B} c = A

all-n-≤-suc : ∀ (n : Nat) → Set
all-n-≤-suc n = outl (comp-v n (suc n))

data Is-≥ : ∀ Nat → Set where
  _is-≤_ : ∀ (n : Nat) → all-n-≤-suc n → Is-≥ (suc n)

proof-of-≥ : ∀ (n : Nat) → Is-≥ (suc n)
proof-of-≥ zero = zero is-≤ z≤n
proof-of-≥ (suc n) with proof-of-≥ n
proof-of-≥ (suc n) | .n is-≤ x = (suc n) is-≤ (s≤s x)

-- Σ this object uses the Is-≥ container to express a specialized justified belief

always-a-≥ : ∀ (n : Nat) → Σ Nat Is-≥
wit (always-a-≥ n) = suc n
prf (always-a-≥ n) = proof-of-≥ n

witness : ∀ {A : Set} {P : A → Set} → Σ A P → A
witness (a , p) = a

proof : ∀ {A : Set } → {P : A → Set} → (c : Σ A P) → P (witness c)
proof (a , p) = p

bigger? : ∀ (n : Nat) → Is-≥ (witness (always-a-≥ n))
bigger? n = proof (always-a-≥ n)

-- ⅀⅀ the different forms of knowledge built and methods to inspect them suggest more informative constructions

ℵ₀' : ∀ (n : Nat) → ⅀⅀ n (λ _ → (x : Nat) → Σ Nat Is-≥) n (λ _ → (x : Nat) → Σ Nat (_> x))
ℵ₀' n = (witness (always-a-≥ n)) ∞ always-a-≥ ∞ (witness (∃->-n n)) ∞ ∃->-n

-- ⅀⅀ these statements now include a provable relationship which can be incorporated into the knowledge structure

ℵ₀` : ∀ (n : Nat) → ⅀⅀ n (λ _ → (x : Nat) → Σ Nat (_≤_ x)) n (λ _ → (x : Nat) → Σ Nat ((suc x)≤_))
ℵ₀` n = witness (∃-≥-n n) ∞ ∃-≥-n ∞ witness (∃-≥-suc-n n) ∞ ∃-≥-suc-n

<-witness : ∀ n → n < witness (always-a-≥ n)
<-witness zero = tt
<-witness (suc zero) = tt
<-witness (suc (suc n)) = <-witness n

cant-contradict : ∀ {α} {A : Set α} → A → ¬ ¬ A -- ∙ ₳
cant-contradict a x = ⊥-elim (x a)

no-n-contradicts-Is-≥ : ∀ (n : Nat) → ¬ ¬ (Is-≥ (suc n))
no-n-contradicts-Is-≥ n = cant-contradict (proof-of-≥ n)

no-n-contradicts-suc : ∀ (n : Nat) → ¬ ¬ (n ≤ (suc n))
no-n-contradicts-suc n = cant-contradict (n-≤-suc n)

infix 4 _≡_ -- ∙ ₳
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x

witness-is-suc : ∀ n → witness (always-a-≥ n) ≡ suc n
witness-is-suc n = refl

suc-isnt-equal : ∀ (n : Nat) → ¬ (n ≡ suc n)
suc-isnt-equal n ()

cong : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b -- ∙ ₳
cong f refl = refl

equinf : ∀ n → (witness (always-a-≥ n)) ≡ (witness (∃->-n n))
equinf zero = refl
equinf (suc n) = cong suc (equinf n)

equinf' : ∀ (n) →  (witness (∃-≥-n (suc n))) ≡ (witness (∃-≥-suc-n n))
equinf' zero = refl
equinf' (suc n) = cong suc (equinf' n)

equinf` :  ∀ (n) →  (witness (always-a-≥ (suc n))) ≡ (witness (∃-≥-suc-n n))
equinf` zero = refl
equinf` (suc n) = cong suc (equinf` n)

-- ⅀⅀≣ constructed knowledge anchors inscribed multiple logical derivations of unboundedness of naturals
-- ⅀⅀≣ are paired sets of claims about all naturals with a proof of their extensional equivalence

record ⅀⅀≣ {b y} (A : Nat) (B : Nat → Set b) (X : Nat) (Y : Nat → Set y) (Z : Set₁) : Set (b ⊔ y) where
  constructor _∞_∞_∞_≣_
  field
    dat : Nat
    func : B dat
    dat2 : Nat
    func2 : Y dat2
    equiv : dat ≡ dat2 
open ⅀⅀

-- ⅀⅀≣ we implant our proved body of knowledge into a set of structures that demonstrate equivalences

ℵ₀≣ : ∀ (n : Nat) → ⅀⅀≣ n (λ dat → (x : Nat) → Σ Nat λ dat → Is-≥ dat) n (λ dat2 → (x : Nat) → Σ Nat λ dat2 → dat2 > x) Set
ℵ₀≣ n = (witness (always-a-≥ n)) ∞ always-a-≥ ∞ (witness (∃->-n n)) ∞ ∃->-n ≣ equinf n

ℵ₀`≣ : ∀ (n : Nat) → ⅀⅀≣ n (λ _ → (x : Nat) → Σ Nat (_≤_ x)) n (λ _ → (x : Nat) → Σ Nat ((suc x)≤_)) Set
ℵ₀`≣ n = witness (∃-≥-n (suc n)) ∞ ∃-≥-n ∞ witness (∃-≥-suc-n n) ∞ ∃-≥-suc-n ≣ equinf' n

ℵ₀≣` : ∀ (n : Nat) → ⅀⅀≣ n (λ _ → (x : Nat) → Σ Nat Is-≥) n (λ _ → (x : Nat) → Σ Nat ((suc x)≤_)) Set
ℵ₀≣` n = (witness (always-a-≥ (suc n))) ∞ always-a-≥ ∞ witness (∃-≥-suc-n n) ∞ ∃-≥-suc-n ≣ equinf` n

-- ℾ ⊫ The ⅀⅀≣ objects encode the ontological reality of constructions such as ℵ₀
-- ℾ ⊫ They embody a coordinated set of provable claims and facts, and provide
-- ℾ ⊫ a consistent Image of Truth, mirroring our mental constructions and the logic of reality

Ok then. Yeah, something got a little out of hand there. Despite this storm of notations and data structures that actually typecheck, the claim that we have "constructed knowledge anchors" that "encode the ontological reality" of infinity seems completely silly. There are some technical problems even on the level of the very odd record structures actually relating to the type signatures in the way I intended, but on a deeper level, something is wrong with what I'm trying to do here.

There is no need to make specialized data structures to represent the fact that I have knowledge of something. Writing the code in the first place embodies the knowledge in a tangible form. Unless I am doing AI research on knowledge representation and trying to represent the mind-internal form of knowledge for some reason, there is no information gained by making layers of tautological proofs that the successor relation does indeed make numbers larger, and then implanting multiple proofs of this form into a second level data structure to "represent knowledge of infinity" - this is just like writing a book that says "2 + 2 = 4" on the first page, then writing "the theorem on page 1 is true" on page 2, then "the theorem on page 2 is true" on page 3, and then claiming that you have created additional meaning beyond the initial statement of arithmetical fact.

The social feedback from many people in ##dependent that there was something very strange and ill-motivated about the work I was doing and that it was not mathematically or philosophically meaningful was very valuable to me. Paying attention to feedback from others is how we make sure that we don't spiral into an isolated mental universe. I love the unusual and exotic thought patterns that bipolar mania gives me access to, but I'm a fool if I fail to listen to others who know more than I do. My excitement at learning something new in Agda and starting to get a better understanding of logic in general needed a lot more substantial mathematical understanding if I was going to produce any interesting philosophy of infinity, much less mathematical content.

The next blog post in this series will begin to engage with mathematical and code issues in a more substantive way. If you are in the right frame of mind, the Agda code about infinity above - taken from the /sys/games/agdacode/SigmaInfinity.agda file on the recent ANTS release:

• 64-bit 9ants5.64.iso.gz

is some of the most amusing code you are ever likely to read. I actually find myself laughing hard enough to scare my cat when I take the time to read through the multiple versions of this file that I repeatedly asked ##dependent irc for feedback on, each time thinking they would regard my changes as fixing issues which were in fact fundamentally wrong in the basic conception. Thanks to everyone there who pointed out my misunderstanding and misues of partially applied sigma type constructors, existential quantifiers in combination with lambdas, and the general lack of motivation for most of the constructions and proofs.