# Consistent theory based on L and not(A->A) is a theorem

I am working on this problem in which I have a theory $$T$$ based on language $$\mathcal{L}$$ and the only information we have is that T is consistent and $$\vdash \lnot(A \rightarrow A)$$. Given this information, how can I know if this theory is sound, complete and/or decidable?

My only guess is that I can say that $$T$$ is sound because since $$T$$ is consistent and we can derive $$\lnot(A \rightarrow A)$$ from axioms and inference rules, $$\lnot(A \rightarrow A)$$ is a theorem and because of that we can assume that $$T$$ is sound (because the premises and conclusions are true).

Thank you!

• Your problem statement makes no sense because in first-order classical logic $\lnot (A \to A)$ is false, and therefore it can only be a theorem in inconsistent theory. Please double check that you transcribed it correctly. Jul 21, 2020 at 20:59

The first thing to point out is that $$\lnot(A \rightarrow A)$$ leads to a contradiction: ($$A \land \lnot A$$). Since propositional logic itself is consistent, it is impossible to derive a contradiction, so $$\vdash \lnot(A \rightarrow A)$$ is impossible.
So perhaps your intention was $$T \vdash \lnot(A \rightarrow A)$$. This can only happen if $$T$$ is itself inconsistent.
Given that $$T$$ is inconsistent, $$T$$ is vacuously complete (since an inconsistent theory can prove any formula) and decidable (for the same reason). As for soundness, it's a property of the logical system, not any particular theory like $$T$$. Propositional logic is sound.