a modal/duality modality

Interactive/Zero-Knowledge Proofs are Analytic A Posteriori

Claim (intuitive, non-precise version). Propositions learned through interactive protocols constitute "practically" analytic a posteriori propositions, refuting Kant's claim that such propositions are impossible.

Claim (precise version). Given the cryptopractical theory of epistemology, the proposition that an element is a member of a interactive-proof-non-trivial language is analytic a posteriori.

Definition. The cryptopractical theory of epistemology (CTE) defines V-agents to be probabilistic polynomial-time Turing machines. We express all propositions as statements of the form "x ∈ L." A singular V-agent knows x ∈ L if L ∈ BPP for arbitrary x. Given the ability to communicate with an untrusted P-agent of unbounded computational power, a V-agent knows x ∈ L if L ∈ IP.
CTE is inspired by the complexity-theoretic solution to the problem of epistemic closure and logical omniscience in Scott Aaronson's Why Philosophers Should Care About Computational Complexity, here expanded to include interactive protocols.

Definition. A IP-non-trivial language is a language L ∈ (IP ∖ BPP).

Lemma. Because the proposition x ∈ L follows directly from the definition of the language, it is an analytic proposition.

Lemma. By the IP-non-triviality of L, V cannot decide L without P. In the proof of soundness of the interactive protocol (without loss of generality, that of SUMCHECK), we crucially rely on the physical, empirical assumption that P cannot inspect the random coin flips of V, as shown in the Aaronson. Thus, the knowledge that x ∈ L gained after the protocol completes is a posteriori.

Proof of Claim. The claim follows directly from these two lemmas under CTE.

Further Work. Given the standard assumption that one-way functions exist, and therefore NP ⊆ CZK, we can define a similar notion of "non-trivially zero-knowledge propositions" where x ∈ L ∈ (CZK ∖ BPP) if V-agents have access to Z-agents implementing zero-knowledge protocols.

However, the proposition x ∈ L isn't necessarily a zero-knowledge one, it just happens to be the case because the V-agent does not know a P-agent willing to go through the non-zero-knowledge protocol. Thus this notion of zero-knowledge depends on the external agents P has access to.

Can we further characterize this notion of "zero-knowledge" in epistemical terms? A possible solution could involve expressing agents as worlds in modal logic, where graph relation R corresponds to agent A being able to communicate with agent B, each world colored by the types of protocols they are willing to engage in. If there are Z-agents but no P-agents for a language L, R is not necessarily transitive, as pointed out in the Aaronson.

One additional advantage of a solution via modal logic is that we can easily accommodate statements about multi-prover interactive systems as well.

Finally, note that NIZKs also rely on physical assumptions, for example in the common random string model, so the claim doesn't only apply to standard interactive protocols.