I have a basic question about the definition of syntactic consistency of a theory $T$. Traditionally, we define syntactic consistency as follows:
A theory $T$ is syntactically consistent if there exists no formula $A$ in the language such that both $A$ and $\neg A$ are provable.
And likewise, the inconsistency is defined as follows:
A theory $T$ is syntactically inconsistent if there exists a formula $A$ in the language such that both $A$ and $\neg A$ are provable.
I wonder if we can just use $\perp$ to do the same job:
$T$ is consistent iff $\vdash\neg(T\rightarrow\perp)$.
$T$ is inconsistent iff $\vdash T\rightarrow\perp$.
Is this plausible?
Best Answer
Yes; if you have a dedicated symbol $\bot$ and a rule that allows you to syntactically derive $\bot$ from contradictory formulas, then you can define (in-)consistency accordingly. Some presentations just define contradiction as "$A$ and $\neg A$" and don't have the symbol $\bot$ for it.
But careful with the notation: $T$ is not a formula, so it does not make sense to write $T \to \bot$. And unprovability ($\not \vdash$) does, in the general case, not entail provability of the negation ($\vdash \neg$)!
What you mean is