Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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|cite|improve this question
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|cite|improve this answer
Not quite what I had in mind, but it's an awesome starting point nonetheless. – goblin 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! – goblin Feb 5 '13 at 4:27

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.