Pith. sign in

REVIEW 3 major objections 5 minor 29 references

Meaning as Use, Application, Employment, Purpose, Usefulness

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Pith's one-line read The paper argues that a continuous 'meaning as use' thread runs through Wittgenstein's whole Nachlass, from 1914 to 1951, and that reduction rules in natural deduction and the lambda calculus are its formal counterpart.

desk verdict A useful collection of dated Nachlass passages and a serious, but methodologically under-reported, continuity thesis. read the letter →

arxiv 2506.07131 v2 pith:AEVOEW3F submitted 2025-06-08 math.HO cs.LO

classification math.HOcs.LO MSC 03A0503B4003F05
keywords meaningasuseWittgenstein'sNachlassGebrauchAnwendungVerwendungZweckreductionrulesproof-theoreticsemantics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper argues that a single thread runs through all of Wittgenstein's writings, from the 1914–1916 notebooks to the manuscripts of 1950–51: meaning ties to the use, application, purpose, and usefulness of signs. Drawing on a searchable online edition of the Nachlass, the paper quotes passages where the German terms Gebrauch, Anwendung, Verwendung, and Zweck explain meaning and sense, and claims these passages support a 'meaning-as-use' semantics for predicate logic. It then presents the reduction rules of natural deduction and the $\beta$-reduction rule of the $\lambda$-calculus as the formal counterpart of that semantics, so that meaning is settled by consequences before any set-theoretic model is consulted. The payoff, if the claim holds, is that the standard early/late Wittgenstein divide collapses and proof-theoretic/dialogical semantics gains a direct Wittgensteinian pedigree.

What carries the argument

The machinery pairs a philological lever with a formal lever. The philological lever is the cluster of German terms Gebrauch (use), Anwendung (application), Verwendung (employment), and Zweck (purpose) as they recur in the searchable Nachlass; their presence across six decades carries the continuity claim. The formal lever is the reduction rule — $\beta$-reduction in Church's $\lambda$-calculus and proof-reduction in Gentzen-style natural deduction — treated as the formal face of meaning-as-use: introduction rules are assertion moves, elimination rules are attack moves, and reductions are the defenses that reveal consequences.

What would settle it

A systematic corpus count of Gebrauch, Anwendung, Verwendung, and Zweck co-occurring with Bedeutung or Sinn across all dated Nachlass manuscripts, with dates and manuscript identifiers, would settle the claim: if the co-occurrence clusters in only some periods, or if a late manuscript (1948–51) explicitly denies that a word's use fixes its meaning, the continuous-thread reading would be falsified.

Watch

Extended reading notes

Core claim

The central discovery claimed is that the association of meaning with use, application, purpose, and usefulness 'shows itself from the very beginning through to the very late writings.' The Nachlass passages gathered here run from the WW1 Notebooks (1914–1916), through the 1929–1933 manuscripts in which Wittgenstein asks whether the sense of a sentence is its purpose and says a sign has meaning only when it finds use, to the 1948–1951 'Last Writings' manuscripts connecting meaning with consequences and application. The paper reads even Tractatus remarks 3.326–3.328 as already demanding attention to significant use and employment, and a 1912 letter to Russell as tying the meaning of the generality sign to its inferential use. On the formal side, the paper's claim is that the most basic settlement of meaning for predicate logic is given by reduction rules: the elimination rules acting on the results of introduction rules display a proposition's consequences, and this is what purpose and usefulness look like in a formal system.

Load-bearing premise

The load-bearing premise is that the quoted passages are representative of the whole Nachlass: because the paper reports no search queries, occurrence counts, inclusion or exclusion criteria, or negative cases, the continuity claim stands or falls on the representativeness of its selection.

Editorial extensions

If this is right

  • The early/late distinction collapses: the meaning-as-use reading is not a second-phase invention but a constant of Wittgenstein's philosophy.
  • Tractatus remarks 3.326–3.328 already commit Wittgenstein to a use-based account of symbols, complicating the picture-theory reading of the early work.
  • Proof-theoretic semantics and dialogical/game-theoretical semantics acquire a direct Wittgensteinian lineage, with reduction rules as the formal rendering of meaning-as-use.
  • The meaning of logical constants in predicate logic is fixed by introduction and elimination rules together with their reductions, before any model-theoretic semantics is invoked.
  • In the $\lambda$-calculus, $\beta$-reduction is the primary meaning-constituting operation, prior to set-theoretic or denotational interpretations.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A corpus-wide frequency analysis of Gebrauch, Anwendung, Verwendung, and Zweck co-occurring with Bedeutung and Sinn across all dated manuscripts would test the continuity claim directly and independently of the quoted sample.
  • If the continuity claim is right, the same cluster of terms should also organize Wittgenstein's remarks on mathematics, color, and certainty, offering a unified entry point for teaching the later philosophy.
  • The dialogue-game reading of reduction rules suggests a testable correspondence between normalization theorems (for example, strong normalization of simply typed $\lambda$-calculus) and the requirement that every play in a suitable semantic game terminates.
  • The same search method could be turned on other word clusters such as Regel, Spiel, and Kriterium to check whether the use-terms are uniquely central or merely one of several threads.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper argues that Wittgenstein's Nachlass, from the WW1 Notebooks through very late manuscripts of 1950–51, exhibits a continuous association of meaning with use, application, employment, purpose, and usefulness, thereby challenging the sharp early/late Wittgenstein divide. The evidence is a series of quoted passages, each cited to a specific manuscript page with an access date, together with a proposed formal counterpart: reduction rules in the lambda calculus and in natural deduction are presented as the proof-theoretic/dialogical realization of 'meaning as use'. The paper also claims that Wittgenstein never abandoned the view of language as a calculus, and that the later focus on ordinary language is a return to his early roots rather than a rejection of them.

Significance. If the continuity thesis is accepted, the paper offers a significant revision of standard Wittgenstein scholarship and gives proof-theoretic semantics a direct Wittgensteinian pedigree. The archival excerpts are valuable and precisely located, and the formal material on β-reduction and natural-deduction reduction rules is standard and correctly stated. The strength of the historical conclusion, however, depends on an unreported selection of passages; the paper does not yet establish that the quoted material is representative of the Nachlass as a whole. The significance is therefore real but conditional on a load-bearing methodological point.

major comments (3)
  1. [Abstract; §1; §4] The central claim that the meaning/use association 'shows itself from the very beginning through to the very late writings' and that the Nachlass 'strongly support[s] and augment[s]' the meaning-as-use reading is supported only by a curated set of quotations. The paper reports no search queries, no occurrence counts, no inclusion/exclusion criteria, and no negative cases that would let a reader judge whether the passages are representative of the corpus. Footnote 1's admission that the text 'substantially reinforces earlier arguments' makes the selection mechanism especially load-bearing. Given that §4 concludes from the Nachlass 'at large', the paper should either supply a documented search methodology or explicitly restrict the conclusion to the passages quoted.
  2. [§1, Ms-107, p. 7] The same quoted passage that is offered as early second-phase evidence contains two counter-currents to the thesis: 'Kann man sagen: der Sinn eines Satzes ist sein Zweck?' is posed as an open question, and 'Die Logik kann aber nicht die Naturgeschichte des Gebrauchs eines Worts angehen' explicitly limits what logic can do with use. The paper does not discuss these tensions, so the page reads as more univocal than the source text warrants. The argument needs to address these counter-currents explicitly, or the historical claim should be weakened to say that the association appears in, rather than uniformly governs, these texts.
  3. [§3.2] The assertion that reduction rules constitute 'the most basic settlement of meaning for predicate logic' is not derived from the quoted Wittgenstein texts, which say nothing about introduction/elimination rules or Attacker/Defender roles. The mapping of constructors/destructors to Assertion/Attack/Defense is a proposal from the author's earlier functional/dialogical framework, as the dense self-citation in footnote 35 indicates. The paper should clearly mark this as a proposed formal counterpart rather than a reading directly evidenced by the Nachlass, and should justify why these specific reduction rules are the privileged formalization among other proof-theoretic options.
minor comments (5)
  1. [§3.2] The section heading 'Predicated logic and rules of (proof-)reduction' contains a typo; it should read 'Predicate logic'.
  2. [§1, Ms-117] The access dates for Ms-117 appear twice as '16 Jaan 2025'; both should read '16 Jan 2025'.
  3. [§3.2; References] The in-text reference 'Martin-L¨or 2022' and the reference-list entry 'Corrections of Assertion and Validity of Inference' should be 'Martin-L¨of 2022' and 'Correctness of Assertion and Validity of Inference', respectively.
  4. [§3.2; References] The name 'Ehrenfecht-Fra¨ıss´e' in the text and the reference 'V¨an¨a¨anen' contain typographical errors; they should be 'Ehrenfeucht-Fraïssé' and 'Väänänen'.
  5. [§1 and §2] The paper would be easier to verify if every quoted German passage identified the transcription layer used (e.g., user-filtered vs. diplomatic); currently only the Ms-131 quotation carries this information.

Circularity Check

0 steps flagged · score 1.0 of 10

No demonstrated circularity: primary-source quotations and standard proof theory carry the argument; unquantified sampling and self-citation weaken but do not invert the derivation.

full rationale

The paper makes two kinds of claims. First, a historical-exegetical claim that Wittgenstein's Nachlass associates meaning with Gebrauch, Anwendung, Verwendung, and Zweck continuously from 1914 to 1951. The evidence consists of dated quotations from primary sources (Ms-101, Ms-102, Ms-107, Ms-111, Ms-112, Ms-113, Ms-115, Ms-137, Ms-152, Ms-173, Ms-175, Ms-176, and the Tractatus), which are external to the author's own prior work; their transcription and attribution are checkable, and the claim does not reduce to the author's prior publications. The weakest point is that the paper reports no search queries, occurrence counts, inclusion or exclusion criteria, or negative cases, so the quoted sample may be unrepresentative; that is an evidential limitation, not a definitional or by-construction circularity. Second, the paper makes a proof-theoretic claim that reduction rules (beta-reduction, proof normalization) are a formal counterpart of meaning-as-use. The rules themselves are standard results of Church, Gentzen, Prawitz, and Martin-Lof, and the paper quotes Martin-Lof independently on purpose and assertion. The identification of these rules with 'meaning as use' is a philosophical interpretation argued from the texts, not an equation that takes its conclusion as an input. The author's self-citations are numerous, and footnote 1 acknowledges that the manuscript 'substantially reinforces earlier arguments,' but the load-bearing evidence for the historical thesis is the quoted Wittgenstein corpus, and the formal content is independently established. No step in the paper's chain was found to reduce by construction to its own inputs. Score 1 reflects the presence of an unquantified, possibly self-confirming sample selection and a heavy self-citation apparatus, not a demonstrated circular derivation.

Assumptions & free parameters 1 free parameters · 5 assumptions · 1 invented entities

The mathematical machinery (§3) is standard: beta-reduction and natural deduction rules are textbook material with no new axioms. The paper's genuine load-bearing assumptions are hermeneutic: that the WAB edition is faithful, that the author's translations are accurate, that the four German terms express one stable motif across five decades, and that the author's own functional/proof-theoretic framework is the right formal mirror of the philosophical thesis. The only 'fitted' element is the selection and glossing of passages, which is hand-picked to support the thesis. No new physical or mathematical entities are postulated; the Assertion/Attack/Defense reading of reduction rules is an interpretive mapping, not a checkable prediction.

free parameters (1)
  • Passage selection and interpretive filter
    The Nachlass contains thousands of pages; the paper presents selected quotations supporting the meaning-as-use thesis without reporting the search protocol, occurrence counts, or negative cases, so the interpretation is hand-fitted to the conclusion it illustrates.
assumptions (5)
  • domain assumption The WAB digital edition of the Nachlass is a faithful basis for claims about Wittgenstein's texts
    All quotations are taken from the online WAB IDP resource; the paper relies on this edition's transcriptions being accurate and complete.
  • domain assumption The author's translations of the German passages are accurate
    Each quotation is paired with the author's English translation, which the argument's framing passages depend on; translation choices can bias the interpretation (e.g., rendering 'Gebrauch' as 'use' in philosophical contexts).
  • ad hoc to paper The four German terms (Gebrauch, Anwendung, Verwendung, Zweck) form a single coherent philosophical motif across contexts
    The continuity thesis presupposes these terms express one stable 'meaning as use' theme from 1914 to 1951, despite changes of philosophical direction the paper itself acknowledges; the paper asserts unity rather than demonstrating it.
  • ad hoc to paper The author's functional/proof-theoretic framework (self-cited, e.g., de Queiroz 1987-2025) is the appropriate formal counterpart of the philosophical thesis
    Section 3 presents beta-reduction rules as the formal counterpart of purpose and consequences; this identification comes from the author's own program, not from the Wittgenstein texts, and is asserted by analogy rather than derived.
  • standard math Standard rules of lambda calculus and natural deduction are correct as stated
    The beta-reduction, conjunction, disjunction, implication, universal, existential, and identity rules in section 3 are standard type-theoretic material restated without proof.
invented entities (1)
  • Assertion/Attack/Defense reading of reduction rules (constructor/destructor/redex as the formal counterpart of meaning as use)
    purpose: To give formal-logical content to the 'meaning as use, purpose, consequences' thesis by interpreting introduction rules as assertions, elimination rules as attacks, and beta-reductions as defenses
    This interpretive mapping is asserted in the section 3 tables; it generates no new predictions about lambda calculus or type theory beyond restating standard reduction rules, and the mapping's correctness is not checkable against external benchmarks.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Meaning as Use, Application, Employment, Purpose, Usefulness." pith.science (2026). https://pith.science/paper/AEVOEW3F

@misc{pith2026250607131,
  author       = {Pith},
  title        = {Pith review of: Meaning as Use, Application, Employment, Purpose, Usefulness},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AEVOEW3F}},
  note         = {Machine review of arXiv:2506.07131}
}
read the original abstract

Arising from the whole body of Wittgenstein's writings is a picture of a (not necessarily straight, linear, but admittedly tireless) journey to come to terms with the mechanics of language as an instrument to conceive `reality' and to communicate an acquired conception of the `world'. The journey passes through mathematics, psychology, color perception, certainty, aesthetic, but, looking at it from a sort of birdview, it seems reasonable to say that these are all used as `test beds' for his reflections and `experimentations' towards an all encompassing perspective of such a fundamental gateway to human reasoning and life-revealing as language. Whatever labelling of Wittgenstein as a mystic, a logicist, a conventionalist, a skeptic, an anti-metaphysics, an anti-realist, a verificationist, a pragmatist, a behaviorist, and many others, does not seem to do justice to his absolute obsession with being a persistent `deep diver' into the nature of language. Working with an open and searchable account of the Nachlass has allowed us to identify important aspects of the philosopher's possible common line of thinking, in spite of changes of directions, some of them acknowledged by Wittgenstein himself. One of those aspects is the association of meaning with use, application, purpose, usefulness of symbols in language, which happens to show itself from the very beginning through to the very late writings. The German terms Gebrauch, Anwendung, \emph{Verwendung}, Zweck in relation to meaning, sense of signs, words, sentences, appear in several texts since the WW1 Notebooks (1914--1916) up until very late manuscripts from 1950--51.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

29 extracted references · 26 canonical work pages

  1. [1]

    A set of postulates for the foundation of logic.Annals of Mathematics, Series 2, 33:346–366,

    Church, A.1932. A set of postulates for the foundation of logic.Annals of Mathematics, Series 2, 33:346–366,

  2. [2]

    345–363,

    (Apr., 1936), pp. 345–363,

  3. [5]

    Hintikka, M

    Springer, Dordrecht. Hintikka, M. and Hintikka, J. 1986.Investigating Wittgenstein. Basil Blackwell, Oxford. Hodges, W

  4. [13]

    The Theory of an Arbitrary Higherλ- Model

    https://doi.org/10.1007/s00153-022- 00856-0 Mart´ınez-Rivillas, D.O., de Queiroz, R.J.G.B. 2023a. “The Theory of an Arbitrary Higherλ- Model”.Bulletin of the Section of Logic, 52(1), 39–58. https://doi.org/10.18778/0138-0680.2023.11 . Also arXiv:2111.07092 Mart´ınez-Rivillas, D.O., de Queiroz, R.J.G.B. 2023b. “Solving homotopy domain equations”. (Submitte...

  5. [17]

    Validity of Inferences Reconsidered

    “Validity of Inferences Reconsidered”. In Piecha, T.; Schroeder-Heister, P. (ed.),Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third T¨ubingen Conference on Proof-Theoretic Semantics, 27–30 March 2019, Univ T¨ubingen, pp. 213–226. http://dx.doi.org/10.15496/publikation-35319. de Queiroz, R.J.G.B

  6. [24]

    https://doi.org/10.1007/978-94-011-4574-9 10 de Queiroz, R.J.G.B., Maibaum, T.S.E

    Springer, Dordrecht. https://doi.org/10.1007/978-94-011-4574-9 10 de Queiroz, R.J.G.B., Maibaum, T.S.E

  7. [28]

    p. 33–40. ISSN 2763-8731. DOI: https://doi.org/10.5753/wbl.2021.15776 Scott, D

  8. [30]

    The Strategic Balance of Games in Logic

    The Strategic Balance of Games in Logic. arXiv:2212.01658 Wittgenstein, L. 1974.Letters to Russell, Keynes and Moore, Ed. with an Introd. by G. H. von Wright, (assisted by B. F. McGuinness), Basil Blackwell, Oxford. Wittgenstein, L. 1961.Notebooks 1914–1916,G. H. von Wright and G. E. M. Anscombe (eds.), Oxford: Blackwell. Wittgenstein, L. 1953.Philosophic...

Show all 29 references
  1. [31]

    Edited by the Wittgenstein Archives at the University of Bergen (W AB) under the direction of Alois Pichler

    Wittgenstein, Ludwig: Interactive Dynamic Presentation (IDP) of Lud- wig Wittgenstein’s philosophicalNachlass[wittgensteinonline.no]. Edited by the Wittgenstein Archives at the University of Bergen (W AB) under the direction of Alois Pichler. Bergen: Wittgenstein Archives at t...

  2. [39]

    de Queiroz, R.J.G.B., de Oliveira, A.G., Gabbay, D.M

    Springer, Dordrecht.. de Queiroz, R.J.G.B., de Oliveira, A.G., Gabbay, D.M. 2011.The Functional Interpretation of Logical Deduction. V ol. 5 of Advances in Logic series. Imperial College Press / World Sci- entific, Oct

  3. [78]

    VII + 298 pp 27 Lorenzen, P

    Springer-Verlag, Berlin-G ¨ottingen-Heidelberg. VII + 298 pp 27 Lorenzen, P. 1969.Normative Logic and Ethics, series B.I-Hochschultaschenb ¨ucher. Systema- tische Philosophie, vol. 236∗, Bibliographisches Institut, Mannheim/Z¨urich. Martin-L¨of, P. 1984.Intuitionistic Type The...

  4. [1935]

    I.Math Z39, 176–210

    Untersuchungen ¨uber das logische Schließen. I.Math Z39, 176–210. https://doi.org/10.1007/BF01201353. (English translation in J. von Plato (2017)). Hintikka, J

  5. [1936]

    1991.The Logical Basis of Metaphysics, Harvard University Press, Cambridge (Mass.)

    Dummett, M. 1991.The Logical Basis of Metaphysics, Harvard University Press, Cambridge (Mass.). Frege, G. 1893.Grundgesetze der Arithmetik. Hermann Pohle, Jena 1893 (Band I) 1903 (Band II) Frege, G. 1965.Basic Laws of Arithmetic, partial translation by M. Furth, Univ. Californ...

  6. [1950]

    Konstruktive Begr ¨undung der Mathematik

    “Konstruktive Begr ¨undung der Mathematik”.Mathematische Zeitschrift 53(2):162–202. Lorenzen, P. 1955.Einf ¨uhrung in die operative Logik und Mathematik. Die Grundlehren der mathematischen Wissenschaften, vol

  7. [1965]

    2013.Basic Laws of Arithmetic, Ph

    Frege, G. 2013.Basic Laws of Arithmetic, Ph. A. Ebert and M. Rossberg (eds. and trans.), Oxford University Press,

  8. [1970]

    InThe Kleene Symposium, J

    Lambda Calculus: some models, some philosophy. InThe Kleene Symposium, J. Barwise, H. J. Keisler & K. Kunen (eds.), North-Holland, 1980, pp. 223–265. V¨an¨a¨anen, J

  9. [1975]

    1965.Natural Deduction: A Proof-Theoretical Study

    Call-by-name, call-by-value and theλ-calculus.Theoretical Computer Sci- enceV olume 1, Issue 2, December 1975, Pages 125–159 Prawitz, D. 1965.Natural Deduction: A Proof-Theoretical Study. Acta Universitatis Stock- holmiensis, Stockholm Studies in Philosophy no

  10. [1980]

    The formulae-as-types notion of construction

    “The formulae-as-types notion of construction”. In H. Curry, J.R. Hindley, J. Seldin (eds.),To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and F ormalism. Academic Press (1980). (Original manuscript circulated in 1969.) Lorenzen, P

  11. [1987]

    Note on Frege’s notions of definition and the relationship proof the- ory vs. recursion theory (Extended Abstract)

    “Note on Frege’s notions of definition and the relationship proof the- ory vs. recursion theory (Extended Abstract)”. InAbstracts of the VIIIth International Congress of Logic, Methodology and Philosophy of Science.V ol. 5, Part I, Institute of Philosophy of the Academy of Sci...

  12. [1989]

    Meaning, function, purpose, usefulness, consequences – intercon- nected concepts (abstract)

    “Meaning, function, purpose, usefulness, consequences – intercon- nected concepts (abstract)”. InAbstracts of F ourteenth International Wittgenstein Symposium (Centenary Celebration), 1989, p

  13. [1992]

    Grundgesetze alongside Begriffsschrift (abstract)

    “Grundgesetze alongside Begriffsschrift (abstract)”, inAbstracts of Fifteenth International Wittgenstein Symposium, 1992, pp. 15–16. Symposium held in Kirch- berg/Wechsel, August 16–23

  14. [1994]

    Equality in Labelled Deductive Systems and the functional interpretation of propositional equality

    “Equality in Labelled Deductive Systems and the functional interpretation of propositional equality”. In P. Dekker, and M. Stokhof, (eds.),Pro- ceedings of the 9th Amsterdam Colloquium 1994, ILLC/Department of Philosophy, University of Amsterdam, pp. 547–546. de Queiroz, R.J.G...

  15. [1997]

    The functional interpretation of modal necessity

    “The functional interpretation of modal necessity”. In M. de Rijke, (ed.),Advances in Intensional Logic, Applied Logic Series, Kluwer, 1997, pp. 61–91. de Queiroz, R.J.G.B., Gabbay, D.M

  16. [2005]

    A new basic set of proof transformations

    “A new basic set of proof transformations”. In S. Artemov, H. Barringer, A. Garcez, L. Lamb, & J. Woods (Eds.),We will show them! Essays in 28 Honour of Dov Gabbay(V ol. 2, pp. 499–528). London: College Publications. Peirce, C. S. 1932.Collected Papers of Charles Sanders Peirc...

  17. [2008]

    On Reduction Rules, Meaning-as-use, and Proof-theoretic Seman- tics

    “On Reduction Rules, Meaning-as-use, and Proof-theoretic Seman- tics”.Studia Logica90:211–247. de Queiroz, R. J. G. B. 2023.“From Tractatus to Later Writings and Back – New Implications from Wittgenstein’s Nachlass” SATS, vol. 24, no. 2, pp. 167–203. https://doi.org/10.1515/sa...

  18. [2013]

    Verificationism Then and Now

    “Verificationism Then and Now”. Chapter 1 of M. van der Schaar (ed.), Judgement and the Epistemic F oundation of Logic, Logic, Epistemology, and the Unity of Sci- ence 31, DOI 10.1007/978-94-007-5137-8 1, Springer

  19. [2016]

    Propositional Equality, Identity Types, and Computational Paths

    “Propositional Equality, Identity Types, and Computational Paths”.South Amer . J. of Logic2(2):245–296. Ramos, A.F. 2018.Explicit computational paths in type theory. PhD thesis, CIn-UFPE (August 30 2018). Centro de Inform ´atica, Universidade Federal de Pernambuco, Recife, Bra...

  20. [2021]

    Convers ˜ao de Termos, Homo- topia, e Estrutura de Grup ´oide

    p. 22–25. ISSN 2595-6116. DOI: https://doi.org/10.5753/etc.2021.16371 Ramos, A.F., de Queiroz, R.J.G.B., de Oliveira, A.G. 2021b. “Convers ˜ao de Termos, Homo- topia, e Estrutura de Grup ´oide”. In:Workshop Brasileiro de L ´ogica (WBL), 2, Evento Online. Porto Alegre: Sociedad...

  21. [2025]

    TheK ∞ Homotopyλ-Model

    “TheK ∞ Homotopyλ-Model”. (Sub- mitted for publication.) arXiv:2505.07103 de Oliveira, A.G., de Queiroz, R.J.G.B

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.