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

[Alasdair Urquhart]

The new book by Pavel Pudlak "Logical Foundations of Mathematics and
Computational Complexity: A gentle introduction" has an interesting
discussion relating to this question.  The relevant passage is on
pp. 504-509.

On Tue, 5 May 2015, Abolfazl Karimi wrote:

> 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
> 
>