A Topological Application of Labelled Natural Deduction

TL;DR

This paper introduces a labelled natural deduction system based on computational paths to compute fundamental groups of topological spaces like the circle, torus, and real projective plane.

Contribution

It presents a novel labelled deduction framework that models equalities and computations between paths, enabling topological calculations within a logical system.

Findings

Successfully computes fundamental groups of key topological spaces

Establishes a new logical approach to algebraic topology

Demonstrates the system's effectiveness in topological calculations

Abstract

We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here: using this system to obtain the calculation of the fundamental group of the circle, of the torus and the real projective plane.