I'm new to logic theory and i'm stuck with the understanding of decidability of a logical system.
As far as I understand, the decidability of a logical system is related to the existence of an effective (in terms of time) procedure to tell whether a given formula can be proved by using the "instruments" of the system.
My question is: Why should we care about whether a given formula can (or cannot) be inferred within a logical system? What will happen when we say that "the formula cannot be formed within the system" or even "I don't know whether I can use the constructed system to prove the validity of the formula"? In this case, does it mean that we will need to construct a new system (for example: set theory version 2), does it mean that the existing system is "weak"?
Thank you very much for your enlightenment.
The decidability problem has to do with determining whether a given syntactically correct well-formed formula is a theorem, a contingent statement, or a contradiction. Classical logic is decidable using the method of truth tables and various other equivalent procedures. There are variant logics, such as intuitionism, several varieties of modal logic, and various experimental or partial logics that vary the "laws" of classical logic. In these, the method of truth tables doesn't apply, so it is not clear whether a given arbitrary wff is a theorem, contradiction, or contingent statement. The usual procedure in these cases is to begin with a set of axioms and inference rules, and infer, derive, or prove the theorems. It then becomes important (and more difficult) to determine whether a given formula is provable.
Multi-valued logics typically have different problem. These are decidable using truth tables, it's just that the theorems that can be proven are typically far less useful and versatile than those of classical logic.