Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Is there an axiomatic theory whose domain of discourse can be interpreted as a collection of first order theories, which has a predicate $\mathrm{Con}$ such that $\mathrm{Con}(T)$ can be interpreted as saying that the theory $T$ is consistent?

More generally, is there an axiomatic theory of consistency?

Alternatively, is there an axiomatic theory of provability, with relation $\vdash$ such that $T \vdash t$ can be read `$T$ proves $t$.' That way, $\mathrm{Con}(T)$ can be defined as shorthand for $\neg(T \vdash \bot)$. In either case, I'd be interested in a reference recommendation.

EDIT: Yet another approach might be a theory with a (deductive) closure operator $D$ together with an extensional relation $\in$. Then $\bot \notin D(T)$ could be defined as saying $\mathrm{Con}(T)$.

share|improve this question
add comment

1 Answer

up vote 2 down vote accepted

There is a field called Provability Logic. Its basic (and difficult) result is that, in a suitable logic, Loeb's theorem captures all the reasoning that Peano arithmetic can perform about provability.


share|improve this answer
Not quite what I had in mind, but it's an awesome starting point nonetheless. –  user18921 Feb 4 '13 at 19:55
There are some proof theorists and logicians who post on MSE, if you unaccept this answer they might be likelier to see the question. I'm just giving the well known superficial answer. –  zyx Feb 5 '13 at 4:17
Thanks for the tip! –  user18921 Feb 5 '13 at 4:27
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.