[FOM] How hard can it be to detect an inconsistency?
Alasdair Urquhart
urquhart at cs.toronto.edu
Wed May 6 22:05:50 EDT 2015
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
>
>
More information about the FOM
mailing list