No. If a set A is finite, its elements are enumerable, and some property P is decidable, then (\forall x \in A) P(x) \vee ~P(x) is true even intuitionistically.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.

 > 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.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....
 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.
 This makes sense, thanks
 > - 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).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?
 Technically, f is not well defined. Or rather, indicator functions aren't well defined.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.
 I’ll accept that indicator functions are not well defined in general however I don’t understand why f should be ill-defined. As I understand it, negation is still allowed in intuitionist mathematics, but you don’t get that (not not X -> X). You still get that (not not not X -> not X), and that (X and not X -> bot). Furthermore it is only a general law of the excluded middle that is not allowed and it is quite possible to prove that e.g. (x : R -> (x > 2 and not x < 2 and not x = 2) or (x <= 2 and not x > 2)).Does it break down somewhere in the definition of continuity?
 If x is a representation of a real number, how do you compute if it is above or below 2? Suppose you start computing its digits, and you get 2.0000000, you don't know if you will get a non-0 digit later if you keep computing.

Search: