Skip to main content
remove extraneous assumption
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For EVERY computably enumerable set $R$ with non-computable complement $R'$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated. In other words, what you have is an intensional property of the set rather than an extensional one.

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For EVERY computably enumerable set $R$ with non-computable complement $R'$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated. In other words, what you have is an intensional property of the set rather than an extensional one.

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For EVERY computably enumerable set $R$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated. In other words, what you have is an intensional property of the set rather than an extensional one.

added 97 characters in body
Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For everyEVERY computably enmberableenumerable set $R$ with non-computable complement $R'$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated. In other words, what you have is an intensional property of the set rather than an extensional one.

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For every computably enmberable set $R$ with non-computable complement $R'$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated.

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For EVERY computably enumerable set $R$ with non-computable complement $R'$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated. In other words, what you have is an intensional property of the set rather than an extensional one.

Source Link
Joel David Hamkins
  • 236.5k
  • 44
  • 777
  • 1.4k

Noah has given an excellent answer. Here is another way to look at such an answer.

Theorem. For every computably enmberable set $R$ with non-computable complement $R'$ and for every computably axiomatizable consistent theory $T$, there is a Turing machine that enumerates $R$, such that $T$ does not prove any assertion of the form $n\in R'$, using that enumeration of $R$.

Proof. Fix any enumeration of $R$, and then modify it to produce a Turing machine that also enumerates everything into $R$, if a proof of a contradiction from $T$ is found. Since $T$ does not prove that $T$ has no such proof, $T$ cannot prove that any assertion of the form $n\in R'$. But meanwhile, since $T$ really is consistent, then this program will enumerate $R$ correctly. QED

Thus, the property you are asking about is not a property of the predicate or the c.e. set you have in mind, but rather it is a property of your way of describing how that set is enumerated.