Decidability (logic)

In mathematical logic and computability theory, decidability refers to the existence of an effective method (an algorithm) for determining whether a given statement or formula is true or false within a specific formal system. More precisely, a formal system, theory, or problem is said to be decidable if there exists an algorithm that, given any statement expressible in the language of that system, will correctly determine whether that statement is a theorem of the system (i.e., provable from the axioms). If no such algorithm exists, the system, theory, or problem is said to be undecidable.

A decision problem can be thought of as a question whose answer is either "yes" or "no" based on some input. A decidable decision problem is one for which there is an algorithm that always produces the correct answer in a finite amount of time.

The concept of decidability is closely related to the concept of completeness. A formal system is complete if every true statement in the system can be proven within the system. However, completeness and decidability are distinct concepts. A system can be complete but undecidable, and vice versa.

One of the most famous examples of an undecidable problem is the halting problem, which asks whether a given program will halt (terminate) or run forever. Alan Turing proved that there is no general algorithm that can solve the halting problem for all possible programs and inputs.

The concept of decidability has significant implications for the limits of what can be known and computed. Undecidability results demonstrate that there are inherent limitations to algorithmic problem-solving and that certain questions are fundamentally beyond the reach of computation. The study of decidability is crucial for understanding the boundaries of computability and the capabilities of formal systems.