Pith Number

pith:ARN4Z42D

pith:2026:ARN4Z42D4YVVXJTDCFV7GUCALJ

not attested not anchored not stored refs resolved

Cut-Elimination for the Bimodal Logic GR

Hirohiko Kushida

A hypersequent calculus for the bimodal logic GR admits cut-elimination.

arxiv:2605.15732 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{ARN4Z42D4YVVXJTDCFV7GUCALJ}

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 present a hypersequent calculus for bimodal logic GR, where the two modalities represent the arithmetic provability predicates of Gödel and Rosser, respectively. We prove the cut-elimination theorem for the calculus.

C2weakest assumption

The specific hypersequent rules correctly capture the axioms and semantics of the bimodal logic GR without introducing extraneous theorems or failing to derive the intended provability statements.

C3one line summary

A hypersequent calculus for bimodal logic GR is presented and proven to satisfy cut-elimination.

References

18 extracted · 18 resolved · 0 Pith anchors

[1] S.N. Artemov and L.D. Beklemishev, PROVABILITY LOGIC, Handbook of Philosophical Logic, D. Gabbay and F. Guenthner (eds.), Volume 10, pp. 189-360, 2002, Kluwer Academic Publishers 2002

[2] Boolos,The Logic of Provability, Cambridge University Press, 1993 1993

[3] Buss, An Introduction to Proof Theory.Handbook of Proof Theory, Elsevier Science, pp 1998

[4] D. Guaspari, and R. M. Solovay, Rosser sentences,Annals of Mathematical Logic, vol. 16 (1979), pp. 81-99 1979

[5] R. Kashima, T. Kurahashi, S. Iwata, and S. Morioka, Cut-free Sequent Calculi for the Provability Logic D,The Review of Symbolic Logic.Published online 2025:1-22. doi:10.1017/S1755020325000036 42 2025 · doi:10.1017/s1755020325000036

Formal links

2 machine-checked theorem links

Receipt and verification

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

Canonical hash

045bccf343e62b5ba663116bf350405a6b8f13b793542becc276ec92a5b33a6b

Aliases

arxiv: 2605.15732 · arxiv_version: 2605.15732v1 · doi: 10.48550/arxiv.2605.15732 · pith_short_12: ARN4Z42D4YVV · pith_short_16: ARN4Z42D4YVVXJTD · pith_short_8: ARN4Z42D

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/ARN4Z42D4YVVXJTDCFV7GUCALJ \
  | 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: 045bccf343e62b5ba663116bf350405a6b8f13b793542becc276ec92a5b33a6b

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "6f19037c87f85b99b1d833317fdf89cceb72db3003dea8e2d9d318628d1ec951",
    "cross_cats_sorted": [],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-15T08:35:38Z",
    "title_canon_sha256": "01a9ed4835be30fde68a46d72c135f4046dd0b3ee249d19176d369432905972f"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15732",
    "kind": "arxiv",
    "version": 1
  }
}