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

[Abolfazl Karimi]

I wonder whether the following problem has a trivial solution
(or any research has been done in this direction):

1) Fix some natural (i.e. commonly used) predicate calculus, say natural
deduction.
2) 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.

(A trivial solution is probably to make the length of the axioms
arbitrarily large,
so that unwinding the formulas by the predicate calculus to extract an
implanted explicit contradiction
takes arbitrarily long number of steps.
But what if we put bounds on the length of the axioms and the number of
axioms?)

If the problem has solutions for every N,
how natural (i.e. similar to known mathematics) can the language and the
axioms be?

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.

Thank you for your consideration.

Abolfazl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150505/6af8ea2f/attachment-0001.html>