Unprovability results involving braids

TL;DR

This paper constructs specific long braid sequences to demonstrate that certain simple combinatorial statements about braid order are true but unprovable in standard arithmetic subsystems, revealing limits of formal proof systems.

Contribution

It introduces a novel method of using braid sequences to establish unprovability results in formal arithmetic systems.

Findings

Certain braid order statements are true but unprovable in ISigma1 and ISigma2.

Long descending braid sequences can encode unprovability results.

Demonstrates limitations of algebraic properties in formal proof systems.

Abstract

We construct long sequences of braids that are descending with respect to the standard order of braids (``Dehornoy order''), and we deduce that, contrary to all usual algebraic properties of braids, certain simple combinatorial statements involving the braid order are true, but not provable in the subsystems ISigma1 or ISigma2 of the standard Peano system.