It is not known whether widely used axiomatic systems such as ZFC are consistent and Godel has shown that it is not possible to prove that they are, at least within the system. In an inconsistent system it is possible to prove anything, so essentially it is useless. If ZFC is inconsistent, then it is very well hidden. Are there any known examples of inconsistent systems that behave consistently "at first," in the sense that the shortest path to proving both a statement and its negation is very complicated?
Consider the system (ZFC + ~PC) (that is, ZFC with one additional axiom, namely the negation of the Poincare Conjecture). Any proof of the inconsistency of this system is also a proof that ZFC implies the Poincare conjecture (and vice versa). Because we only recently learned that ZFC implies the Poincare Conjecture, we only recently learned that (ZFC + ~PC) is inconsistent. And the shortest known proof of that inconsistency (i.e. the shortest known proof of the Poincare Conjecture) is very long and complicated.
There are a lot of systems which have the property that you can prove they must be inconsistent, but actually finding the inconsistency is arbitrarily expensive.
I think you may find some such systems in cryptography. An arbitrary example would be any system containing
- A given number A (say, 246,590,906,444,061,810,100,793,941)
- A predicate "IsSimpleComposite(X)" which returns true if a number is only divisible by 1, itself, and two other numbers (minor technicality: allow both of these numbers to be the same to handle cases is IsSimpleComposite(4), which should be true because 4 = 2 * 2 ).
- IsSimpleComposite(A) is true
It would take a remarkably long time to discover that A is 613651369 * 633910099 * 633910111.
As a nastier case:
- Given a number B (say 2425967623052370772757633156976982469681)
- The same IsSimpleComposite(X)
- IsSimpleComposite(X) is true
You would have to prove that B is prime before the inconsistency appears (It happens to be prime!)
I give that example as a finite case, because finite cases are easier to follow. There are systems where the inconsistency appears as you start dealing with infinity. They are even nastier, but much harder to follow.