Difference between revisions of "User:IssaRice/Computability and logic/List of possibilities for completeness and decidability"

From Machinelearning
Jump to: navigation, search
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? !! Complete logic? (semantic completeness) !! Decidable theory? !! Complete theory? (negation-completeness) !! Example or proof of non-existence
+
! Decidable logic? !! 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 || Empty theory (theory with no non-logical axioms) inside propositional logic
 
|-
 
|-
| 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 || 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 || 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 || 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 || No || No ||
 
|-
 
|-
| Yes || No || Yes || Yes ||
+
| Yes || Yes || Yes ||
 
|-
 
|-
| Yes || No || Yes || No ||
+
| 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>
 
|-
 
|-
| Yes || No || No || Yes ||
+
| No || Yes || No ||
 
|-
 
|-
| Yes || No || No || 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 || Yes || 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 || No || No || The theory of Robinson arithmetic inside first-order logic
|-
 
| 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 <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 || 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 ||
 
 
|}
 
|}
  

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 T_1 with just \neg p as an axiom inside a propositional logic with propositional atoms p,q,r.[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 \phi or \neg \phi, which gives us an algorithm for deciding whether or not \phi is a theorem.
Yes No No
Yes Yes Yes
No Yes Yes First-order logic with two binary predicates R and S with the axiom \forall x \forall y (R(x,y)\wedge S(x,y)).[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 \phi or \neg \phi, which gives us an algorithm for deciding whether or not \phi is a theorem.
No No No The theory of Robinson arithmetic inside first-order logic

References

  1. Peter Smith. An Introduction to Gödel's Theorems (2nd ed). p. 32.
  2. Carl Mummert. https://math.stackexchange.com/a/541680/35525