You probably mean homomorphic encryption[1].

[1] - https://en.wikipedia.org/wiki/Homomorphic_encryption

Bitcoin does have a (non-turing-complete) scripting language built in for ensuring that transactions meet arbitrary requirements. I wonder what subset of proofs could be verified in that environment.

The language doesn't support loops; in terms of flow control, you get if statements and that's it. So probably not much of interest.

I wonder which is easier to encode, natural deduction or Hilbert style.

I don't know how to do that, but I did think about a cryptocurrency in which people got paid for optimizing objective functions.

https://docs.google.com/file/d/0B3qaT-ZL6aeKOHNEQWdpZEtRYWc/...