pith. machine review for the scientific record. sign in

arxiv: 2605.05368 · v2 · submitted 2026-05-06 · 🧮 math.LO · cs.AI

Recognition: 2 theorem links

· Lean Theorem

Towards an Inferentialist Account of Information Through Proof-theoretic Semantics

David Pym, Matthew Collins, Timo Eckhardt

Pith reviewed 2026-05-11 01:42 UTC · model grok-4.3

classification 🧮 math.LO cs.AI
keywords inferentialismproof-theoretic semanticsinformation theoryinferondistributed systemssemanticslogiccorrelation
0
0 comments X

The pith

Replacing truth with inferability yields the inferon as information's primitive unit

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

The paper develops an inferentialist approach to information by using proof-theoretic semantics to replace the role of truth with inferability. This shift allows for a logical account of information grounded in reasoning rather than correspondence to facts. The authors introduce the inferon as the basic unit in this framework. They connect this to modeling information flow in distributed systems. A sympathetic reader would care because it provides mathematical tools for understanding information in complex computational environments where truth may not be straightforward.

Core claim

We replace truth with inferability in the key concepts of information and trace the consequences. Using proof-theoretic semantics, we develop the first steps towards a mathematical-logical theory of an inferentialist primitive unit of information, the 'inferon'. This proof-theoretic approach counterpoints the model-theoretic view of information articulated in situation theory. It facilitates addressing information as range, as correlation, and as code with a focus on correlation. This yields a reasoning-based theory of information flow in models of distributed systems.

What carries the argument

The inferon, the inferentialist primitive unit of information realized through proof-theoretic semantics by substituting inferability for truth.

Load-bearing premise

That replacing truth with inferability in existing information concepts, realized via proof-theoretic semantics, yields a coherent and useful theory for information in distributed systems.

What would settle it

A concrete distributed system example where an inferon-based analysis of information transmission produces inconsistent or incomplete results compared to established truth-based accounts of the same flows.

Figures

Figures reproduced from arXiv: 2605.05368 by David Pym, Matthew Collins, Timo Eckhardt.

Figure 1
Figure 1. Figure 1: Base rules: atomic, level 1, and level 2, respectively valuation of the atom. The meaning of the remaining connectives is then defined inductively, with the meaning of implication formulæ requiring, analogously to the requirement for base-extensions described above, judgements relative to worlds higher in the ordering. In fact, looking at the current world instead will incur the vacuous satisfaction proble… view at source ↗
Figure 2
Figure 2. Figure 2: Notational conventions view at source ↗
Figure 3
Figure 3. Figure 3: Sandqvist’s B-eS for intuitionistic propositional logic and Gheorghiu’s extension of it to first-order While view at source ↗
Figure 4
Figure 4. Figure 4: The calculus NJ in sequential form (eliding ⊤) [69, 84, 52] It is base-extension semantics that provides the logical basis for the use of bases to provide the inferential alternative to infons that we call inferons. In this setting, developed in Section 5, we need to define base rules of atoms of the form ⟨p, b⟩, where p is a propositional or predicate atom and b is a boolean polarity.4 5. An Inferentialis… view at source ↗
Figure 5
Figure 5. Figure 5: Inferonic base rules Other forms of bases rules are also possible (e.g., [77]). It could be suggested that the presence of polarities in inferonic atoms constitutes a degree of ‘semantic pollution’ [72]. We would argue that our set-up lies within the scope of Avron’s criterion [5] for acceptability, that ‘ . . . the framework should be independent of any particular semantics. One should not be able to gues… view at source ↗
Figure 6
Figure 6. Figure 6: Support relation for inferons: propositional case The base-extension semantics presented here very closely corresponds that for intutionistic logic, the difference being the inferonic structure of propositions. For the soundness and completeness of this theory of inferons, we consider the the derivability relation given by NJ with inferons as atomic formulæ and with the (Inferon) axiom, as given in view at source ↗
Figure 7
Figure 7. Figure 7: The axiom (Inferon) for the theory of inferons The (Inferon) axiom, as given in view at source ↗
Figure 8
Figure 8. Figure 8: Support relation for inferons: first-order case Theorem 11 (soundness) and Theorem 12 (completeness) can be extended to the first-order case (see [44]), with the same adaptations to handle the atomic cases. As [44] uses a Hilbert-type axiomatic proof-system, this extension is not completely trivial. However, our treatment of quantifiers in the semantics is equivalent to that in [44] and so the differences … view at source ↗
Figure 9
Figure 9. Figure 9: Compound inferons, with internal logical connectives Lemma 13. For any compound inferon ⟨⟨ϕ,P, b⟩⟩, there exists a non-compound inferon ψ such that, for any B, ⊩B ⟨⟨ϕ,P, b⟩⟩ iff ⊩B ψ Proof. This follows from a simple induction on the complexity of ϕ using the extension of the support relation in view at source ↗
Figure 10
Figure 10. Figure 10: Contextual support relation For any site P, let B(P) be the base consisting of the rule set {⇒ ι | ι ∈ P}. The following is easily shown: P ⊢B ι iff ⊢B∪B(P) ι for all ι, P and B. From this it follows that Θ ⊩ P B ϕ iff Θ ⊩B∪B(P) ϕ view at source ↗
Figure 11
Figure 11. Figure 11: The airport security system (taken from [47]) l1 (check-in): The passport p is checked for validity. This involves using some of the atomic inferonic information ⟨⟨IW (p), 1⟩⟩ carried by the passport. A ticket t is issued. This functions as an authentication token that is used in subsequent stages. The ticket carries this authentication information as an inferonic atom ⟨⟨T(t), 1⟩⟩. Not all of the informat… view at source ↗
Figure 12
Figure 12. Figure 12: A generic distributed system (taken from [47], cf. [56]) Certain substructural logics are well-known to be useful in producing richer models than can be expressed purely in intuitionistic logic. For example, multiplicative linear logics have a number-of￾uses reading, while bunched logics have a sharing interpretation. It is known how to give a base extension semantics to both the linear logic IMALL and th… view at source ↗
read the original abstract

Information is one of the most widely-discussed concepts of the current era. However, a great deal of insightful work notwithstanding, it is yet to be given wholly convincing logical or mathematical foundations. Without them, we lack adequate reasoning tools for understanding the complex ecosystems of systems upon which the society depends. We seek to rectify this by taking a first step towards developing an inferentialist semantic theory of information. There are three key interacting components. First, conceptual analysis: the metaphysics of information. Dretske expressed the key concepts of information in terms of intentionality, truth, and transmissibility. We replace truth with inferability, and trace the consequences of this replacement. Second, logic: proof-theoretic semantics (P-tS) provides a mathematical-logical realization of inferentialist reasoning. Using P-tS, we develop the first steps towards a mathematical-logical theory of an inferentialist primitive unit of information, the 'inferon'. This proof-theoretic approach counterpoints the model-theoretic view of information articulated in situation theory. Furthermore, we argue that it facilitates addressing all three components of van Benthem and Martinez's categorization of the understandings of information, as range, as correlation, and as code. Our focus is on information-as-correlation. Third, systems: the P-tS tools we develop provide the basis for a mathematical account of distributed systems modelling -- a key tool from informatics for understanding the organization of information processing systems. This yields a reasoning-based theory of information flow in models of distributed systems. Overall, we seek to give a conceptually rigorous mathematical-logical account of information and its role within informatics, grounded in inference and reasoning.

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 / 0 minor

Summary. The paper proposes taking first steps toward an inferentialist account of information by replacing truth with inferability in Dretske's framework of intentionality, truth, and transmissibility. It invokes proof-theoretic semantics (P-tS) to introduce the 'inferon' as a primitive unit of information, contrasts this with situation theory, and claims this approach addresses van Benthem and Martinez's three understandings of information (range, correlation, code) with focus on correlation. The work further aims to supply P-tS-based tools for modeling information flow in distributed systems.

Significance. If the announced replacement of truth by inferability were carried out with explicit P-tS constructions and shown to yield coherent notions of transmissibility and intentionality while preserving key properties from Dretske-style information theory, the resulting inferentialist primitive could complement model-theoretic approaches and provide a reasoning-based foundation for information in informatics. The programmatic outline correctly identifies a potential gap in logical foundations for information ecosystems, but the absence of any realized formal objects limits immediate impact.

major comments (2)
  1. [Abstract] Abstract: The central claim that 'Using P-tS, we develop the first steps towards a mathematical-logical theory of an inferentialist primitive unit of information, the inferon' is unsupported. No explicit definition of the inferon (e.g., as a canonical proof object, a set of introduction/elimination rules, or a derived notion in a P-tS framework), no concrete replacement of truth by inferability in any Dretske-style concept, and no demonstration that the resulting notion preserves or reinterprets transmissibility or intentionality appear anywhere in the manuscript.
  2. [The manuscript as a whole] The manuscript as a whole: The announced application to distributed systems modeling and to information-as-correlation is presented only at the level of a high-level program. No specific P-tS rules, sequent calculi, or proof-theoretic derivations are supplied that would realize information flow or correlation in a distributed-systems setting, leaving the claim that the tools 'provide the basis for a mathematical account' without technical content.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful and constructive report. The comments correctly identify the exploratory character of the work, and we have revised the manuscript to add greater explicitness and illustrative technical content while preserving its framing as first steps toward an inferentialist account.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that 'Using P-tS, we develop the first steps towards a mathematical-logical theory of an inferentialist primitive unit of information, the inferon' is unsupported. No explicit definition of the inferon (e.g., as a canonical proof object, a set of introduction/elimination rules, or a derived notion in a P-tS framework), no concrete replacement of truth by inferability in any Dretske-style concept, and no demonstration that the resulting notion preserves or reinterprets transmissibility or intentionality appear anywhere in the manuscript.

    Authors: The paper is deliberately positioned as taking first steps, introducing the inferon conceptually as the primitive unit grounded in inferability rather than truth, realized via the inferentialist resources of proof-theoretic semantics. We trace the replacement of truth by inferability through Dretske's triad and argue that intentionality and transmissibility can be reinterpreted in terms of inferential relations and preservation of inferability across channels. We acknowledge that a fully axiomatized definition with specific introduction/elimination rules is not supplied, as that would exceed the scope of an initial outline. In the revised manuscript we have added a dedicated subsection that characterizes the inferon more precisely as a canonical proof object in a natural-deduction setting and sketches the reinterpretation of transmissibility as preservation of inferability. revision: yes

  2. Referee: [The manuscript as a whole] The manuscript as a whole: The announced application to distributed systems modeling and to information-as-correlation is presented only at the level of a high-level program. No specific P-tS rules, sequent calculi, or proof-theoretic derivations are supplied that would realize information flow or correlation in a distributed-systems setting, leaving the claim that the tools 'provide the basis for a mathematical account' without technical content.

    Authors: The referee is right that the distributed-systems application remains programmatic; the manuscript's primary contribution is the conceptual and logical groundwork for treating information-as-correlation within a proof-theoretic framework, in contrast to situation theory. No claim is made to a complete implementation. To meet the concern we have inserted a short illustrative example in the revised version, consisting of a simple sequent-calculus derivation that shows how inferons can encode correlation-based information flow between agents in a minimal distributed scenario. This supplies concrete technical content without altering the paper's foundational orientation. revision: partial

Circularity Check

0 steps flagged

No circularity: conceptual proposal with no load-bearing derivation that reduces to inputs

full rationale

The manuscript presents a high-level program: conceptual replacement of truth by inferability in Dretske-style information notions, followed by the introduction of an 'inferon' as a primitive via proof-theoretic semantics, with the goal of addressing information-as-correlation in distributed systems. No equations, formal definitions, or derived predictions appear in the supplied text that would allow a claimed result to be shown equivalent to the framing by construction. The steps remain programmatic statements rather than a closed mathematical chain. Self-citation (if present) is not invoked to justify a uniqueness theorem or to force the central object. The work is therefore self-contained as an outline of future formalization rather than circular.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The proposal rests on conceptual replacements from prior information theory and the introduction of new primitives without independent empirical or formal grounding shown in the abstract.

axioms (2)
  • domain assumption Inferentialist semantics can replace truth with inferability while preserving key information concepts
    Invoked in the conceptual analysis section of the abstract.
  • domain assumption Proof-theoretic semantics realizes inferentialist reasoning mathematically
    Used to develop the inferon theory.
invented entities (1)
  • inferon no independent evidence
    purpose: primitive unit of information in the inferentialist theory
    Newly postulated concept introduced to ground the account.

pith-pipeline@v0.9.0 · 5598 in / 1225 out tokens · 46081 ms · 2026-05-11T01:42:31.561867+00:00 · methodology

Review history (2 revisions) →

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.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

  1. [1]

    ,The Situation in Logic, CSLI Publications, 1988. [10]J. Barwise and J. Etchemendy,Information, infons, and inference, in Situation Theory and Its Applications; Volume 1, Center for the Study of Language (CSLI), 1990, pp. 33–78. [11]J. Barwise, D. Gabbay, and C. Hartonas,On the logic of information flow, Logic Journal of IGPL, 3 (1995), pp. 7–49

    work page 1988

  2. [2]

    ,Information flow and the lambek calculus, CSLI Lecture Notes, 58 (1996). [13]J. Barwise and J. Perry,Situations and Attitudes, The Journal of Philosophy, 78 (1981), pp. 668–691

    work page 1996

  3. [3]

    ,Situations and Attitudes, MIT Press, Cambridge, MA, 1983. [15]J. Barwise and J. Seligman,Information Flow: The Logic of Distributed Systems, Cambridge University Press, 1997. [16]K. Bimb ´o,Introduction: From Information at Large to Semantics of Logics, in J. Michael Dunn on Information Based Logics, K. Bimb´ o, ed., Springer International Publishing, 20...

    work page 1983

  4. [4]

    Michael Dunn on Information Based Logics, Springer, 2016

    , ed.,J. Michael Dunn on Information Based Logics, Springer, 2016. [18]R. Brandom,Making It Explicit: Reasoning, Representing, and Discursive Commitment, Harvard University Press, 1994

    work page 2016

  5. [5]

    ,Articulating Reasons: An Introduction to Inferentialism, Harvard University Press, 2000. [20]O. Bueno,Computer Simulations: An Inferential Conception, The Monist, 97 (2014), pp. 378–398. [21]Y. Buzoku and D. J. Pym,Base-extension semantics for intuitionistic modal logics (extended abstract), in Automated Reasoning with Analytic Tableaux and Related Metho...

    work page 2000

  6. [6]

    ,The Problem of Relations in Inductive Logic, Philosophical Studies, 2 (1951), pp. 75–80. [25]T. Caulfield, M.-C. Ilau, and D. Pym,Engineering ecosystem models: Semantics and pragmatics, in Sim- ulation Tools and Techniques, D. Jiang and H. Song, eds., Cham, 2022, Springer International Publishing, pp. 236–258. [26]G. Chaitin,Algorithmic Information Theor...

    work page 1951

  7. [7]

    ,Situation theory and situation semantics, in Logic and the Modalities in the Twentieth Century, D. M. Gabbay and J. Woods (editors), Handbook of the History of Logic, Volume 7, North-Holland, 2006, pp. 601–664. [30]F. Dretske,The Metaphysics of Information, in Wittgenstein and the Philosophy of Information, Alois Pichler and Herbert Hrachovec, ed., De Gr...

    work page 2006

  8. [8]

    ,The Logical Basis of Metaphysics, Harvard University Press, 1991. [34]J. Dunn,The Concept of Information and the Development of Modern Logic, Zwischen traditioneller und moderner Logik: Nichtklassische Ans¨ atze, (2001), pp. 423––447. [35]T. Eckhardt and D. Pym,Base-extension semantics for modal logic, Logic Journal of the IGPL, 33 (2024), p. jzae004

    work page 1991

  9. [9]

    Arxiv, math.LO, eprint=2411.15775,https://arxiv.org/abs/2411.15775

    ,Inferentialist Public Announcement Logic: Base-extension Semantics, 2024. Arxiv, math.LO, eprint=2411.15775,https://arxiv.org/abs/2411.15775

    work page arXiv 2024

  10. [10]

    ,Base-extension Semantics for S5 Modal Logic, Logic Journal of the IGPL, (2025). [38]L. Floridi,Is semantic information meaningful data?, Philosophy and phenomenological research, 70 (2005), pp. 351–370

    work page 2025

  11. [11]

    ,The Logic of Being Informed, Logique et Analyse, 49 (2006), pp. 433–460

    work page 2006

  12. [12]

    ,The Philosophy of Information, Oxford University Press, 2011

    work page 2011

  13. [13]

    ,The Logic of Information, Oxford University Press, 2019. [42]N. Fresco and M. Michael,Information and Veridicality: Information Processing and the Bar-Hillel/Carnap Paradox, Philosophy of Science, 83 (2016), pp. 131–151. [43]G. Gentzen,Untersuchungen ¨ uber das logische Schliessen, Mathematische Zeitschrift, 39 (2034), pp. 176–210. [44]A. Gheorghiu,Proof...

    work page 2019

  14. [14]

    ,Classical Logic without Bivalance, 2026. [46]A. Gheorghiu and Y. Buzoku,Proof-theoretic semantics for classical propositional logic with assertion and denial, 2025.https://arxiv.org/abs/2503.05364. [47]A. Gheorghiu, T. Gu, and D. Pym,Inferentialist Resource Semantics, ENTICS 14727, 4 (Proceedings of MFPS XL) (2024).https://doi.org/10.46298/entics.14727. ...

    work page doi:10.46298/entics.14727 2026

  15. [15]

    ,Semantical Analysis of the Logic of Bunched Implications, Studia Logica, 111 (2023), pp. 525–571

    work page 2023

  16. [16]

    ,From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic, Studia Logica, (2025).https://doi.org/10.1007/s11225-024-10163-9

    work page doi:10.1007/s11225-024-10163-9 2025

  17. [17]

    [52]J.-Y

    ,Proof-theoretic Semantics for Second-order Logic.https://arxiv.org/abs/2508.07786, 2025. [52]J.-Y. Girard, Y. Lafont, and P. Taylor,Proofs and Types, Cambridge University Press, 1989. [53]T. Gu, A. Gheorghiu, and D. Pym,Proof-theoretic Semantics for the Logic of Bunched Implications, Studia Logica, (2025). doi.org/10.1007/s11225-025-10202-z. [54]J. Hinti...

    work page doi:10.1007/s11225-025-10202-z 2025

  18. [18]

    ,Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-theoretic Semantics, Studia Logica, 107 (2019), pp. 233–246. [67]D. Prawitz,Ideas and Results in Proof Theory, in Studies in Logic and the Foundations of Mathematics, vol. 63, Elsevier, 1971, pp. 235–307

    work page 2019

  19. [19]

    Prawitz, ed., vol

    ,Towards a Foundation of General Proof Theory, in Studies in Logic and the Foundations of Mathemat- ics, D. Prawitz, ed., vol. 74, North Holland, Amsterdam, 1973, pp. 225–250

    work page 1973

  20. [20]

    Originally published as: Dag Prawitz, Natural Deduction: A Proof-theoretical Study, Almqvist & Wiksell, 1965

    ,Natural Deduction: A Proof-theoretical Study, Dover, 2005. Originally published as: Dag Prawitz, Natural Deduction: A Proof-theoretical Study, Almqvist & Wiksell, 1965

    work page 2005

  21. [21]

    Yes” and “No

    ,Meaning Approached Via Proofs, Synthese, 148 (2006), pp. 507–524. [71]D. Pym, E. Ritter, and E. Robinson,Categorical proof-theoretic semantics, Studia Logica, (2024).https: //doi.org/10.1007/s11225-024-10101-9. [72]S. Read,Semantic Pollution and Syntactic Purity, The Review of Symbolic Logic, 8(4) (2015), pp. 1–13. [73]G. Restall,Information Flow and Rel...

    work page doi:10.1007/s11225-024-10101-9 2006

  22. [22]

    ,Base-extension semantics for intuitionistic sentential logic, Logic Journal of the IGPL, 23 (2015), pp. 719–731

    work page 2015

  23. [23]

    World Logic Day — University College London (Accessed June 2023)

    ,Atomic bases and the validity of Peirce’s law.https://sites.google.com/view/wdl-ucl2022/ schedule#h.ttn75i73elfw, 2022. World Logic Day — University College London (Accessed June 2023). [78]P. Schroeder-Heister,Validity Concepts in Proof-theoretic Semantics, Synthese, 148 (2006), pp. 525–571

    work page 2022

  24. [24]

    Pelis, ed., Filosofia, 2008

    ,Proof-Theoretic versus Model-Theoretic Consequence, in The Logica Yearbook 2007, M. Pelis, ed., Filosofia, 2008

    work page 2007

  25. [25]

    ,Proof-Theoretic Semantics, in The Stanford Encyclopedia of Philosophy, E. N. Zalta, ed., Metaphysics Research Lab, Stanford University, Spring 2018 ed., 2018. [81]J. Seligman,Situation Theory Reconsidered, Springer International Publishing, Cham, 2014, pp. 895–932. [82]C. E. Shannon,A Mathematical Theory of Communication, University of Illinois Press, 19...

    work page 2018

  26. [26]

    ,Logical Dynamics of Information and Interaction, Cambridge University Press, 2011

    work page 2011

  27. [27]

    Michael Dunn on Information Based Logic, K

    ,Tracking Information, in J. Michael Dunn on Information Based Logic, K. Bimb´ o, ed., Springer Inter- national Publishing, Cham, 2016, pp. 363–389

    work page 2016

  28. [28]

    ,Logic, Information, and Agency, CSLI Publications, The University of Chicago Press, 2025. [89]J. van Benthem and M. Martinez,The Stories of Logic and Information, Handbook of the Philosophy of Information, Elsevier Science Publishers, Amsterdam, (2008), pp. 217–280. Commentators: Israel, David and Perry, John. [90]H. van Ditmarsch, W. van der Hoek, and B...

    work page 2025