Pith Number

pith:OLQ2BQE5

pith:2026:OLQ2BQE55AJ7CBCHFPTB2UOB7S

not attested not anchored not stored refs resolved

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

Pablo Barenbaum

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

arxiv:2605.16157 v1 · 2026-05-15 · cs.LO

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{OLQ2BQE55AJ7CBCHFPTB2UOB7S}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

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.

C2weakest assumption

The framework assumes that the property of a datum constituting evidence for a proposition is semi-decidable, which permits the definition of verifier and generator programs that faithfully capture the epistemic content of the logic.

C3one line summary

Epistemic realizability assigns verifier and generator programs to propositions and proves soundness and completeness for minimal, second-order, and higher-order intuitionistic logic.

References

146 extracted · 146 resolved · 0 Pith anchors

[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 2018

[2] 1999.Term Rewriting and All That 1999

[3] 1984.The Lambda Calculus: Its Syntax and Semantics 1984

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

[5] 2013.Lambda Calculus with Types 2013

Receipt and verification

First computed	2026-05-20T00:01:55.413195Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

72e1a0c09de813f104472be61d51c1fca0febcae82be30e2f6eda4214cf5bf4d

Aliases

arxiv: 2605.16157 · arxiv_version: 2605.16157v1 · doi: 10.48550/arxiv.2605.16157 · pith_short_12: OLQ2BQE55AJ7 · pith_short_16: OLQ2BQE55AJ7CBCH · pith_short_8: OLQ2BQE5

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/OLQ2BQE55AJ7CBCHFPTB2UOB7S \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 72e1a0c09de813f104472be61d51c1fca0febcae82be30e2f6eda4214cf5bf4d

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "d9010e334e547c054c7aa9e489f852e36ec6b5658a8a8b85e6c9908b5f2307f7",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-15T16:38:04Z",
    "title_canon_sha256": "0ec7ed869a40f9e2027dcdc21bcdc42b77db11b4d644bdc03fe35fa5d1438dd5"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.16157",
    "kind": "arxiv",
    "version": 1
  }
}