English

A Topological Application of Labelled Natural Deduction

Logic in Computer Science 2021-05-11 v4 Algebraic Topology

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.

Keywords

Cite

@article{arxiv.1906.09105,
  title  = {A Topological Application of Labelled Natural Deduction},
  author = {Tiago M. L. Veras and Arthur F. Ramos and Ruy J. G. B. de Queiroz and Anjolina G. de Oliveira},
  journal= {arXiv preprint arXiv:1906.09105},
  year   = {2021}
}

Comments

42 pages, 5 figures. arXiv admin note: text overlap with arXiv:1804.01413, arXiv:1803.01709, arXiv:1906.09107