pith. sign in

arxiv: 2605.05368 · v5 · 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-06-30 23:15 UTC · model grok-4.3

classification 🧮 math.LO cs.AI
keywords information theoryproof-theoretic semanticsinferentialismdistributed systemsDretskeinferonsituation theory
0
0 comments X

The pith

Information can be formalized as the inferon, a primitive unit defined by inferability in proof theory instead of truth in models.

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

The paper develops the first steps of an inferentialist theory of information by taking Dretske's concepts and replacing truth with inferability. It then uses proof-theoretic semantics to introduce the inferon as the basic unit and applies this to model information flow in distributed systems. The approach focuses on information as correlation and aims to supply reasoning tools for complex information ecosystems. A sympathetic reader would care because existing foundations for information remain incomplete for understanding the systems society depends on.

Core claim

By replacing truth with inferability in Dretske's analysis of intentionality and transmissibility, and realizing the change through proof-theoretic semantics, the authors take initial steps toward a mathematical-logical theory in which the inferon functions as the primitive unit of information. This proof-theoretic account stands as a counterpoint to the model-theoretic view in situation theory and supports reasoning about information flow in models of distributed systems while addressing information as range, correlation, and code.

What carries the argument

The inferon, the primitive unit of information realized through inferability in proof-theoretic semantics.

If this is right

  • Information flow in distributed systems becomes expressible through inference rules rather than model satisfaction.
  • The correlation aspect of information receives a direct formalization via proof-theoretic tools.
  • A reasoning-based account of information processing replaces truth-conditional accounts in informatics models.
  • All three components of information understanding (range, correlation, code) become addressable within one inferentialist framework.

Where Pith is reading between the lines

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

  • The inferon might supply a new primitive for analyzing information security properties stated in terms of what can be inferred rather than what holds in models.
  • The approach could be tested by encoding a simple message-passing protocol and checking whether inferon-based reasoning reproduces expected transmission behavior.
  • Connections to existing proof-theoretic work on concurrency and resource-sensitive logics become natural next steps for extending the account.

Load-bearing premise

Dretske's concepts of information can be captured and extended by replacing truth with inferability and then realized as a coherent theory in proof-theoretic semantics for distributed systems.

What would settle it

A concrete distributed-system scenario in which the inferon fails to capture a case of information transmission that Dretske's original truth-based account handles without contradiction.

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 2
Figure 2. Figure 2: Notational conventions (At) ⊩B P iff ⊢B P for closed P (∧) ⊩B ϕ1 ∧ ϕ2 iff ⊩B ϕ1 and ⊩B ϕ2 (∨) ⊩B ϕ1 ∨ ϕ2 iff for every closed P and every C ⊇ B, if ϕ1 ⊩C P and ϕ2 ⊩C P, then ⊩C P (⊃) ⊩B ϕ1 ⊃ ϕ2 iff ϕ1 ⊩B ϕ2 (Inf) for Θ ̸= ∅, Θ ⊩B ϕ iff for every C ⊇ B, if ⊩C ψ, for every ψ ∈ Θ, then ⊩C ϕ (⊥) ⊩B ⊥ iff for all closed P, ⊩B P . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . … 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

2 major / 1 minor

Summary. The manuscript proposes a three-part program for an inferentialist theory of information: (1) a conceptual replacement of Dretske's truth by inferability, (2) a proof-theoretic semantics (P-tS) realization that introduces the 'inferon' as a primitive unit and contrasts with situation theory while addressing van Benthem and Martinez's range/correlation/code trichotomy (focus on correlation), and (3) an application of the resulting tools to reasoning-based modeling of information flow in distributed systems.

Significance. A rigorously executed version of the proposed replacement and P-tS construction could supply a genuinely inference-centered alternative to model-theoretic accounts of information and a new formal handle on distributed-systems modeling. The manuscript itself, however, contains only the high-level plan and does not exhibit any of the promised derivations, definitions, or examples.

major comments (2)
  1. [Abstract] Abstract: the 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; the manuscript supplies neither a formal definition of the inferon, nor any P-tS rules or sequent calculi in which it is introduced, nor any worked example.
  2. [Abstract] Abstract: the replacement of truth by inferability is asserted to 'trace the consequences' for Dretske's intentionality and transmissibility, yet no derivation or preservation argument is given that would show the resulting notions remain non-circular or extensionally adequate.
minor comments (1)
  1. [Abstract] The manuscript would be strengthened by the addition of at least one concrete P-tS derivation or small example illustrating how an inferon encodes correlation.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback. The manuscript is framed as an initial conceptual program rather than a completed formal theory, and we respond to the specific concerns below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the 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; the manuscript supplies neither a formal definition of the inferon, nor any P-tS rules or sequent calculi in which it is introduced, nor any worked example.

    Authors: We agree that the manuscript does not contain a completed formal definition, sequent calculus, or worked example of the inferon. The 'first steps' consist in the conceptual introduction of the inferon as the inferentialist primitive realized via P-tS, together with the contrast to situation theory and the argument for addressing the correlation component of van Benthem and Martinez's trichotomy. The full technical development is explicitly left for future work. We will revise the abstract to state this scope more precisely. revision: partial

  2. Referee: [Abstract] Abstract: the replacement of truth by inferability is asserted to 'trace the consequences' for Dretske's intentionality and transmissibility, yet no derivation or preservation argument is given that would show the resulting notions remain non-circular or extensionally adequate.

    Authors: The consequences are traced at the conceptual level by showing how intentionality and transmissibility can be reformulated once truth is replaced by inferability, without circularity in the inferentialist setting. A formal preservation argument would require the completed P-tS construction, which is outside the scope of the present high-level outline. The paper's contribution at this stage is the identification of the replacement and its initial philosophical implications. revision: no

Circularity Check

0 steps flagged

No significant circularity; proposal is explicitly programmatic

full rationale

The paper presents itself as 'first steps' toward an inferentialist theory by replacing truth with inferability in Dretske's concepts and sketching an 'inferon' via proof-theoretic semantics. No load-bearing derivation, equation, or uniqueness claim is advanced that reduces to a fitted parameter, self-citation chain, or definitional renaming. The central move is a conceptual substitution whose consequences are traced at the level of metaphysics and systems modeling rather than a closed mathematical reduction. External benchmarks (situation theory, van Benthem/Martinez categories) are invoked for contrast, not as internal justification. This is self-contained conceptual groundwork, not a derivation whose soundness depends on its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The proposal introduces the new entity 'inferon' without independent evidence and rests on domain assumptions that inferentialism and proof-theoretic semantics are suitable for information; no free parameters are visible in the abstract.

axioms (2)
  • domain assumption Dretske's concepts of information (intentionality, truth, transmissibility) can be reformulated by replacing truth with inferability while preserving essential properties.
    This replacement is presented as the key move in the conceptual analysis component.
  • domain assumption Proof-theoretic semantics supplies an appropriate mathematical realization of inferentialist reasoning that can be applied to information.
    Invoked to develop the theory of the inferon and to address information-as-correlation.
invented entities (1)
  • inferon no independent evidence
    purpose: Primitive unit of information in the proposed inferentialist theory.
    Introduced as the central new concept whose mathematical-logical theory is to be developed via P-tS.

pith-pipeline@v0.9.1-grok · 5830 in / 1640 out tokens · 51218 ms · 2026-06-30T23:15:47.828055+00:00 · methodology

Review history (4 revisions) →

discussion (0)

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

Reference graph

Works this paper leans on

28 extracted references · 5 canonical work pages · 1 internal anchor

  1. [1]

    ,The Situation in Logic, CSLI Publications, 1988. [11]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. [12]J. Barwise, D. Gabbay, and C. Hartonas,On the logic of information flow, Logic Journal of IGPL, 3 (1995), pp. 7–49

    1988

  2. [2]

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

    1996

  3. [3]

    ,Situations and Attitudes, MIT Press, Cambridge, MA, 1983. [16]J. Barwise and J. Seligman,Information Flow: The Logic of Distributed Systems, Cambridge University Press, 1997. [17]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...

    1983

  4. [4]

    Michael Dunn on Information Based Logics, Springer, 2016

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

    2016

  5. [5]

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

    2000

  6. [6]

    ,The Problem of Relations in Inductive Logic, Philosophical Studies, 2 (1951), pp. 75–80. [26]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. [27]G. Chaitin,Algorithmic Information Theor...

    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. [31]F. Dretske,The Metaphysics of Information, in Wittgenstein and the Philosophy of Information, Alois Pichler and Herbert Hrachovec, ed., De Gr...

    2006

  8. [8]

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

    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). [39]L. Floridi,Is semantic information meaningful data?, Philosophy and phenomenological research, 70 (2005), pp. 351–370

    2025

  11. [11]

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

    2006

  12. [12]

    ,The Philosophy of Information, Oxford University Press, 2011

    2011

  13. [13]

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

    2019

  14. [14]

    ,Classical Logic without Bivalance, 2026. [47]A. Gheorghiu and Y. Buzoku,Proof-theoretic semantics for classical propositional logic with assertion and denial, 2025.https://arxiv.org/abs/2503.05364. [48]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 internal anchor Pith review Pith/arXiv arXiv doi:10.46298/entics.14727 2026

  15. [15]

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

    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]

    [53]J.-Y

    ,Proof-theoretic Semantics for Second-order Logic.https://arxiv.org/abs/2508.07786, 2025. [53]J.-Y. Girard, Y. Lafont, and P. Taylor,Proofs and Types, Cambridge University Press, 1989. TOW ARDS AN INFERENTIALIST ACCOUNT OF INFORMATION 31 [54]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. [68]D. Prawitz,Ideas and Results in Proof Theory, in Studies in Logic and the Foundations of Mathematics, vol. 63, Elsevier, 1971, pp. 235–307

    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

    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

    2005

  21. [21]

    Yes” and “No

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

    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). [79]P. Schroeder-Heister,Validity Concepts in Proof-theoretic Semantics, Synthese, 148 (2006), pp. 525–571

    2022

  24. [24]

    Pelis, ed., Filosofia, 2008

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

    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. [82]J. Seligman,Situation Theory Reconsidered, Springer International Publishing, Cham, 2014, pp. 895–932. [83]C. E. Shannon,A Mathematical Theory of Communication, University of Illinois Press, 19...

    2018

  26. [26]

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

    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

    2016

  28. [28]

    ,Logic, Information, and Agency, CSLI Publications, The University of Chicago Press, 2025. [90]J. van Benthem,Logic, information and agency, 2026. Forthcoming monograph, draft dated 31st May 2026. [91]J. van Benthem and M. Martinez,The Stories of Logic and Information, Handbook of the Philosophy of Information, Elsevier Science Publishers, Amsterdam, (200...

    2025