Existentials and Zero-Knowledge Proofs
When I use "∃ x . P(x)" in typed programming (using intuitionistic logic), I must have in hand an x and a proof of P(x). This is not the case in the classical logic, in which I might have a proof of ∃ x . P(x) without knowing any details of x at all.
This idea that I know such an x exists though I have no knowledge of it reminds me of zero-knowledge proofs. Of course, the zero-knowledge proofs referenced in the Wikipedia article aren't so much proofs as they are assurances with high probability. I looked around for zero-knowledge proofs that were more proof-like, but I didn't find much. I wonder if there is any deeper connection between classical existentials and zero-knowledge proofs?
1 comment:
Interesting point. Zero knowledge proofs are currently mainly used in security settings to prove you know something but not revealing anymore about it.
You would think this would be useful to increase modularity in programming. Where providing as little information as possible between different components is beneficial.
On another weird connection to Zero knowledge proofs
http://www.wisdom.weizmann.ac.il/~naor/PUZZLES/waldo.html
The medium tech solution seems to imply there might be a connection between copying and them.
Post a Comment