pith. sign in

arxiv: 2605.16157 · v1 · pith:OLQ2BQE5new · submitted 2026-05-15 · 💻 cs.LO

Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)

Pablo Barenbaum This is my paper

Pith reviewed 2026-05-19 18:42 UTC · model grok-4.3

classification 💻 cs.LO
keywords epistemic realizabilityintuitionistic logicverifier programsgenerator programssoundness and completenessminimal logicsecond-order logichigher-order logic
0
0 comments X

The pith

Epistemic realizability interpretations using verifiers and generators are sound and complete for minimal, second-order, and higher-order intuitionistic logic.

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

This paper develops epistemic realizability as a semantics for intuitionistic logics where the evidence relation is semi-decidable. Each proposition is equipped with a verifier program that checks whether a datum counts as evidence and a dual generator program that produces a generic realizer. The construction is carried through for minimal logic, second-order intuitionistic logic, and higher-order intuitionistic logic, accompanied by proofs that the interpretations are both sound and complete. A sympathetic reader would care because the approach supplies a computational account of the epistemic content of proofs in these systems.

Core claim

The paper shows that assigning to each proposition A a verifier program checking whether a datum X realizes A, together with a dual generator program behaving as a generic realizer for A, yields a semantics under which minimal logic, second-order intuitionistic logic, and higher-order intuitionistic logic are each sound and complete.

What carries the argument

The central mechanism is the verifier-generator pair for each proposition, where the verifier semi-decides membership in the evidence relation and the generator supplies a generic realizer, thereby capturing the epistemic content of the logic.

If this is right

  • Minimal logic receives a sound and complete epistemic realizability interpretation.
  • Second-order intuitionistic logic is sound and complete under the verifier-generator semantics.
  • Higher-order intuitionistic logic likewise admits a sound and complete epistemic semantics.
  • The epistemic content of these logics is captured by programs that semi-decide evidence relations.

Where Pith is reading between the lines

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

  • The same verifier-generator construction could be tested on fragments of classical logic to see where semi-decidability breaks.
  • The approach suggests a route for extracting computational content from higher-order proofs that respects epistemic constraints.
  • Similar pairs might be defined for other constructive type theories to compare their realizability strengths.

Load-bearing premise

The property that a datum constitutes evidence for a proposition is semi-decidable.

What would settle it

A concrete falsifier would be an explicit formula in higher-order intuitionistic logic together with a datum such that the associated verifier accepts or rejects the datum in a manner that violates either the soundness or the completeness of the proposed interpretation.

read the original abstract

This paper explores epistemic realizability, a form of realizability in which the property that a piece of data constitutes evidence for a logical proposition is semi-decidable. In this framework, each proposition A is assigned a verifier} program that checks whether a datum X is a realizer for A, and a dual generator program that behaves as a generic realizer for X. We propose epistemic realizability interpretations for minimal logic, second-order intuitionistic logic, and higher-order intuitionistic logic, proving that each system is sound and complete under the proposed semantics.

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

Summary. The paper proposes epistemic realizability interpretations for minimal logic, second-order intuitionistic logic, and higher-order intuitionistic logic. In this semantics, each proposition A is equipped with a verifier program that semi-decides whether a datum X realizes A and a dual generator program that produces generic realizers. The framework relies on the semi-decidability of the evidence relation to define these programs, and the manuscript claims to establish soundness and completeness for each of the three systems.

Significance. If the soundness and completeness proofs are valid, the work supplies a computationally oriented epistemic semantics that directly incorporates semi-decidability into realizability. This could strengthen links between constructive logic and verifiable evidence, especially in the higher-order case where standard realizability interpretations become more intricate. The explicit separation of verifiers and generators is a distinctive feature that may prove useful for applications in proof assistants or epistemic logic programming.

major comments (2)
  1. [Definitions of epistemic realizability for second- and higher-order logic] The central soundness and completeness claims rest on the semi-decidability assumption for the evidence relation, yet the manuscript provides no explicit argument showing that this assumption is preserved under the inductive definitions of the verifier and generator clauses for second- and higher-order quantifiers. Without such an argument, it is unclear whether the programs remain total or semi-decidable when higher-order variables are instantiated.
  2. [Completeness proof for higher-order intuitionistic logic] The completeness direction for higher-order intuitionistic logic appears to require that every valid formula possesses a realizer whose verifier accepts it; however, the paper does not address whether the generator programs can be constructed uniformly when the logic includes impredicative quantification, which risks an implicit appeal to choice principles not present in the object logic.
minor comments (2)
  1. [Section 3] Notation for the verifier and generator programs is introduced without a consolidated table; a single table listing the clauses for each connective and quantifier would improve readability.
  2. [Introduction] The abstract states that proofs exist for all three systems, but the introduction does not provide a roadmap indicating which sections contain the respective soundness and completeness arguments.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The positive assessment of the potential applications in proof assistants and epistemic logic programming is appreciated. Below we respond point by point to the major comments, indicating where clarifications or additions will appear in the revised manuscript.

read point-by-point responses

  1. Referee: [Definitions of epistemic realizability for second- and higher-order logic] The central soundness and completeness claims rest on the semi-decidability assumption for the evidence relation, yet the manuscript provides no explicit argument showing that this assumption is preserved under the inductive definitions of the verifier and generator clauses for second- and higher-order quantifiers. Without such an argument, it is unclear whether the programs remain total or semi-decidable when higher-order variables are instantiated.

    Authors: We agree that an explicit inductive argument for preservation of semi-decidability is not spelled out in the current text. The definitions ensure preservation because each verifier and generator clause is assembled from the base semi-decidable evidence relation using only effective operations (existential quantification over enumerable domains, recursive calls on subformulas, and uniform substitution of higher-order parameters). Nevertheless, to remove any ambiguity we will insert a new lemma (Lemma 4.7 in the revised numbering) that proves by induction on formula complexity that both the verifier and generator remain semi-decidable programs for all three systems, including under instantiation of second- and higher-order variables. revision: yes

  2. Referee: [Completeness proof for higher-order intuitionistic logic] The completeness direction for higher-order intuitionistic logic appears to require that every valid formula possesses a realizer whose verifier accepts it; however, the paper does not address whether the generator programs can be constructed uniformly when the logic includes impredicative quantification, which risks an implicit appeal to choice principles not present in the object logic.

    Authors: The generator for an impredicatively quantified formula is defined by a single, uniform clause that does not select particular realizers; it simply encodes the semantic condition that the generic realizer must satisfy the property for every possible instantiation. The completeness construction then extracts an explicit realizer from the assumption of validity by following the semantic clauses, without invoking any choice axiom inside the object logic. The meta-theoretic reasoning is carried out in a classical ambient theory that already contains the necessary enumerations, but no non-constructive choice is imported into the intuitionistic object theory. We will add a short clarifying paragraph after the statement of the higher-order completeness theorem to make this uniformity explicit. revision: partial

Circularity Check

0 steps flagged

No significant circularity; semantics defined independently and proved sound/complete

full rationale

The paper explicitly adopts semi-decidability as an input assumption to define verifier and generator programs for epistemic realizability. It then constructs interpretations for minimal, second-order, and higher-order intuitionistic logic and proves soundness and completeness. No load-bearing step reduces by construction to a fitted parameter, self-citation, or renamed input; the central claims rest on independent proof obligations rather than self-referential equations or ansatzes smuggled via prior work. This is a standard self-contained realizability development.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Information is limited to the abstract; the central claim rests on the semi-decidability assumption and standard background logic rather than new free parameters or invented entities with independent evidence.

axioms (1)
  • domain assumption The property that a datum constitutes evidence for a logical proposition is semi-decidable
    This assumption enables the definition of verifier and generator programs in the epistemic realizability framework.
invented entities (1)
  • Verifier and generator programs for epistemic realizers no independent evidence
    purpose: To check and produce evidence for propositions in a semi-decidable manner
    Newly introduced to extend realizability semantics to an epistemic setting.

pith-pipeline@v0.9.0 · 5610 in / 1136 out tokens · 69564 ms · 2026-05-19T18:42:51.243818+00:00 · methodology

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

146 extracted references · 146 canonical work pages

  1. [1]

    Steve Awodey, Jonas Frey, and Sam Speight. 2018. Impredicative encodings of (higher) inductive types. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. 76–85

    work page 2018

  2. [2]

    1999.Term Rewriting and All That

    Franz Baader and Tobias Nipkow. 1999.Term Rewriting and All That. Cambridge University Press. https://books.google.com.ar/books?id=N7BvXVUCQk8C

    work page 1999

  3. [3]

    1984.The Lambda Calculus: Its Syntax and Semantics

    Henk Barendregt. 1984.The Lambda Calculus: Its Syntax and Semantics. Vol. 103. Elsevier

    work page 1984

  4. [4]

    Henk Barendregt. 1991. Introduction to generalized type systems.Journal of Functional Programming1, 2 (1991), 125–154

    work page 1991

  5. [5]

    2013.Lambda Calculus with Types

    Henk Barendregt, Wil Dekkers, and Richard Statman. 2013.Lambda Calculus with Types. Cambridge University Press

    work page 2013

  6. [6]

    Corrado Böhm and Alessandro Berarducci. 1985. Automatic Synthesis of Typed Lambda-Programs on Term Algebras.Theor. Comput. Sci.39 (1985), 135–154

    work page 1985

  7. [7]

    Steven Bronsveld, Herman Geuvers, and Niels van der Weide. 2025. Impredicative Encodings of Inductive and Coinductive Types. In10th International Conference on Formal Structures for Computation and Deduction

    work page 2025

  8. [8]

    Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-idempotent intersection types for the Lambda-Calculus.Log. J. IGPL25, 4 (2017), 431–464

    work page 2017

  9. [9]

    2007.Sémantiques de la logique linéaire et temps de cal- cul

    Daniel de Carvalho. 2007.Sémantiques de la logique linéaire et temps de cal- cul. Ph. D. Dissertation. Ecole Doctorale Physique et Sciences de la Matière (Marseille)

    work page 2007

  10. [10]

    Alonzo Church. 1940. A Formulation of the Simple Theory of Types.The Journal of Symbolic Logic8, 2 (1940), 56–68. https://books.google.com.ar/books?id=hP_ sGwAACAAJ

    work page 1940

  11. [11]

    Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the 𝜆-calculus.Notre Dame J. Formal Log.21, 4 (1980), 685–693

    work page 1980

  12. [12]

    Pierre-Louis Curien and Hugo Herbelin. 2000. The Duality of Computation

    work page 2000

  13. [13]

    Rowan Davies and Frank Pfenning. 2001. A modal analysis of staged computation. Journal of the ACM (JACM)48, 3 (2001), 555–604

    work page 2001

  14. [14]

    Bruno Miguel Antunes Dinis and Étienne Miquey. 2021. Realizability with Stateful Computations for Nonstandard Analysis. InAnnual Conference for Computer Science Logic. https://api.semanticscholar.org/CorpusID:228902453

    work page 2021

  15. [15]

    1991.The Logical Basis of Metaphysics

    Michael Dummett. 1991.The Logical Basis of Metaphysics. Harvard University Press, Cambridge, MA

    work page 1991

  16. [16]

    Claudia Faggian. 2002. Travelling on designs: ludics dynamics. InInternational Workshop on Computer Science Logic. Springer, 427–441

    work page 2002

  17. [17]

    Claudia Faggian and Michele Basaldella. 2011. Ludics with repetitions (exponen- tials, interactive types and completeness).Logical Methods in Computer Science7 (2011)

    work page 2011

  18. [18]

    Laura Fontanella, Guillaume Geoffroy, and Richard Matthews. 2024. Realizability Models for Large Cardinals. In32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 288), Aniello Murano and Alexandra Silva (Eds.). Schloss Dagstuhl – Leibniz- Zentrum für Informatik, Dagstuhl, Germa...

    work page doi:10.4230/lipics.csl 2024

  19. [19]

    Michał J. Gajda. 2024. Consistent Ultrafinitist Logic. In29th International Con- ference on Types for Proofs and Programs (TYPES 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 303), Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Infor- matik, Dagstuhl, Germany, 5:1–5:20. doi...

    work page doi:10.4230/lipics.types.2023.5 2024

  20. [20]

    Candidats de Reductibilité

    Jean H. Gallier. 1990. On Girard’s “Candidats de Reductibilité”. InLogic and Computer Science, Piergiorgio Odifreddi (Ed.). APIC Studies in Data Processing, Vol. 31. Academic Press, London, UK, 123–203

    work page 1990

  21. [21]

    Philippa Gardner. 1994. Discovering needed reductions using type theory. In Theoretical Aspects of Computer Software. Springer, 555–574

    work page 1994

  22. [22]

    1972.Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur

    Jean-Yves Girard. 1972.Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis. Université Paris 7

    work page 1972

  23. [23]

    Jean-Yves Girard. 2001. Locus Solum: From linear logic to ludics.Mathematical Structures in Computer Science11, 3 (2001), 301–506

    work page 2001

  24. [24]

    2011.The Blind Spot: Lectures on Logic

    Jean-Yves Girard. 2011.The Blind Spot: Lectures on Logic. European Mathematical Society, Zürich, Switzerland. doi:10.4171/088

    work page doi:10.4171/088 2011

  25. [25]

    1989.Proofs and Types

    Jean-Yves Girard, Yves Lafont, and Paul Taylor. 1989.Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Vol. 7. Cambridge University Press, Cambridge, UK

    work page 1989

  26. [26]

    Mauricio Guillermo and Alexandre Miquel. 2016. Specifying Peirce’s law in classical realizability.Mathematical Structures in Computer Science26, 7 (2016), 1269–1303

    work page 2016

  27. [27]

    Joel David Hamkins. 2025. A potentialist conception of ultrafinitism. arXiv:2512.06564 [math.LO] https://arxiv.org/abs/2512.06564

    work page arXiv 2025

  28. [28]

    Delia Kesner. 2016. Reasoning About Call-by-need by Means of Types. InFoun- dations of Software Science and Computation Structures - 19th International Con- ference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Compute...

    work page doi:10.1007/978-3-662-49630-5_25 2016

  29. [29]

    Stephen Cole Kleene. 1945. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic10, 4 (1945), 109–124. doi:10.2307/2269016

    work page doi:10.2307/2269016 1945

  30. [30]

    Georg Kreisel. 1962. Foundations of Intuitionistic Logic. InLogic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress, E. Nagel, P. Suppes, and A. Tarski (Eds.). Stanford University Press, Stanford, CA, 198–210

    work page 1962

  31. [31]

    Jean-Louis Krivine. 2009. Realizability in classical logic.Panoramas et synthèses 27 (2009), 197–229

    work page 2009

  32. [32]

    Mannucci

    Mirco A. Mannucci. 2023. Model Theory of Ultrafinitism II: Deconstructing the Term Model (First Draft). arXiv:2311.17931 [math.LO] https://arxiv.org/abs/2311. 17931

    work page arXiv 2023

  33. [33]

    1984.Intuitionistic Type Theory

    Per Martin-Löf. 1984.Intuitionistic Type Theory. Studies in Proof Theory, Vol. 1. Bibliopolis, Naples. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980

    work page 1984

  34. [34]

    Alexandre Miquel. 2011. Existential witness extraction in classical realizability and via a negative translation.Logical Methods in Computer Science7 (2011)

    work page 2011

  35. [35]

    Étienne Miquey and Hugo Herbelin. 2018. Realizability Interpretation and Nor- malization of Typed Call-by-Need\lambda-calculus with Control.. InFoSSaCS. 276–292

    work page 2018

  36. [36]

    1986.Predicative Arithmetic

    Edward Nelson. 1986.Predicative Arithmetic. Princeton University Press, Prince- ton, N.J

    work page 1986

  37. [37]

    Edward Nelson. n.d.. Understanding Intuitionism. (n.d.). https://web.math. princeton.edu/~nelson/papers/int.pdf Available at https://web.math.princeton. edu/~nelson/papers/int.pdf

    work page

  38. [38]

    Tobias Nipkow. 1991. Higher-order critical pairs. InProceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 342–343

    work page 1991

  39. [39]

    Michel Parigot. 1992. 𝜆𝜇-Calculus: An algorithmic interpretation of classical natu- ral deduction. InLogic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 190–201

    work page 1992

  40. [40]

    Rohit Parikh. 1971. Existence and feasibility in arithmetic.Journal of Symbolic Logic36 (1971), 494 – 508. https://api.semanticscholar.org/CorpusID:6467866

    work page 1971

  41. [41]

    Daniele Pautasso and Simona Ronchi Della Rocca. 2023. A Quantitative Version of Simple Types. In8th International Conference on Formal Structures for Compu- tation and Deduction (FSCD 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 260), Marco Gaboardi and Femke van Raamsdonk (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik...

    work page doi:10.4230/lipics.fscd.2023.29 2023

  42. [42]

    Frank Pfenning and Rowan Davies. 2001. A judgmental reconstruction of modal logic.Mathematical structures in computer science11, 4 (2001), 511–540

    work page 2001

  43. [43]

    Dag Prawitz. 1971. Ideas and results in proof theory.Proceedings of the Second Scandinavian Logic Symposium63 (1971), 235–307

    work page 1971

  44. [44]

    John C Reynolds. 1974. Towards a theory of type structure. InProgramming Symposium. Springer, 408–425

    work page 1974

  45. [45]

    Reynolds

    John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83. North-Holland, 513–523

    work page 1983

  46. [46]

    Vladimir Yu. Sazonov. 1995. On feasible numbers. InLogic and Computational Complexity, Daniel Leivant (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 30–51

    work page 1995

  47. [47]

    Dana S. Scott. 1980. Relating Theories of the Lambda-calculus. InTo H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Roger Hindley and Jonathan P. Seldin (Eds.). Academic Press, London, 403–450

    work page 1980

  48. [48]

    Siek and Walid Taha

    Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. InProceedings of the 2006 Scheme and Functional Programming Workshop. 81–92. http://scheme2006.cs.uchicago.edu/13-siek.pdf

    work page 2006

  49. [49]

    2006.Lectures on the Curry-Howard isomorphism

    Morten Heine Sørensen and Pawel Urzyczyn. 2006.Lectures on the Curry-Howard isomorphism. Vol. 149. Elsevier

    work page 2006

  50. [50]

    2003.Term Rewriting Systems

    Terese. 2003.Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55. Cambridge University Press

    work page 2003

  51. [51]

    Kazushige Terui. 2011. Computational ludics.Theoretical Computer Science412, 20 (2011), 2048–2071

    work page 2011

  52. [52]

    A. S. Troelstra and D. van Dalen. 1988.Constructivism in Mathematics: An Introduction. Studies in Logic and the Foundations of Mathematics, Vol. 1. North- Holland, Amsterdam

    work page 1988

  53. [53]

    A. S. Yessenin-Volpin. 1975. The Ultra-Intuitionistic Criticism and the Antitradi- tional Program for Foundations of Mathematics.Journal of Symbolic Logic40, 1 (1975), 95–97. doi:10.2307/2272294

    work page doi:10.2307/2272294 1975

  54. [54]

    Doron Zeilberger. 2004. “Real” Analysis is a Degenerate Case of Discrete Analysis. InNew Progress in Difference Equations (Proceedings of the ICDEA 2001), Bernd Aulbach, Saber Elaydi, and Gerry Ladas (Eds.). Taylor & Francis, London, 1–4

    work page 2004

  55. [55]

    Noam Zeilberger. 2008. On the unity of duality.Annals of pure and applied logic 153, 1-3 (2008), 66–96. Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic P. Barenbaum A Minimal Logic — Properties of𝜆 → 𝔪 A.1 Minimal Logic: Determinism of Weak Head Reduction (Thm. 3.5) To show that weak head reduction in 𝜆→ 𝔪 is deterministic,i.e.that ...

    work page 2008

  56. [56]

    There exist 𝑛1, 𝑛2 ≥ 0such that 𝑀→ 𝑛1 𝑤 ★ and W[𝑁] → 𝑛2 𝑤 ★ and𝑛=1+𝑛 1 +𝑛 2. Proof. (1 =⇒ 2) Suppose that W[𝑀?𝑁] → 𝑛 𝑤 ★. We proceed by induction on 𝑛. The reduction cannot be empty, so 𝑛> 0,i.e. 𝑛= 1 +𝑚 for some 𝑚≥ 0, and the reduction must be of the form W[𝑀?𝑁] → 𝑤 𝑃→ 𝑚 𝑤 ★. We consider two subcases, depending on whether the redex contracted in the firs...

    work page

  57. [57]

    Hence 𝑀=★→ 0 𝑤 ★ and W[𝑁] → 𝑚 𝑤 ★, and taking 𝑛1 := 0and 𝑛2 :=𝑚we have that𝑛=1+𝑚=1+𝑛 1 +𝑛 2, as required

    If the contracted redex is 𝑀?𝑁 , then 𝑀=★ , and the re- duction is of the form W[★?𝑁] → 𝑤 W[𝑁] → 𝑚 𝑤 ★. Hence 𝑀=★→ 0 𝑤 ★ and W[𝑁] → 𝑚 𝑤 ★, and taking 𝑛1 := 0and 𝑛2 :=𝑚we have that𝑛=1+𝑚=1+𝑛 1 +𝑛 2, as required

    work page

  58. [58]

    If the contracted redex is internal to 𝑀, then the reduc- tion is of the form W[𝑀?𝑁] → 𝑤 W[𝑀 ′?𝑁] → 𝑚 𝑤 ★ where 𝑀→ 𝑤 𝑀 ′. By i.h. there exist 𝑚1, 𝑚2 such that 𝑀 ′ →𝑚1 𝑤 ★ and W[𝑁] → 𝑚2 𝑤 ★ and 𝑚= 1 +𝑚 1 +𝑚 2. Taking 𝑛1 := 1 +𝑚 1 and 𝑛2 :=𝑚 2, we have that 𝑀→ 𝑤 𝑀 ′ ↠𝑚1 𝑤 ★ where 𝑛=1+𝑚=2+𝑚 1 +𝑚 2 =1+𝑛 1 +𝑛 2. (2 =⇒ 1) Suppose that 𝑀→ 𝑛1 𝑤 ★ and W[𝑁] → 𝑛2 𝑤 ...

    work page

  59. [59]

    There exist W0, 𝑅0 such that 𝑀=W 0 [𝑅0] where WΓ 0 =W and 𝑅Γ 0 =𝑅and𝑅 0 is a redex

    work page

  60. [60]

    There exist W0, 𝑥, 𝑁 , 𝑦, 𝑃 such that 𝑀=W 0 [𝑥 𝑁] where WΓ 0 =W and𝑥 Γ =𝜆𝑦. 𝑃

    work page

  61. [61]

    There exist W0, 𝑥, 𝑁 such that 𝑀=W 0 [𝑥?𝑁] where WΓ 0 =W and 𝑥 Γ =★

    work page

  62. [62]

    Proof.Straightforward by induction on𝑀.□ Lemma A.6 (Universality).Let Γ⊨𝜎

    There exist W0, 𝑥 such that 𝑀=W 0 [⟨a⟩𝑥] where WΓ 0 =W and 𝑥 Γ =✠ a. Proof.Straightforward by induction on𝑀.□ Lemma A.6 (Universality).Let Γ⊨𝜎 . If 𝑀 Γ ↠★ then 𝑀𝜎 ↠★ . Proof. Suppose that Γ⊨𝜎 . By Thm. 3.7, it suffices to show that 𝑀 Γ ↠𝑤 ★ implies 𝑀𝜎 ↠𝑤 ★. Suppose that 𝑀 Γ ↠𝑤 ★. Let us write |𝐴| for the size of the type 𝐴, and |Γ| for the maximum size of...

    work page

  63. [63]

    First note that 𝑅Γ →𝑤 𝑆 Γ is also a root reduc- tion step by Thm

    If 𝑀=W[𝑅] where 𝑅 is a redex: consider the root reduction step 𝑅→ 𝑤 𝑆. First note that 𝑅Γ →𝑤 𝑆 Γ is also a root reduc- tion step by Thm. A.3. Since head reduction is deterministic Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic P. Barenbaum (Thm. A.3), the input reduction sequence must be of the form: 𝑀 Γ =W Γ [𝑅Γ]by Thm. A.4 →𝑤 WΓ ...

    work page

  64. [64]

    If𝑀=W[𝑥 𝑁]where𝑥 Γ is an abstraction,i.e.𝑥 Γ =𝜆𝑦. 𝑃. First, we claim that 𝑥 : 𝐴⇒𝐵∈Γ for certain types 𝐴, 𝐵. Indeed, if 𝑥∉dom(Γ) then 𝑥 Γ =𝑥 is not an abstraction; so we must have that 𝑥∈dom(Γ) . Moreover if 𝑥 :a ∈Γ , i.e.if it is assigned an atomic type, then 𝑥 Γ =✠ a is not an abstraction; so we must have that 𝑥 occurs in Γ with a type which is not an at...

    work page

  65. [65]

    Indeed, since 𝑥 Γ =★ , we know that 𝑥∈dom(Γ) , but if 𝑥 : 𝐴∈dom(Γ) then 𝑥 Γ =✠ 𝐴 ≠★ , contradicting the fact that𝑥 Γ =★

    If 𝑀=W[𝑥?𝑁] where 𝑥 Γ =★ : we claim that this case is impossible. Indeed, since 𝑥 Γ =★ , we know that 𝑥∈dom(Γ) , but if 𝑥 : 𝐴∈dom(Γ) then 𝑥 Γ =✠ 𝐴 ≠★ , contradicting the fact that𝑥 Γ =★

    work page

  66. [66]

    Since head reduction is deterministic (Thm

    If 𝑀=W[⟨ a⟩𝑥] where 𝑥 Γ =✠ a: then it must be the case that 𝑥 :a ∈Γ . Since head reduction is deterministic (Thm. A.3), the input reduction sequence must be of the form: 𝑀 Γ =W[⟨a⟩𝑥] Γ =W Γ [⟨a⟩𝑥 Γ]by Thm. A.4 =W Γ [⟨a⟩✠ a]since𝑥:a∈Γ →𝑤 WΓ [★] =W[★] Γ by Thm. A.4 →𝑚 𝑤 ★ Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic P. Barenbaum No...

    work page

  67. [67]

    Then the application 𝑀 ↓ 𝑥 𝛽 -reduces to a 𝛽-normal form 𝑁 ↓ in at most one step, and |𝑀 ↓ |Γ⊢𝐴⇒𝐵 ≥ |𝑁 ↓ |Γ,𝑥:𝐴⊢𝐵

    Let 𝑀 ↓ be a normal term. Then the application 𝑀 ↓ 𝑥 𝛽 -reduces to a 𝛽-normal form 𝑁 ↓ in at most one step, and |𝑀 ↓ |Γ⊢𝐴⇒𝐵 ≥ |𝑁 ↓ |Γ,𝑥:𝐴⊢𝐵

    work page

  68. [68]

    Then 𝑀 ↓ 𝑥1

    Let 𝑀 ↓ be a normal term. Then 𝑀 ↓ 𝑥1 . . . 𝑥𝑛 𝛽-reduces to a 𝛽-normal form 𝑁 in at most 𝑛 steps, and |𝑀 ↓ |Γ⊢𝐴1⇒...𝐴𝑛 ⇒𝐵 ≥ |𝑁 ↓ |Γ,𝑥1:𝐴1,...,𝑥𝑛:𝐴𝑛 ⊢𝐵. Proof. The second item is immediate by induction on 𝑛, re- sorting to the first item in each step. To show the first item, pro- ceed by induction on the shape of the normal term 𝑀 ↓ according to Thm. 3.12....

    work page

  69. [69]

    𝐵? 𝑘 ✠b)𝑁 Δ 1

    If for every index1 ≤𝑖≤𝑚 we have that ⟨𝐵𝑖 ⟩𝑁 Δ 𝑖 ↠★ , then: ⟨a⟩((𝐵 ? 1 . . . 𝐵? 𝑘 ✠b)𝑁 Δ 1 . . . 𝑁 Δ 𝑚)↠⟨ a⟩(✠ b 𝑁 Δ 𝑘+1 . . . 𝑁 Δ 𝑚). The reducts of ✠b 𝑁 Δ 𝑘+1 . . . 𝑁 Δ 𝑚 always have ✠b at the head and exactly 𝑚−𝑘> 0arguments, so the argument of ⟨a⟩(·) does not reduce to✠ a, and the metaterm does not reduce to★

    work page

  70. [70]

    Then: ⟨a⟩((𝐵 ? 1

    Otherwise, let1 ≤𝑖≤𝑚 be the least index such that ⟨𝐵𝑖 ⟩𝑁 Δ 𝑖 does not reduce to★. Then: ⟨a⟩((𝐵 ? 1 . . . 𝐵? 𝑘 ✠b)𝑁 Δ 1 . . . 𝑁 Δ 𝑚) ↠⟨a⟩((⟨𝐵 𝑖 ⟩𝑁 Δ 𝑖 ?(𝐵 ? 𝑖+1 . . . 𝐵? 𝑘 ✠b))𝑁 Δ 𝑖+1 . . . 𝑁 Δ 𝑚) Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic P. Barenbaum Since ⟨𝐵𝑖 ⟩𝑁 Δ 𝑖 does not reduce to★, the unit eliminator(⟨𝐵 𝑖 ⟩𝑁 Δ 𝑖 ?(·)) d...

    work page

  71. [71]

    Hence 𝑁1 =𝜆𝑥

    If both steps are at the root: note that there is only one rewriting rule in 𝜆F 𝔪 that involves an application at the root. Hence 𝑁1 =𝜆𝑥 . 𝑁 ′ 1 and the two steps are of the form (𝜆𝑥 . 𝑁′ 1)𝑃 1 →𝑤 𝑁 ′ 1 {𝑥 :=𝑃 1}, so 𝑀2 =𝑀 3 =𝑁 ′ 1 {𝑥 :=𝑃 1} and we are done

    work page

  72. [72]

    Similarly, the step 𝑀1 →𝑤 𝑀2 is of the form 𝑁1 𝑃1 →𝑤 𝑁3 𝑃1 with 𝑁1 →𝑤 𝑁3

    If both steps are internal to 𝑁1: then the step 𝑀1 →𝑤 𝑀2 is of the form 𝑁1 𝑃1 →𝑤 𝑁2 𝑃1 with 𝑁1 →𝑤 𝑁2. Similarly, the step 𝑀1 →𝑤 𝑀2 is of the form 𝑁1 𝑃1 →𝑤 𝑁3 𝑃1 with 𝑁1 →𝑤 𝑁3. By i.h., there exists a term 𝑁4 such that 𝑁2 →= 𝑤 𝑁4 and 𝑁3 →= 𝑤 𝑁4. Taking 𝑀4 :=𝑁 4 𝑃1 we have that 𝑀2 = 𝑁2 𝑃1 →𝑤 𝑁4 𝑃1 =𝑀 4 and𝑀 3 =𝑁 3 𝑃1 →𝑤 𝑁3 𝑃1 =𝑀 4

    work page

  73. [73]

    Without loss of generality, sup- pose that the first step 𝑀1 →𝑤 𝑀2 is at the root and the second step 𝑀1 →𝑤 𝑀3 is internal to 𝑁1

    If one step is at the rule, and one internal to 𝑁1: we claim that this case is impossible. Without loss of generality, sup- pose that the first step 𝑀1 →𝑤 𝑀2 is at the root and the second step 𝑀1 →𝑤 𝑀3 is internal to 𝑁1. Then 𝑁1 =𝜆𝑥 . 𝑁 ′ 1 and the first step is of the form 𝑀1 =(𝜆𝑥 . 𝑁 ′ 1)𝑃 1 →𝑤 𝑁 ′ 1 {𝑥 :=𝑃 1}=𝑀 2. Then the second step is of the form 𝑀1...

    work page

  74. [74]

    Type-variable (𝐴=𝑎 ): Then the only way to reduce 𝑀1 is with a reduction internal to 𝑁1 and we conclude resorting to the i.h

    work page

  75. [75]

    If 𝑁1 =✠ a, then 𝑀1 reduces at the root, so 𝑀1 =⟨ a⟩✠a →𝑤 ★ and this is the only way to reduce 𝑀1

    Eigenvariable (𝐴= a): Then there are two cases. If 𝑁1 =✠ a, then 𝑀1 reduces at the root, so 𝑀1 =⟨ a⟩✠a →𝑤 ★ and this is the only way to reduce 𝑀1. Otherwise 𝑁1 ≠✠ a, so both steps 𝑀1 →𝑀 2 and 𝑀1 →𝑀 3 must be internal to 𝑁1 and we conclude by resorting to the i.h

    work page

  76. [76]

    Without loss of generality, suppose that 𝑀1 →𝑤 𝑀2 is at the root and 𝑀1 →𝑤 𝑀3 is internal to 𝑁1

    Implication (𝐴=(𝐵⇒𝐶) ): If both steps are at the root or both are internal to 𝑁1, it is easy to conclude, similarly as in the case of the term-abstraction. Without loss of generality, suppose that 𝑀1 →𝑤 𝑀2 is at the root and 𝑀1 →𝑤 𝑀3 is internal to 𝑁1. Then the situation is the following, where 𝑁1 →𝑤 𝑁2: 𝑀1 =⟨𝐴⇒𝐵⟩𝑁 1 // ⟨𝐵⟩(𝑁 1 ✠𝐴)=𝑀 2 𝑀3 =⟨𝐴⇒𝐵⟩𝑁 2 // ⟨𝐵⟩...

    work page

  77. [77]

    𝐵) ): If both steps are at the root or both are internal to 𝑁1, it is easy to conclude, similarly as in the case of the term-abstraction

    Universal quantification (𝐴=(∀𝑎. 𝐵) ): If both steps are at the root or both are internal to 𝑁1, it is easy to conclude, similarly as in the case of the term-abstraction. Without loss of generality, suppose that 𝑀1 →𝑤 𝑀2 is at the root and 𝑀1 →𝑤 𝑀3 is internal to 𝑁1. Then the situation is the Verifiers and Generators: Epistemic Semantics for Intuitionisti...

    work page

  78. [78]

    𝑀▷𝑁 then 𝑁 is of the form 𝑁=𝜆𝑥

    If 𝜆𝑥 . 𝑀▷𝑁 then 𝑁 is of the form 𝑁=𝜆𝑥 . 𝑀 ′ and 𝑀▷𝑀 ′

    work page

  79. [79]

    𝑀▷𝑁 then 𝑁 is of the form 𝑁=Λ𝑎

    If Λ𝑎. 𝑀▷𝑁 then 𝑁 is of the form 𝑁=Λ𝑎. 𝑀 ′ and 𝑀▷𝑀 ′

    work page

  80. [80]

    Lemma B.4 (Reflexivity).𝑀▷𝑀 Proof.Straightforward by induction on𝑀.□ Lemma B.5 (Substitution).If 𝑀▷𝑀 ′ and 𝑁▷𝑁 ′ then 𝑀{𝑥 := 𝑁}▷𝑀 ′{𝑥:=𝑁 ′}

    If✠ a ▷𝑁then𝑁=✠ a. Lemma B.4 (Reflexivity).𝑀▷𝑀 Proof.Straightforward by induction on𝑀.□ Lemma B.5 (Substitution).If 𝑀▷𝑀 ′ and 𝑁▷𝑁 ′ then 𝑀{𝑥 := 𝑁}▷𝑀 ′{𝑥:=𝑁 ′}. Proof. Straightforward by induction on the derivation of 𝑀▷ 𝑀 ′, resorting to reflexivity (Thm. B.4) in thevarcase.□ Lemma B.6 (Type substitution).If 𝑀▷𝑀 ′ then 𝑀{𝑎 :=𝐴}▷ 𝑀 ′{𝑎:=𝐴}. Proof. Straight...

    work page

Showing first 80 references.