It's not the existence of the set of "smooth reals" that square to 0 without being 0 that creates the universe in which every geometric object is infinitesimally straight.
Rather, for any ring of "smooth reals" R, the set D={d in R:^2=0} allows us to construct a "dual ring" as follows. First, take the map RxR -> R^D sending a pair (a,b) of "smooth reals" to the linear function D->R given by d|->a+bd. Then induce a ring structure on RxR that would make the map into a ring homomorphism when R^D, the set of R-valued functions on D, is given the pointwise ring structure.
Explicitly, (a_1,b_1)+(a_2,b_2)=(a_1+a_2,b_1+b_2) since (a_1+b_1d)+(a_2+b_2d)=(a_1+a_2)+(b_1+b_2)d, and (a_1,b_1)(a_2,b_2)=(a_1a_2+a_1b_2+a_2b_1) since (a_1+b_1d)(a_2+b_2d)=a_1a_2+(a_1b_2+a_2b_1)d+d^2b_1b_2 and d^2=0.
Thus, we have the structure of a ring on the set of RxR, which is tradtionally denoted by R[e] where e(psilon) is a variable x assumed to square to zero, i.e. an indeterminate, so hypothetical, order 2 infinitesimal.
Now, Axiom 1 of synthetic differential geometry asserts that the map sending the ring of dual numbers to the ring of R-valued functions on D is a bijection. In other words, it restricts the domain of discourse so that, when it comes to functions on order 2 infinitesimals, we may only ever talk linear functions, and it also expands the discourse in requiring that we have distinct linear functions, one for every pair y-intercept,slope pair.
It is the second bit that forces every geometric object to admit "infinitsimally straight" approximations, because every geometric object is essentially contained in a copy of R^n (n-tuples of "smooth real numbers"), and so it is forced to have non-trivial linear functions from D.
---
One reference for the relationship to the dual numbers is the first few pages of Anders Kock's book Synthetic Differential Geometry, available from his web-site at home.imf.au.dk/kock/sdg99.pdf. Another, more readable reference, are Mike Shulman's notes available at http://home.sandiego.edu/~shulman/papers/sdg-pizza-seminar.p....
- 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.
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.
I don’t understand how it is possible to have such an axiom. Why can you not construct the function $f : x \mapsto I(x > 2)$ where $I$ is 1 for true, 0 for false. And then prove that the preimage of $(-1,0.5)$ is $(-\infty,2]$ which is not open?
In your case it is not provable that (x > 2 or x =< 2), that would require exactly the law of the excluded middle.
This is explained in one of the later slides.
Does it break down somewhere in the definition of continuity?
A list of examples of "anti-classical" axioms:
- All functions are continuous, and all sets automatically carry the "right" topology. This means, for instance, that constructing the Real numbers in the standard ways (Cauchy sequences or Dedekind cuts) also endows them with the desired topology (the Euclidean topology in this case).
- All functions are computable. This axiom is called "Church's thesis". It's nice because it shows that a lot of Computability Theory is similar to classical set theory, but with the edition of Church's thesis, and the absence of LEM.
- Some numbers in a set called the "smooth reals" square to 0... without being zero. This seems to create a universe in which every geometric object is "infinitesimally straight". I haven't fully grasped why this works. It's like the dual numbers, but somehow made all-pervasive.