structure for 'Theory of Logic'    |     alphabetical list of themes    |     unexpand these ideas

5. Theory of Logic / K. Features of Logics / 7. Decidability

[are positive or negative answers always possible?]

7 ideas
Validity is provable, but invalidity isn't, because the model is infinite [Church, by McGee]
     Full Idea: Church showed that logic has a proof procedure, but no decision procedure. If an argument is invalid, there is a model with true premises and false conclusion, but the model will typically be infinite, so there is no way to display it concretely.
     From: report of Alonzo Church (A Note on the entscheidungsproblem [1936]) by Vann McGee - Logical Consequence 5
Expressions are 'decidable' if inclusion in them (or not) can be proved [Enderton]
     Full Idea: A set of expressions is 'decidable' iff there exists an effective procedure (qv) that, given some expression, will decide whether or not the expression is included in the set (i.e. doesn't contradict it).
     From: Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 1.7)
     A reaction: This is obviously a highly desirable feature for a really reliable system of expressions to possess. All finite sets are decidable, but some infinite sets are not.
'Effective' means simple, unintuitive, independent, controlled, dumb, and terminating [Smith,P]
     Full Idea: An 'effectively decidable' (or 'computable') algorithm will be step-by-small-step, with no need for intuition, or for independent sources, with no random methods, possible for a dumb computer, and terminates in finite steps.
     From: Peter Smith (Intro to Gödel's Theorems [2007], 02.2)
     A reaction: [a compressed paragraph]
A theory is 'decidable' if all of its sentences could be mechanically proved [Smith,P]
     Full Idea: A theory is 'decidable' iff there is a mechanical procedure for determining whether any sentence of its language can be proved.
     From: Peter Smith (Intro to Gödel's Theorems [2007], 03.4)
     A reaction: Note that it doesn't actually have to be proved. The theorems of the theory are all effectively decidable.
Any consistent, axiomatized, negation-complete formal theory is decidable [Smith,P]
     Full Idea: Any consistent, axiomatized, negation-complete formal theory is decidable.
     From: Peter Smith (Intro to Gödel's Theorems [2007], 03.6)
'Recursion theory' concerns what can be solved by computing machines [Feferman/Feferman]
     Full Idea: 'Recursion theory' is the subject of what can and cannot be solved by computing machines
     From: Feferman / Feferman (Alfred Tarski: life and logic [2004], Ch.9)
     A reaction: This because 'recursion' will grind out a result step-by-step, as long as the steps will 'halt' eventually.
Both Principia Mathematica and Peano Arithmetic are undecidable [Feferman/Feferman]
     Full Idea: In 1936 Church showed that Principia Mathematica is undecidable if it is ω-consistent, and a year later Rosser showed that Peano Arithmetic is undecidable, and any consistent extension of it.
     From: Feferman / Feferman (Alfred Tarski: life and logic [2004], Int IV)