Implicit Proof Systems
summary
Defines circuit that outputs proof bits as a way to present exponentially long proofs succinctly and insists on a separate short certificate that the circuit actually encodes a valid P proof. Proves that implicit Extended Frege is captured by bounded arithmetic (V1 2 / S1 2) and that the theory proves the soundness of implicit proofs of logarithmic circuit size by encoding proofs with Gödel numbers and a binary representation trick to construct 2^n. Raises open simulation questions, suggests using reflection principles to lift simulations and shows iteration and collapse remain unresolved.
AI-written summary · about