|
A logical system is decidable iff there exists an algorithm such that for every well-formed formula in that system there exists a maximum finite number N of steps such that the algorithm is capable of deciding in less than or equal to N algorithmic steps whether the formula is (semantically) valid or not valid.
Example: Propositional calculus is decidable, because there exists for it an algorithm — truth-table construction — such that for every formula which combines M atomic formulas there is a maximum number N = 2M of steps such that after completing those N steps the algorithm will always decide whether the formula is valid or not. Here, a "step" of the algorithm has been (arbitrarily) defined as completion of a row of the truth-table.
If a system is undecidable, then there exist in it formulas which are not known to be either valid or invalid: perhaps such a formula can be categorized neither as valid or invalid. Such formulas are said to be "undecided."
If a formula in an undecidable logical system is undecided, then there is the option of adopting such formula as a new axiom of the system. Alternatively, it is also possible to adopt the negation of such undecided formula as a new axiom of an alternative system. The resulting pair of axiomatic systems would be mutually incompatible. Example: the parallel postulate.
First-order predicate calculus is decidable if confined to predicates with only one argument. If it includes predicates with two or more arguments, then it is not decidable.
| 
