[FOM] How hard can it be to detect an inconsistency?

[Dmytro Taranovsky]

On 05/05/2015 07:35 PM, Abolfazl Karimi wrote:
>  Given any natural number N,
>     design a language (of non-logical symbols) and a finite set of 
> contradictory axioms,
>     such that any proof of a contradiction is of length greater than N.

PA + there is proof of not Con(PA) that has less than N symbols
is inconsistent but the proof of inconsistency cannot be done with much 
less than N symbols.  To get a large N, one can, for example, set 
N=A(9,9) where A is Ackermann's function.
>
> If the problem has solutions for every N,
> how natural (i.e. similar to known mathematics) can the language and 
> the axioms be?

I do not know any natural examples.

>
> This problem is in response to the argument that
> since for many years we haven't yet encountered
> any contradiction in some well-developed theory (e.g. ZFC)
> then the probability of its inconsistency must be low.

The hypothesis is that a natural axiomatic system with a well-developed 
theory about what the axioms do and do not (assuming consistency) imply 
is very likely to be consistent.  Additional arguments are that
- ZFC is likely to be true.
- Con(ZFC) is implied by a variety of propositions (e.g every projective 
set is measurable).
- There is an essentially well-ordered hierarchy of large cardinal 
axioms that extend ZFC with no signs of inconsistency.

Sincerely,
Dmytro Taranovsky