Certainly it is _true_, since it is decidable and classically true, but I think that the relevant question is can you come up with a proof without actually finding a collision in SHA256? In essence, what I am asking is if there are axioms we can add in an intuitionistic system that we know to be inconsistent (but that we can't prove inconsistent without doing things that we believe are hard cryptograhically), such that the resulting system corresponds to a notion of cryptographic security.
I think this wouldn't work, because you can prove intuitionistically that every finite set is "decidable" using the following ingredients:
- An upper bound N on the size of the set.
- A surjection f:[1,N] -> S where [1,N] is the set of integers from 1 to N.
- Proof by induction that every set S where the above two ingredients can be found is decidable. The induction will be in N. This can be carried out internally in any intuitionistic system.
In the case of SHA-256, there is an upper bound N on the number of 256-bit inputs (which is equal to 2^256), and a surjection f which maps integers to corresponding bitstrings. Then the general lemma I described above is true, and you can prove that there must be a collision.
It doesn't entirely prove you wrong. (I need to do some real work). But almost certainly what you describe can't work. Some sort of induction will probably thwart what you're trying to do.
You have far more freedom in modeling intuitionistic logic than you think. :)
In this case, the point is that in a logic for cryptography, you would have a type "S" of "bit strings of arbitrary but unknown length" which is restricted in such a way that you cannot eliminate into discrete types (such as the natural numbers). In particular, there would be no way of proving "x != y" for x, y in S at all unless you assume that there was some function which established this.
One way to get a model for such a logic is to interpret types as (reflexive) graphs and functions as graph homomorphisms. The resulting category is a topos and hence gives you a model of type theory.
There is such a wealth of knowledge about building models for intuitionistic logic that it is difficult to say what can and cannot be done without a thorough literature review.
