Abstract:
We propose a new type of quantum computer which is used
to prove a spectral representation for a class S of computable sets. When
S ∈ S codes the theorems of a formal system, the quantum computer
produces through measurement all theorems and proofs of the formal
system. We conjecture that the spectral representation is valid for all
computably enumerable sets. The conjecture implies that the theorems of
a general formal system, like Peano Arithmetic or ZFC, can be produced
through measurement; however, it is unlikely that the quantum computer
can produce the proofs as well, as in the particular case of S. The analysis
suggests that showing the provability of a statement is different from
writing up the proof of the statement.