I usually think of logics as search algorithms, since that's how the semantics for the meta-language describing them are defined. I guess you could call a Turi

I usually think of logics as search algorithms, since that's how the semantics for the meta-language describing them are defined. I guess you could call a Turing Machine implementing the search algorithm for proofs implied by a logic an "observer", since it produces "reachability observations" i.e. proofs.