# What does it really mean for a formal system to be consistent?

As far as I understand, asserting that a formal system $$T$$ is consistent means that there does not exist a sentence $$\varphi$$, expressed in the language of $$T$$, such that $$T$$ proves $$\varphi$$ and $$T$$ proves $$\neg\varphi$$. This definition of consistency makes sense on an intuitive level, but it invites the question: in what metatheory is the sentence "there does not exist a $$\varphi$$ such that $$T$$ proves $$\varphi$$ and $$T$$ proves $$\neg\varphi$$" expressed?

It often seems that people consider some formal systems to be consistent in a Platonic sense, and they are not making a claim about any particular metatheory. For example, many logicians really believe in the consistency of, say, Peano Arithmetic. However, can this idea be made sense of from a formalist point of view?

• I suppose we would know the answer to your question if we knew the answer to the simpler question, what does it really mean for a sentence $\varphi$ to be provable in a formal system $T$. Why, then, do you speak of consistency? Is that not an unnecessary complication? Also, what does it really mean for $\varphi$ to be expressed in the language of $T$? Is expressibility somehow less problematic that provability?
– bof
Jul 1 at 23:17
• “Consistency” often refers to having a model. I.e. $T$ is consistent if and only if $T$ has a model. What exactly a “model” is can vary contextually. This notion of consistency is more useful in abstract model theory because most logics don’t contain a clear notion of “proof”. In first order logic though, if $T$ is a first order theory capable of expressing arithmetic, then there is a sentence con($T$) which is satisfiable if and only if $T$ is consistent. This is expressed in a similar way to the meta theoretic sentence you described.
– Joe
Jul 2 at 1:18
• Consistency is a "formalist" property: two sentences whose only difference is the leading negation sign in one of them. Jul 6 at 10:43