Separation logic describes heap memory — the dynamic storage a program allocates and deallocates during execution. Its core operator, the separating conjunction, lets you reason about disjoint pieces of memory independently. This modularity is what makes it useful for verifying programs: you can prove properties of one data structure without worrying about others.
A minimal fragment — just the points-to predicate (cell x stores value y), zero, and successor — should be expressively weak. It can describe linked lists and simple heap shapes but lacks quantifiers over heap content, arithmetic operators, or recursive predicates. It seems too sparse to encode serious mathematics.
The paper shows this fragment encodes all Π₀₁ formulas of Peano Arithmetic. Addition, multiplication, and inequality are all representable as patterns of heap cells: a chain of pointers of length n + m simulates addition; nested chains simulate multiplication. The encoding makes the validity problem for this fragment Π₀₁-complete — as hard as the consistency of arithmetic.
The structural point: the heap is accidentally arithmetic. The pointer structure of dynamic memory — cells linked to cells — is rich enough to simulate number theory even when the logic describing it is stripped to its minimum syntax. The decidable fragments of separation logic become undecidable the moment natural numbers enter, no matter how minimally they are introduced. Expressiveness is not a property of the syntax but of the underlying structure the syntax can describe.