In 'Lob's Theorem as a Limitation on Mechanism' Detlefson uses Lob's theorem to argue for the 'general limitative thesis' that "There are epistemically valuable humanoid systems of belief A such that no humanoid observer O who uses A as an 'additive' epistemic authority can either know or truly believe of A that she is mechanizable (i.e. that her belief-set, A, is r.e.)."
By saying that O uses A as an 'additive' epistemic authority, Detlefson means that A is disposed to assert something which O couldn't already learn by deriving it from his current beliefs. And, for O to take A as an epistemic authority means that he's disposed to accept all sentences of the form 'if A asserts that X, then X'.
Now, Lob's theorem says that (given a formal provability PROV predicate which satisfies certain constraints) you can only prove "If PROV(X) then X", in situations where you can directly prove that X. And Detlefson (in my opinion) correctly draws the consequence that the following two things can't simultaniously be true: a)A is an additive epistemic authority for you b) A is mechanizable, and you know that a certain program M recursively enumerates all the things that A is disposed to say.*
But, note the following crucial difference between this point and the 'general limitative thesis' above. From the fact that, if you knew which program enumerates all the sentences A is disposed to accept, A would no longer be an *additive* epistemic authority for you, it doesn't follow that you can't truly believe there is some program which enumerates the sentences which, something that's currently an additive epistemic authority for you, would accept.
Thus, I'm puzzled when, Detlefson immediately follows a statement that you can't know which program captures the behavior of something that's an additive epistemic authority for you, with "we therefore maintain that", and then a statement of the General Limitative Thesis, which says that you can't know (or even truely believe!) that there is some such program.
*Actually, you don't need Lob's theorem for this. For, if A is an additive authority for me, there must be some proposition P which A can derive but I can't. But M recursively enumerates the set of sentences which A is disposed to accept. So, there's some stage t at which A arrives at proposition P, and the t-th step of program M is to output P. But I can prove that the t-th stage of program M outputs P, and I believe that M enumerates all and only the sentences A accepts, AND I believe of each proposition that if A accepts, the it's true. So, from these things, I too can derive that P. Contradiction.