pith. sign in

arxiv: 2605.05368 · v3 · pith:GMSS2YW3new · submitted 2026-05-06 · 🧮 math.LO · cs.AI

Towards an Inferentialist Account of Information Through Proof-theoretic Semantics

Matthew Collinson , Timo Eckhardt , David Pym This is my paper

Pith reviewed 2026-05-20 23:13 UTC · model grok-4.3

classification 🧮 math.LO cs.AI
keywords inferentialismproof-theoretic semanticsinformation theorylogicdistributed systemsinferonsemantics
0
0 comments X

The pith

Replacing truth with inferability yields a proof-theoretic primitive unit of information called the inferon

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

The paper takes a first step toward an inferentialist semantic theory of information by adapting Dretske's framework to center on inferability rather than truth. It applies proof-theoretic semantics to define an inferon as the basic building block that captures how information moves through valid reasoning steps. This setup is positioned as an alternative to model-based accounts and is meant to cover information understood as range, as correlation, and as code, with special attention to correlation. The resulting tools also support mathematical modeling of information flow inside distributed systems. A reader would care because modern systems depend on information yet still lack unified logical foundations for reasoning about it.

Core claim

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. 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. The P-tS tools we develop provide the basis for a mathematical account of distributed systems modelling. This yields a reasoning-based theory of information flow in models of分布式s

What carries the argument

The inferon, defined via proof-theoretic semantics as the primitive unit that replaces truth with inferability in the analysis of intentionality and transmissibility.

If this is right

  • It supplies a reasoning-based theory of information flow inside models of distributed systems.
  • It addresses van Benthem and Martinez's three understandings of information: range, correlation, and code.
  • It supplies a conceptually rigorous mathematical-logical account of information grounded in inference rather than models.
  • It provides tools that counterpoint the situation-theoretic view of information.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The inferon could be tested by applying the proof rules to small, explicit distributed-system diagrams to check whether correlation is preserved under composition.
  • Similar replacements of truth by inferability might be tried in other semantic frameworks that currently rely on possible worlds or situations.
  • The approach opens a route to treating information processing itself as a form of proof construction rather than state transition.

Load-bearing premise

The assumption that replacing truth with inferability in Dretske's concepts, when paired with proof-theoretic semantics, produces a coherent primitive unit that covers the main ways information is understood without creating inconsistencies or losing explanatory power.

What would settle it

A concrete distributed system example in which the inferon either produces contradictory inferences about correlation or fails to track information flow that Dretske-style analysis would predict would disprove the central claim.

Figures

Figures reproduced from arXiv: 2605.05368 by David Pym, Matthew Collinson, 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 10
Figure 10. Figure 10: Contextual support relation again the Inf-rule of [PITH_FULL_IMAGE:figures/full_fig_p025_10.png] 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

3 major / 2 minor

Summary. The paper takes first steps toward an inferentialist account of information by replacing truth with inferability in Dretske's framework, using proof-theoretic semantics (P-tS) to introduce a primitive unit called the 'inferon', counterpointing situation theory's model-theoretic view, addressing van Benthem and Martinez's three understandings of information (with focus on correlation), and sketching applications to reasoning-based modeling of information flow in distributed systems.

Significance. If the inferon receives a rigorous P-tS realization that demonstrably captures correlation while preserving transmissibility and intentionality, the work could supply a novel inference-grounded alternative to existing logical foundations for information, with potential relevance to informatics and distributed-systems analysis.

major comments (3)
  1. [conceptual analysis] Conceptual analysis: the claim that replacing truth with inferability preserves Dretske-style intentionality and transmissibility is asserted without axioms, lemmas, or derivations showing how inferability behaves under information flow; this leaves the grounding of the inferon vulnerable to the circularity noted in the stress-test.
  2. [logic] Logic section: the inferon is introduced as a mathematical-logical primitive via P-tS, yet no sequent-calculus rules, natural-deduction clauses, or cut-elimination argument is supplied that would define it or verify its coverage of information-as-correlation.
  3. [systems] Systems section: the promised reasoning-based theory of information flow in distributed systems is outlined at a high level but lacks concrete P-tS derivations or examples that would connect the inferon to actual distributed-systems modeling.
minor comments (2)
  1. The three components (conceptual analysis, logic, systems) are announced clearly in the abstract but their boundaries blur in the body; explicit section headings or a roadmap paragraph would improve readability.
  2. Terminology such as 'inferon' and 'inferentialist primitive unit' is used before any formal characterization; a brief definitional paragraph immediately after introduction would help.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive report and the recommendation of major revision. The comments correctly identify places where the manuscript would benefit from greater formal detail and concrete illustrations. We address each major comment below and indicate the revisions we intend to make.

read point-by-point responses

  1. Referee: [conceptual analysis] Conceptual analysis: the claim that replacing truth with inferability preserves Dretske-style intentionality and transmissibility is asserted without axioms, lemmas, or derivations showing how inferability behaves under information flow; this leaves the grounding of the inferon vulnerable to the circularity noted in the stress-test.

    Authors: We accept that the preservation of intentionality and transmissibility is currently supported only by conceptual argument. In the revised version we will insert a short subsection that states basic axioms governing inferability under information flow and proves two lemmas: one showing that intentionality is retained when truth is replaced by inferability, and one showing transmissibility is preserved. These additions should reduce the risk of circularity by supplying explicit inferential constraints on the inferon. revision: yes

  2. Referee: [logic] Logic section: the inferon is introduced as a mathematical-logical primitive via P-tS, yet no sequent-calculus rules, natural-deduction clauses, or cut-elimination argument is supplied that would define it or verify its coverage of information-as-correlation.

    Authors: The paper presents the inferon as a first-step primitive whose full proof-theoretic definition lies beyond the present scope. We will nevertheless add an outline of candidate sequent-calculus rules for inferons together with a brief argument that they capture the correlation aspect of information. A complete cut-elimination result will be noted as work for a follow-up paper rather than claimed here. revision: partial

  3. Referee: [systems] Systems section: the promised reasoning-based theory of information flow in distributed systems is outlined at a high level but lacks concrete P-tS derivations or examples that would connect the inferon to actual distributed-systems modeling.

    Authors: We agree that a high-level sketch is insufficient. The revised systems section will contain a worked example of a small distributed network (two agents exchanging messages under a simple protocol) together with explicit P-tS derivations that show how inferons track information flow and correlation in that setting. revision: yes

Circularity Check

0 steps flagged

Conceptual proposal without definitional or derivational reduction

full rationale

The paper performs a conceptual replacement of 'truth' by 'inferability' in Dretske's framework and sketches the use of proof-theoretic semantics to introduce the 'inferon' as a primitive unit. No equations, sequent rules, natural-deduction clauses, or explicit derivations appear in the supplied text that would reduce the inferon, any transmissibility property, or any information-as-correlation claim to the replacement itself by construction. No self-citations, fitted parameters, or uniqueness theorems are invoked as load-bearing steps. The work is explicitly framed as 'first steps' and 'towards' a theory, remaining self-contained at the level of conceptual analysis without circular reduction of outputs to inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The account rests on the assumption that inferability can substitute for truth while preserving key properties of information, plus standard background results from proof theory. No explicit free parameters or new physical entities are introduced; the inferon is a conceptual primitive.

axioms (2)
  • domain assumption Proof-theoretic semantics provides a mathematical realization of inferentialist reasoning.
    Invoked in the logic component to realize the inferentialist view.
  • ad hoc to paper Replacing truth with inferability in Dretske's framework preserves the core concepts of intentionality and transmissibility.
    Central conceptual move stated in the abstract.
invented entities (1)
  • inferon no independent evidence
    purpose: Primitive unit of information in an inferentialist semantic theory.
    Introduced as the basic building block developed via proof-theoretic semantics.

pith-pipeline@v0.9.0 · 5830 in / 1466 out tokens · 28010 ms · 2026-05-20T23:13:09.897827+00:00 · methodology

Review history (3 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.

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

28 extracted references · 28 canonical work pages

  1. [1]

    30 MATTHEW COLLINSON ∗, TIMO ECKHARDT ∗, AND DA VID PYM ∗ [10]J

    ,The Situation in Logic, CSLI Publications, 1988. 30 MATTHEW COLLINSON ∗, TIMO ECKHARDT ∗, AND DA VID PYM ∗ [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...

    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. TOW ARDS AN INFERENTIALIST ACCOUNT OF INFORMATION 31 [53]T. Gu, A. Gheorghiu, and D. Pym,Proof-theoretic Semantics for the Logic of Bunched Implications, Studia Logica, (20...

    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. 32 MATTHEW COLLINSON ∗, TIMO ECKHARDT ∗, AND...

    work page 2025