Difference between revisions of "User:IssaRice/Computability and logic/List of possibilities for completeness and decidability"
From Machinelearning
Line 1: | Line 1: | ||
+ | Suppose we have an effectively axiomatized and consistent theory inside a complete logic. | ||
+ | |||
{| class="sortable wikitable" | {| class="sortable wikitable" | ||
|- | |- | ||
− | ! Decidable logic? | + | ! Decidable logic? !! Decidable theory? !! Complete theory? (negation-completeness) !! Example or proof of non-existence |
|- | |- | ||
− | + | | Yes || Yes || Yes || Empty theory (theory with no non-logical axioms) inside propositional logic | |
|- | |- | ||
− | + | | 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 || 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 || No || No || | |
|- | |- | ||
− | | Yes | + | | Yes || Yes || Yes || |
|- | |- | ||
− | + | | No || Yes || Yes || First-order logic with two binary predicates <math>R</math> and <math>S</math> with the axiom <math>\forall x \forall y (R(x,y)\wedge S(x,y))</math>.<ref>Carl Mummert. https://math.stackexchange.com/a/541680/35525</ref> | |
|- | |- | ||
− | | | + | | No || Yes || No || |
|- | |- | ||
− | + | | No || 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. | |
|- | |- | ||
− | | No | + | | No || No || No || The theory of Robinson arithmetic inside first-order logic |
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
|} | |} | ||
Revision as of 20:21, 20 February 2019
Suppose we have an effectively axiomatized and consistent theory inside a complete logic.
Decidable logic? | Decidable theory? | Complete theory? (negation-completeness) | Example or proof of non-existence |
---|---|---|---|
Yes | Yes | Yes | Empty theory (theory with no non-logical axioms) inside propositional logic |
Yes | Yes | No | Smith's example of with just as an axiom inside a propositional logic with propositional atoms .^{[1]} |
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 | No | No | |
Yes | Yes | Yes | |
No | Yes | Yes | First-order logic with two binary predicates and with the axiom .^{[2]} |
No | Yes | No | |
No | 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 | No | No | The theory of Robinson arithmetic inside first-order logic |
References
- ↑ Peter Smith. An Introduction to Gödel's Theorems (2nd ed). p. 32.
- ↑ Carl Mummert. https://math.stackexchange.com/a/541680/35525