Decidability of A Logical System
Each logical system comes with both a syntactic component, which among other things determines the notion of provability, and a semantic component, which determines the notion of logical validity. The logically valid formulas of a system are sometimes called the theorems of the system, especially in the context of first-order logic where Gödel's completeness theorem establishes the equivalence of semantic and syntactic consequence. In other settings, such as linear logic, the syntactic consequence (provability) relation may be used to define the theorems of a system.
A logical system is decidable if there is an effective method for determining whether arbitrary formulas are theorems of the logical system. For example, propositional logic is decidable, because the truth-table method can be used to determine whether an arbitrary propositional formula is logically valid.
First-order logic is not decidable in general; in particular, the set of logical validities in any signature that includes equality and at least one other predicate with two or more arguments is not decidable (provided the finitely axiomatizable theory Robinson Arithmetic is consistent; this provison is implicit in every undecidability claim made in this article). Logical systems extending first-order logic, such as second-order logic and type theory, are also undecidable.
The validities of monadic predicate calculus with identity are decidable, however. This system is first-order logic restricted to signatures that have no function symbols and whose relation symbols other than equality never take more than one argument.
Some logical systems are not adequately represented by the set of theorems alone. (For example, Kleene's logic has no theorems at all.) In such cases, alternative definitions of decidability of a logical system are often used, which ask for an effective method for determining something more general than just validity of formulas; for instance, validity of sequents, or the consequence relation {(Г, A) | Г ⊧ A} of the logic.
Read more about this topic: Decidability (logic)
Famous quotes containing the words logical system, logical and/or system:
“The sensual and spiritual are linked together by a mysterious bond, sensed by our emotions, though hidden from our eyes. To this double nature of the visible and invisible world—to the profound longing for the latter, coupled with the feeling of the sweet necessity for the former, we owe all sound and logical systems of philosophy, truly based on the immutable principles of our nature, just as from the same source arise the most senseless enthusiasms.”
—Karl Wilhelm Von Humboldt (1767–1835)
“Opera, next to Gothic architecture, is one of the strangest inventions of Western man. It could not have been foreseen by any logical process.”
—Kenneth MacKenzie Clark, Baron of Saltwood (1903–1983)
“Fear, coercion, punishment, are the masculine remedies for moral weakness, but statistics show their failure for centuries. Why not change the system and try the education of the moral and intellectual faculties, cheerful surroundings, inspiring influences? Everything in our present system tends to lower the physical vitality, the self-respect, the moral tone, and to harden instead of reforming the criminal.”
—Elizabeth Cady Stanton (1815–1902)