Chapter 2 — The Logic of Being

{-# OPTIONS --cubical --guardedness #-}

module ch02-being where

Where we are

Chapter 1 introduced Concepts (types), Judgments (typing), and the Syllogism (function composition). Those Concepts were postulated — we never asked “what is the simplest possible Concept?”

The Science of Logic begins not with the syllogism but with the pair Pure Being (Sein) and Pure Nothing (Nichts). Hegel argues these are equally indeterminate, and their tension gives rise to Becoming (Werden). Here we set up the type-theoretic correspondents:

What’s at stake

Pure Being is not picked out of a hat. Hegel chooses it as the starting point because it presupposes nothing: every other concept (a chair, a number, justice — anything determinate) carries content that would have to be justified having smuggled in. Pure Being carries no content. It’s where you start if you want a logic with no foreign assumptions.

The whole Science of Logic depends on what happens next. If thought can move at all from Pure Being to its opposite without importing external content — if Being collapses into Nothing just by being thought through honestly — then the categories of thought are self-generating and the dialectical engine is real. If thought can’t make that move, the entire programme stalls at step one.

Said more directly: Hegel is trying to give a logical account of how something arises from nothing. Why is there something rather than nothing at all? You can’t answer that question without a way to derive determinate content from sheer indeterminacy. Chapter 2 is where the derivation either starts or fails.

1. Pure Being (Das Sein)

Hegelian thesis

Hegel’s Pure Being is the most abstract concept possible: pure existence without any further qualities. “X is” — said of nothing in particular and without further specification.

The Science of Logic opens with this concept (§132). Hegel emphasizes that Pure Being has no determinations whatsoever: no content, no internal distinction, no relation. It is the absolute beginning precisely because it presupposes nothing.

Intuition

A type-theoretic correspondent should be a type that “just is” — inhabited, but trivially. The natural choice: a type with exactly one inhabitant, where the inhabitant carries no information. That is the unit type, traditionally written ⊤ (“top”).

In code

Agda’s record keyword defines a type whose values are tuples of fields. A record with no fields and a single constructor tt is inhabited by exactly one value.

record ⊤ : Set where
  constructor tt

Reads as

“Pure Being ⊤ is the type whose sole inhabitant is tt, with no further data.”

2. Pure Nothing (Das Nichts)

Hegelian thesis

Hegel’s Pure Nothing is the categorical opposite of Pure Being: the concept under which nothing falls. He insists that Pure Nothing is not merely “the absence of being” but a positive thinking of the non-being itself.

The Science of Logic asserts that Pure Nothing has the same indeterminacy as Pure Being. Both lack any qualities. This is already the seed of the dialectical move to come — but we develop that in Section 3.

In code

In type theory the categorial opposite of “one inhabitant” is “no inhabitants.” We declare a type with data and provide no constructors. There is then no way to build a term of type ⊥, and under propositions-as-types, ⊥ is the proposition that is provably false.

data ⊥ : Set where
  -- (intentionally no constructors)

Reads as

“Pure Nothing ⊥ is the type with no inhabitants whatsoever.”

3. Becoming (Das Werden)

Hegelian thesis

Hegel’s central early move: Being and Nothing are equally indeterminate, so they “pass over into each other.” Their truth is Becoming — the movement between them (§134 ff.). The famous formulation is that Sein and Nichts are identical in their truth.

This is the move the chapter promised. If it works, Hegel has begun answering the deepest question of the Logic: how does determinate content arise from sheer indeterminacy? Becoming is the first determinate concept — the first something — and it is generated by the tension between two indeterminate ones. No external content was imported; the movement is internal to thought itself.

Caveat: This chapter only models the form of the transition — two functions, one in each direction. The much stronger claim that Sein and Nichts are identical is formalized in Chapter 4 using a Higher Inductive Type. Consistent formal logic cannot make ⊤ and ⊥ judgmentally equal, so the identification will happen at the path level rather than the equation level. (See Higher Inductive Types for the relevant Cubical primitive.)

Why this matters: for Hegel, the process is the philosophy. It is not just that Being and Nothing turn out to be identical — it is that thought discovers their identity by working through the contradiction. The collapse is the dialectical move. Our formal version, by contrast, gives the destination (a path-identification, in Chapter 4) without the journey. This is the place a reader skeptical of formalizing Hegel will plant their flag, and they are not wrong to do so. We accept the gap openly: what we capture is the result the contradiction is meant to produce, not the productive contradiction itself.

Intuition

For now, a first weak way to model the transition: any type X sits “between” ⊥ and ⊤, because there is a unique function ⊥ → X (the principle of explosion: from nothing, anything follows) and a unique function X → ⊤ (any determinate thing can be stripped of its qualities and reduced to bare existence).

        ⊥ ───── from-nothing ─────▶ X ───── to-being ─────▶ ⊤

These functions exist for trivial categorical reasons (⊥ is initial, ⊤ is terminal in the category of types). They carry no information in themselves — Chapter 4 will give the transition real content.

In code

The function from Nothing into any type uses the absurd pattern (). This tells Agda: “there are no inhabitants of ⊥ to consider, so this function is defined everywhere it needs to be defined (which is nowhere).”

from-nothing : {X : Set} → ⊥ → X
from-nothing ()

The function to Being throws away its input and returns the unique inhabitant of ⊤:

to-being : {X : Set} → X → ⊤
to-being x = tt

Reads as

From ⊥: “From the empty type, a function to any type X exists vacuously — there is nothing to map, so every case is handled.”

To ⊤: “Any term of type X collapses to the featureless point of Pure Being.”

What we verified

In this chapter, Agda has checked these constructions:

• ⊤ is well-formed as a unit type with sole inhabitant tt.
• ⊥ is well-formed as an uninhabited type.
• from-nothing : {X : Set} → ⊥ → X typechecks — the principle of explosion is a real Agda function.
• to-being : {X : Set} → X → ⊤ typechecks — the unique map to the terminal type is constructed explicitly.

What we now know that we didn’t before: the structural form of Hegel’s opening move has a type-theoretic shape — ⊤, ⊥, and the bare arrows between them and any type. What we have is the destination of the Sein-Nichts collapse; what we do not have yet, and what Chapter 4 reaches for, is its dialectical content.

What’s next

Chapter 3 replaces our postulates with real proofs, introduces paths from Cubical Agda, and begins to give the bare construction of “Becoming” real content. We will see the first place the --cubical pragma earns its keep: a proof that Pure Being is contractible, which is much stronger than “has one inhabitant.”