Comments 2006-10-25

edit

The article has been sitting in a half-finished state for a while. I expanded it and set it up for further improvement.

  • This article needs to be at an undergraduate level at the highest
  • More references, especially at the undergrad level, are needed
  • The notation should be kept as simple as possible (but not more simple than that).
  • I think that a proof would be nice, and the proof is elementary anyway.
  • More corollaries would be good.

CMummert 13:42, 25 October 2006 (UTC)Reply

Quantifier Blocks

edit

I believe the 'alternative' definition I added using quantifier blocks and bounded quantifiers should probably be the primary definition. However, I don't remember and need to get back to working on my thesis.Logicnazi (talk) 02:46, 24 November 2007 (UTC)Reply

Definition of

edit

The definition of   differs from the traditional one for   since it would not allow bounded quantifiers. Since Post theorem doesn't say anything about   relation this doesn't affect the theorem, but it seems misleading. Catrincm (talk) 13:34, 30 September 2014 (UTC)Reply

T halts on input n at time n1 at most if and only if is satisfied

edit

What does it mean: "at most if and only if"? Is it equivalence or one-direction consequence?

Eugepros (talk) 10:08, 6 October 2018 (UTC)Reply

I think they mean to say that   is true if and only if   halts at or prior to time  . Related to that, the assertion that   can be a   formula (only having bounded quantifiers) is almost certainly incorrect, or else it needs a citation. I've never seen any formalization of turing machines where the halting time function is  . Obviously   is  , which is sufficient for Post's theorem, and it's even primitive recursive, but the idea that it could be   seems implausible. Jade Vanadium (talk) 20:13, 8 July 2024 (UTC)Reply