Difference between revisions of "User:IssaRice/Computability and logic/List of possibilities for completeness and decidability"
From Machinelearning
Line 7: | Line 7: | ||
| Yes || Yes || Yes || No || Smith's example of <math>T_1</math> with just <math>\neg p</math> as an axiom inside a propositional logic with propositional atoms <math>p,q,r</math>.<ref>Peter Smith. ''An Introduction to Gödel's Theorems'' (2nd ed). p. 32.</ref> | | Yes || Yes || Yes || No || Smith's example of <math>T_1</math> with just <math>\neg p</math> as an axiom inside a propositional logic with propositional atoms <math>p,q,r</math>.<ref>Peter Smith. ''An Introduction to Gödel's Theorems'' (2nd ed). p. 32.</ref> | ||
|- | |- | ||
− | | Yes || Yes || No || Yes || | + | | 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 <math>\phi</math> or <math>\neg \phi</math>, which gives us an algorithm for deciding whether or not <math>\phi</math> is a theorem. |
|- | |- | ||
| Yes || Yes || No || No || | | Yes || Yes || No || No || |
Revision as of 20:06, 20 February 2019
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