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.
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.