User:IssaRice/Computability and logic/List of possibilities for completeness and decidability
From Machinelearning
Decidable logic? | Complete logic? (semantic completeness) | Decidable theory? | Complete theory? (negation-completeness) | Example or proof of non-existence |
---|---|---|---|---|
Yes | Yes | Yes | Yes | Empty theory (theory with no non-logical axioms) inside propositional logic |
Yes | Yes | Yes | No | Smith's example of with just as an axiom inside a propositional logic with propositional atoms .^{[1]} |
Yes | Yes | No | Yes | Assuming the theory is effectively axiomatized and consistent, this is not possible. To see why, suppose the theory is negation-complete. We could then computably enumerate all the theorems (since the theory is effectively axiomatized), and after a finite amount of time we will find exactly one of or , which gives us an algorithm for deciding whether or not is a theorem. |
Yes | Yes | No | No | |
Yes | No | Yes | Yes | |
Yes | No | Yes | No | |
Yes | No | No | Yes | |
Yes | No | No | No | |
No | Yes | Yes | Yes | First-order logic with two binary predicates and with the axiom .^{[2]} |
No | Yes | Yes | No | |
No | Yes | No | Yes | Assuming the theory is effectively axiomatized and consistent, this is not possible. To see why, suppose the theory is negation-complete. We could then computably enumerate all the theorems (since the theory is effectively axiomatized), and after a finite amount of time we will find exactly one of or , which gives us an algorithm for deciding whether or not is a theorem. |
No | Yes | No | No | The theory of Robinson arithmetic inside first-order logic |
No | No | Yes | Yes | |
No | No | Yes | No | |
No | No | No | Yes | |
No | No | No | No |
References
- ↑ Peter Smith. An Introduction to Gödel's Theorems (2nd ed). p. 32.
- ↑ Carl Mummert. https://math.stackexchange.com/a/541680/35525