{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiebfo73bunwywqedufbyhbnfrl53vaeokyj5h3gtg4geynv5v74py",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mnwgv3sz24e2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2606.10535v1",
  "publishedAt": "2026-06-10T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Pavel Pudlák",
    "Neil Thapen"
  ],
  "textContent": "**Authors:** Pavel Pudlák, Neil Thapen\n\nIn the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.",
  "title": "Quantified propositional calculi and narrow implicit proofs"
}