6 ms·

> we can assume powerful axioms that would classically be inconsistent Where could I find some explicit examples of this being useful? One idea I had is that

> we can assume powerful axioms that would classically be inconsistent Where could I find some explicit examples of this being useful? One idea I had is that this might actually be very useful for proving things about cryptography. Generally, if you want to formally prove something is cryptographically sound, you can only do so in terms of the asymptotics of families of functions, rather than proving anything specific regarding, say, SHA256. But if you could prove constructively a statement like (an adversary can break program P) -> (exists x,y: x != y and SHA256(x)=SHA256(y)) it seems that would serve as a proof that P is secure. Statements of this form are trivially provable classically since (exists x,y: x != y and SHA256(x)=SHA256(y)) can be proven on its own by the pigeonhole principle, regardless of the correctness of P, but it seems that in order to prove this constructively you would actually have to find a collision in SHA256.

contravariant 8y ago
I don't think you'll find much use for it when reasoning about a specific computable hash function because there's e.g. no clear distinction between using the pingeonhole principle and using the properties of the hash function itself. You could however reason about a 'generic' hash function and show that a particular program can only be broken if someone can find a hash collision. That doesn't really require constructionist reasoning though.
man-and-laptop 8y ago
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.
- dooglius 8y ago
  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.
  - man-and-laptop 8y ago
    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.
    - dooglius 8y ago
      This makes sense, thanks
    - fmap 8y ago
      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.
js8 8y ago
I would like to point out that we don't have even classical way of proving something to be cryptographically sound, since we don't know if really P!=NP. Perhaps there is a constructive proof of P!=NP and this will actually let you prove cryptographic strength of something constructively. And if you are already taking P!=NP as an axiom, what difference it makes that constructivism takes out just another axiom that you assume to be true?
vladsotirov 8y ago
One "application" (in quotes because honestly for all the fanfare I haven't come across something that was worked out to be usable by non-specialists) is automatic differentiation, see http://blog.sigfpe.com/2006/09/practical-synthetic-differential.html http://blog.sigfpe.com/2006/09/practical-synthetic-different... Generally speaking, the ability to extended intuionistic mathematics by new axioms that are classically inconsistent is a bit of a misnomer. The real power is that these "axioms" allow you to easily and immediately specialize the generic language of intuionistic mathematics into a domain-specific language for various areas. So that 1. adding the continuity axiom gives you a domain-specific language which can only describe continuous functions and no others 2. adding the differentiation axiom gives you a domain-specific language called synthetic differential geometry in which you can only talk about differentiable functions 3. adding the computability axiom gives you a domain-specific language in which you can only talk about computable functions. 4. adding the law of the excluded middle gives you the domain-specific language of classical mathematics. Now, each of the first three can also be interpreted within classical mathematics (which is how we know the extensions are consistent with classical mathematics), but that's analogous to writing an interpreter in C versus merely adding new syntax to an existing language (e.g. how DSLs can be implemented in LISP).

contravariant 8y ago

I don't think you'll find much use for it when reasoning about a specific computable hash function because there's e.g. no clear distinction between using the pingeonhole principle and using the properties of the hash function itself. You could however reason about a 'generic' hash function and show that a particular program can only be broken if someone can find a hash collision. That doesn't really require constructionist reasoning though.

man-and-laptop 8y ago

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.

dooglius 8y ago
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.
- man-and-laptop 8y ago
  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.
  - dooglius 8y ago
    This makes sense, thanks
  - fmap 8y ago
    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.

js8 8y ago

I would like to point out that we don't have even classical way of proving something to be cryptographically sound, since we don't know if really P!=NP. Perhaps there is a constructive proof of P!=NP and this will actually let you prove cryptographic strength of something constructively. And if you are already taking P!=NP as an axiom, what difference it makes that constructivism takes out just another axiom that you assume to be true?

vladsotirov 8y ago

One "application" (in quotes because honestly for all the fanfare I haven't come across something that was worked out to be usable by non-specialists) is automatic differentiation, see http://blog.sigfpe.com/2006/09/practical-synthetic-differential.html http://blog.sigfpe.com/2006/09/practical-synthetic-different... Generally speaking, the ability to extended intuionistic mathematics by new axioms that are classically inconsistent is a bit of a misnomer. The real power is that these "axioms" allow you to easily and immediately specialize the generic language of intuionistic mathematics into a domain-specific language for various areas. So that 1. adding the continuity axiom gives you a domain-specific language which can only describe continuous functions and no others 2. adding the differentiation axiom gives you a domain-specific language called synthetic differential geometry in which you can only talk about differentiable functions 3. adding the computability axiom gives you a domain-specific language in which you can only talk about computable functions. 4. adding the law of the excluded middle gives you the domain-specific language of classical mathematics. Now, each of the first three can also be interpreted within classical mathematics (which is how we know the extensions are consistent with classical mathematics), but that's analogous to writing an interpreter in C versus merely adding new syntax to an existing language (e.g. how DSLs can be implemented in LISP).