pith. sign in

arxiv: 1906.09107 · v1 · pith:R4TABX6Znew · submitted 2019-06-19 · 💻 cs.LO · math.AT

An alternative approach to the calculation of fundamental groups based on labeled natural deduction

Tiago M. L. de Veras , Arthur F. Ramos , Ruy J. G. B. de Queiroz , Anjolina G. de Oliveira This is my paper

Pith reviewed 2026-05-25 19:47 UTC · model grok-4.3

classification 💻 cs.LO math.AT
keywords labelled deductioncomputational pathsfundamental groupsSeifert-Van Kampen theoremnatural deductionterm rewritingKlein bottletorus
0
0 comments X

The pith

A labelled deduction system based on computational paths computes the fundamental groups of the Klein bottle, torus and two-holed torus using the Seifert-Van Kampen theorem.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a labelled natural deduction system in which computational paths, defined as sequences of rewrites, serve as equalities between terms. A term rewriting system is added to establish equalities between these paths. The authors apply the system together with the Seifert-Van Kampen theorem to derive the fundamental groups of the Klein bottle K², the torus T² and the two-holed torus M₂ = T² # T². They present the calculations as simpler than those performed by standard algebraic topology or by homotopy type theory.

Core claim

The central claim is that a labelled deduction system treating computational paths as equalities, equipped with a term rewriting system for path equalities, permits the calculation of the fundamental groups of K², T² and M₂ via the Seifert-Van Kampen theorem in a manner less complex than conventional mathematical proofs or homotopy type theory techniques.

What carries the argument

Labelled deduction system in which computational paths are sequences of rewrites serving as equalities between terms of the same type, together with a term rewriting system that computes equalities between equalities.

Load-bearing premise

The labelled deduction rules and their rewriting system correctly encode the homotopy relations and path compositions needed for the Seifert-Van Kampen theorem to produce the actual topological fundamental groups.

What would settle it

Performing the labelled deduction calculation for the torus and obtaining a group other than the known fundamental group Z × Z would show the encoding does not match topology.

Figures

Figures reproduced from arXiv: 1906.09107 by Anjolina G. de Oliveira, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras.

Figure 1
Figure 1. Figure 1: Deformation retract of X in A by map r(x). On the other hand the composition r∗i : X → X is not the IdX because A ⊂ X, so consider the map H : X ×I −→ X defined by: H(x, t) =    H(x, 0) = x, ∀x ∈ X. H(x, 1) = (r ∗ i)(x) ∈ A, ∀x ∈ X. H(x0, t) = x0, ∀x0 ∈ A. So H is a homotopy between IdX and r∗i, then by lemma 1 we have that (r∗i)∗ = r∗ ∗i∗ is the identity homomorphism of π1(X, x0). Therefore, since r∗ ∗… view at source ↗
Figure 2
Figure 2. Figure 2: Paths (loops) α and β with base point x0 in K2 Given a point x0, we can slice the Klein bottle and represent it as a square whose sides are the loops α and β, how show in figure 5 [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Sliced Klein bottle with oriented paths α and β The figure 5 is a usual representation of Klein bottle where α and β are loops with base point in x0, therefore α, β ∈ π1(K2 , x0). We need to prove the following theorem Theorem 6. π1(K2 , x0) is a free group generated by loops α and β such that βαβα−1 = ρx0 , that is, π1(K 2 , x0) = [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The subsets are represented in darker color. [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: V ∩ W with loop ξx1 . This way we have that ξx1 ∈ π1(V ∩ W, x1), we can define by L the subspace of V ∩ W of the all loops generated by ξx1 , that is, L = [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: r carry x to L. Therefore, we have that L is a deformation retract of V ∩W because there is a map H : V ∩W ×I −→ V ∩W defined by: H(x, t) = (1 − t)x + tr(x) that satisfies, H(x, t) =    H(x, 0) = x H(x, 1) = r(x) H(x, t) = x, ∀a ∈ A. that is, H is a homotopy between r(x) and the identity application in such a way that each point of L remains fixed during homotopy. Since L is a deformation retract of V ∩… view at source ↗
Figure 7
Figure 7. Figure 7: Projection map. Since we can identify the four base points x0 ∈ B˜ as a single point in the quotient space B, we have that B is the subspace of V formed by the collage of two circles (loopsx0 ) by the point x0. So the π1(E, x0) is the free subgroup generated by [αx0 ] and [βx0 ] both elements of π1(E, x0). Taking the construction analogous to the case of the intersection made earlier, if we define a map H … view at source ↗
Figure 8
Figure 8. Figure 8: Every loop in x1 continuously deforms in βαβα−1 . Therefore π1(V, x0) = [PITH_FULL_IMAGE:figures/full_fig_p015_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Paths α and β with base point x0 in Torus Definition 14 (vertical loop). We define as vertical loop the path (loop) that passes through the inner part of T 2 in the vertical direction. In figure 9, this loop is denoted by α. Definition 15 (horizontal loop). We define as horizontal loop the path (loop) that passes the inner part of T 2 in the horizontal direction. In figure 9, this loop is denoted by β. Not… view at source ↗
Figure 10
Figure 10. Figure 10: Sliced Torus with oriented paths α and β. Consider the following path in the figure: τ (β, α, σ(β), σ(α)) = β ∗ α ∗ β −1 ∗ α −1 : Proposition 2. The aforementioned path is rw-equal to the reflexive path. Proof. Indeed, 17 [PITH_FULL_IMAGE:figures/full_fig_p017_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The subsets are represented in darker color. [PITH_FULL_IMAGE:figures/full_fig_p021_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Every loop in x1 continuously deforms in βαβ−1α −1 . Therefore π1(V, x0) = [PITH_FULL_IMAGE:figures/full_fig_p022_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: M2 = T 2 1#T 2 2 Two holed torus. Proof. The results obtained in the last subsections mean that our objective can be obtained rather straightforwardly, as we will see next. Consider M2 = M1 ∪ M2 and see that M0 = M1 ∩ M2 is homotopy equivalent to circle S 1 and therefore π1(M0) ' π1(S 1 ) ' π1(Z). 23 [PITH_FULL_IMAGE:figures/full_fig_p023_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: M1 (left) and M2 (right) . Slicing M1 and M2 , we can represent them as rectangles, whose sides are the loops α1, β1 for M1 and α2, β2 for M2 as shown in figure 14 [PITH_FULL_IMAGE:figures/full_fig_p024_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: M1 sliced and M2 sliced. But Mi is homotopy equivalent to T 2 i minus one point x1 for i = {1, 2}. So we can calculate π1 [PITH_FULL_IMAGE:figures/full_fig_p024_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: T 2 1 r {x1} (left) and T 2 2 r {x1} (right) sliced. Again, from previous results we have: (i) π1(M0, x0) ' Z. (ii) π1(M1, x0) ' [PITH_FULL_IMAGE:figures/full_fig_p024_16.png] view at source ↗
read the original abstract

In this work, we use a labelled deduction system based on the concept of computational paths (sequence 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 use a labelled deduction system based on the concept of computational paths (sequence of rewrites) to obtain some results of algebraic topology and with support of the Seifet-Van Kampen Theorem we will calculate, in a way less complex than the one made in mathematics \cite{Munkres} and the technique of homotopy type theory \cite{hott}, the fundamental group of Klein Blottle $\mathbb{K}^2$, of the Torus $\mathbb{T}^2$ and Two holed Torus $\mathbb{M}_2=\mathbb{T}^2\# \mathbb{T}^2$ (the connected sum two torus).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript introduces a labeled natural deduction system based on computational paths (sequences of rewrites treated as equalities) together with an associated term-rewriting system. It claims that this framework, used in conjunction with the Seifert–Van Kampen theorem, yields the fundamental groups of the Klein bottle K², the torus T², and the two-holed torus M₂ = T²#T² in a manner less complex than the classical treatment in Munkres or the homotopy-type-theory approach.

Significance. If the rewriting rules on computational paths can be shown to enforce precisely the same relations that arise from the inclusions in the Seifert–Van Kampen pushout, the work would supply a purely logical calculus for a standard family of fundamental-group computations. No machine-checked proofs, parameter-free derivations, or reproducible code are supplied, so the significance remains conditional on verification of the encoding.

major comments (2)
  1. [Abstract] Abstract: the central claim that the labeled deduction system produces the fundamental groups “with support of the Seifert-Van Kampen Theorem” is not accompanied by any explicit translation between the term-rewriting rules on computational paths and the amalgamated-product construction or the attaching maps of the theorem; without this translation it is impossible to confirm that the computed presentations coincide with the known topological groups (e.g., ⟨a,b | aba⁻¹b⁻¹⟩ for T²).
  2. [Abstract] Abstract: the repeated assertion of “less complex” calculations relative to Munkres or HoTT is unsupported by any concrete rewriting derivations, length comparisons, or side-by-side examples; the claim is therefore unevaluable from the given text.
minor comments (1)
  1. [Abstract] Abstract: typographical errors include “Seifet-Van Kampen”, “Klein Blottle”, and inconsistent notation for the surfaces (K² vs. ℂ²).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on the manuscript. We respond to each major comment below and indicate the changes planned for the revised version.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that the labeled deduction system produces the fundamental groups “with support of the Seifert-Van Kampen Theorem” is not accompanied by any explicit translation between the term-rewriting rules on computational paths and the amalgamated-product construction or the attaching maps of the theorem; without this translation it is impossible to confirm that the computed presentations coincide with the known topological groups (e.g., ⟨a,b | aba⁻¹b⁻¹⟩ for T²).

    Authors: We agree that an explicit translation is required to make the connection verifiable. The revised manuscript will add a dedicated subsection that maps the term-rewriting rules on computational paths to the relations induced by the inclusions in the Seifert–Van Kampen pushout, thereby confirming that the resulting presentations match the standard ones such as ⟨a, b | aba⁻¹b⁻¹⟩ for the torus. revision: yes

  2. Referee: [Abstract] Abstract: the repeated assertion of “less complex” calculations relative to Munkres or HoTT is unsupported by any concrete rewriting derivations, length comparisons, or side-by-side examples; the claim is therefore unevaluable from the given text.

    Authors: We acknowledge that the claim of reduced complexity lacks supporting derivations or comparisons in the current text. The revision will incorporate explicit rewriting derivations for the torus (and, space permitting, the other spaces) together with a brief side-by-side comparison of derivation length or number of steps against the classical treatment and the HoTT approach. revision: yes

Circularity Check

0 steps flagged

No circularity: external Seifert-Van Kampen theorem invoked as independent support

full rationale

The paper's approach applies a labeled deduction system with term rewriting on computational paths, then invokes the Seifert-Van Kampen theorem (external, cited via Munkres) to obtain fundamental group presentations for K², T² and M₂. No step defines a result in terms of itself, renames a fitted parameter as a prediction, or relies on a load-bearing self-citation whose content is unverified. The rewriting rules are presented as a computational tool whose correctness is assumed to align with the topological theorem rather than being derived from the target groups. This is a standard non-circular application of an external theorem.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the Seifert-Van Kampen theorem as an external domain assumption and on the unstated claim that the labeled system faithfully models path equalities in topology.

axioms (1)
  • domain assumption Seifert-Van Kampen Theorem can be applied inside the labeled deduction system
    Invoked in the abstract to obtain the fundamental-group calculations.

pith-pipeline@v0.9.0 · 5712 in / 1146 out tokens · 23449 ms · 2026-05-25T19:47:10.988960+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

50 extracted references · 50 canonical work pages · 1 internal anchor

  1. [1]

    Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013

    The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book

    work page 2013

  2. [2]

    Roger and Seldin, Jonathan P

    Hindley, J. Roger and Seldin, Jonathan P. Lambda-calculus and combinators: an introduction, 2008. Cambridge University Press

    work page 2008

  3. [3]

    de Oliveira, A. G. Proof transformations for labelled natural deduction via term rewriting. Master’s thesis, Depto. de Informática, Universidade Federal de Pernambuco, Recife, Brazil, April 1995

    work page 1995

  4. [4]

    de Oliveira, A. G. and de Queiroz, R. J. G. B. A New Basic Set of Proof Transformations. In We Will Show Them! Essays in Honour of Dov Gabbay. South American Journal of Logic V olume 2 (2), p.499-528. S. Artemov, H. Barringer, A. Garcez, L. Lamb and J. Woods (eds.), 2005. College Publications, London, ISBN 1904987125

    work page 2005

  5. [5]

    de Queiroz, R. J. G. B. and de Oliveira, A. G. and Ramos, A. F. Propositional equality, identity types, and direct computational paths. South American Journal of Logic, 2(2). p.245-296, 2016. Special Issue A Festschrift for Francisco Miraglia, M. E. Coniglio, H. L. Mariano and V . C. Lopes (Guest Editors)

    work page 2016

  6. [6]

    de Queiroz, R. J. G. B. and de Oliveira, A. G. Term rewriting systems with labelled deductive systems. Proceedings of Brazilian Symposium on Artificial Intelligence (SBIA’94),p.59-74,1994

    work page 1994

  7. [7]

    de Oliveira, A. G. and de Queiroz, R. J. G. B. A normalization procedure for the equational fragment of labelled natural deduction. Logic Journal of IGP.Oxford Univ Press. V ol 7 (2):173-215

    work page

  8. [8]

    de Queiroz, R. J. G. B. and Gabbay, D. M. Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality. p.547-565,1994. ILLC/Department of Philosophy, University of Amsterdam

    work page 1994

  9. [9]

    1900-1982,Hindley, J

    Curry, Haskell B. 1900-1982,Hindley, J. Roger. and Seldin, Jonathan P. To H. B. Curry: Essays on Combinatory Logic Lambda Calculus and Formalism. edited by J.P. Seldin, J.R. Hindley. p.xxv+606pp,1980. London by Academic press

    work page 1900

  10. [10]

    Martin-Löf

    P. Martin-Löf. An intuitionistic theory of types: predicative part, in H. E. Rose and J.C.Shepherdson (eds.) Logic Colloquium ’73, V ol. 80 of Studies in Logic and The Foundations of Mathematics, pp 73 -– 118, North-Holland, Amsterdam,1975. p.viii+513pp, Proceedings of the Colloquium held in Bristol,UK,1973

    work page 1975

  11. [11]

    Martin-Löf

    P. Martin-Löf. Constructive Mathematics and Computer Programming, in L. J. Cohen, J. Los, H.Pfeiffer, and K.-P. Podewski (eds.). Logic, Methodology and Philosophy of Science VI, Series Studies in Logic and The Foundations of Mathematics,pp 153—175, North-Holland, Amsterdam. p.xiii+738pp, 1992. Proceedings of the International Congress held in Hannover, Au...

    work page 1992

  12. [12]

    de Queiroz, R. J. G. B. and Gabbay,D. M. The Functional Interpretation of the Existential Quantifier. Bulletin of the Interest Group in Pure and Applied Logics, 3(2 and 3). p.243–290, 1995. Abstract in JSL 58(2):753–754,

    work page 1995

  13. [13]

    Presented at Logic Colloquium ’91, Uppsala, August 9–16

    work page

  14. [14]

    de Queiroz, R. J. G. B. and Gabbay,D. M. Labelled Natural Deduction. InLogic, Language and Reasoning. Essays in Honor of Dov Gabbay’s 50th Anniversary, H.J. Ohlbach and U. Reyle (eds.). Kluwer Academic Publishers, June 1999. pp. 173-–250

    work page 1999

  15. [15]

    de Queiroz, R. J. G. B; Gabbay, D. M. and de Oliveira, A.G. The Functional Interpretation of Logical Deduction. World Scientific, 2012

    work page 2012

  16. [16]

    de Queiroz, R. J. G. B. and de Oliveira, A. G. Natural deduction for equality: The missing entity. Advances in Natural Deduction - A Celebration of Dag Prawitz’s Work, p.63-91. Springer,2014

    work page 2014

  17. [17]

    de Queiroz, R. J. G. B. and de Oliveira, A. G. Propositional Equality, Identity Types and Reversible Rewriting Sequences as Homotopies. Palestra ministrado no Workshop de Lógica, Universidade Federal do Ceará, Fortaleza, CE. 2014

    work page 2014

  18. [18]

    de Queiroz, R. J. G. B. and de Oliveira, A. G. and Gabbay, D. M. The Functional Interpretation of Logical Deduction. World Scientifi, 2011

    work page 2011

  19. [19]

    V oevodsky

    V . V oevodsky. Univalent Foundations and Set Theory, 2014. Lecture at IAS, Princeton, New Jersey, Mar 2014

    work page 2014

  20. [20]

    Martin-Löf

    P. Martin-Löf. Intuitionistic Type Theory. Series Studies in Proof Theory. Bibliopolis Naples, iv+91pp, 1980.Notes by Giovanni Sambi of a series of lectures given in Padova

    work page 1980

  21. [21]

    On the Identity Type as the Type of Computational Paths

    Ramos, Arthur F. and de Queiroz, R. J. G. B. and de Oliveira, A. G. On the Identity Type as the Type of Computational Paths. http://arxiv.org/abs/1504.04759, 2015

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  22. [22]

    and De Queiroz, Ruy J

    Ramos, Arthur F. and De Queiroz, Ruy J. G. B. and De Oliveira, Anjolina G. On the identity type as the type of computational paths. Logic Journal of the IGPL,vol.25 (4), p.562-584, 2017

    work page 2017

  23. [23]

    Topology (2nd Edition), Chapter 9, Topic 54 - The fundamental group of circle, Pearson, 2000

    Munkres, James R. Topology (2nd Edition), Chapter 9, Topic 54 - The fundamental group of circle, Pearson, 2000. Institute for Advanced Study

    work page 2000

  24. [24]

    Licata, Daniel and Shulman, Michael

    R. Licata, Daniel and Shulman, Michael. Calculating the Fundamental Group of the Circle in Homotopy Type Theory, 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2013. ACM/IEEE

    work page 2013

  25. [25]

    http://plato.stanford.edu/archives/win2014/entries/category-theory/, interview published in google discussion group of Homotopy Type Theory, by Martin H

    Vladimir V oevodsky to Martin Escardo, In the vein of bringing to public record things that Vladimir said, here is a short interview. http://plato.stanford.edu/archives/win2014/entries/category-theory/, interview published in google discussion group of Homotopy Type Theory, by Martin H. Escardo On Thursday, 12 October 2017 20:24:26, in response to an inte...

    work page 2017

  26. [26]

    Martin-Löf

    P. Martin-Löf. Intuitionistic Type Theory. Series Studies in Proof Theory. Bibliopolis Naples, iv+91pp, 1980. Notes by Giovanni Sambi of a series of lectures given in Padova. 26 An alternative approach to the calculation of fundamental groups based on labeled natural deductionA PREPRINT A Subterm Substitution In Equational Logic, the sub-term substitution...

    work page 1980

  27. [27]

    τ(C[r],C[σ(r)])⊿trC[ρ]

    work page

  28. [28]

    τ(C[σ(r)],C[r])⊿tsrC[ρ]

    work page

  29. [29]

    τ(C[r],C[ρ])⊿trrC[r]

    work page

  30. [30]

    τ(C[ρ],C[r])⊿tlrC[r]

    work page

  31. [31]

    subL(C[r],C[ρ])⊿slrC[r]

    work page

  32. [32]

    subR(C[ρ],C[r])⊿srrC[r]

    work page

  33. [33]

    subL(subL(s,C[r]),C[σ(r)])⊿slss

    work page

  34. [34]

    subL(subL(s,C[σ(r)]),C[r])⊿slsss

    work page

  35. [35]

    subR(C[s], subR(C[σ(s)],r ))⊿srsr

    work page

  36. [36]

    subR(C[σ(s)], subR(C[s],r ))⊿srrr r

    work page

  37. [37]

    µ(t,ξ 1(r),ξ 2(s))⊿mxxt

    work page

  38. [38]

    σ(τ(r,s ))⊿stssτ(σ(s),σ (r))

    work page

  39. [39]

    σ(subL(r,s ))⊿ssbl subR(σ(s),σ (r))

    work page

  40. [40]

    σ(subR(r,s ))⊿ssbr subL(σ(s),σ (r))

    work page

  41. [41]

    σ(ξ(s,r ))⊿sxssξ(σ(s),σ (r))

    work page

  42. [42]

    σ(µ(s,r ))⊿smssµ(σ(s),σ (r))

    work page

  43. [43]

    σ(µ(r,u,v ))⊿smsssµ(σ(r),σ (u),σ (v))

    work page

  44. [44]

    τ(r, subL(ρ,s ))⊿tsbll subL(r,s )

    work page

  45. [45]

    τ(r, subR(s,ρ ))⊿tsbrl subL(r,s )

    work page

  46. [46]

    τ(subL(r,s ),t )⊿tsblrτ(r, subR(s,t ))

    work page

  47. [47]

    τ(subR(s,t ),u )⊿tsbrr subR(s,τ (t,u ))

    work page

  48. [48]

    τ(τ(t,r ),s )⊿ttτ(t,τ (r,s ))

    work page

  49. [49]

    τ(C[u],τ (C[σ(u)],v ))⊿ttsv

    work page

  50. [50]

    τ(C[σ(u)],τ (C[u],v ))⊿tstu 28

    work page