How to use Manuel Lerman's framework of priority method as blackbox?

Question

Manuel Lerman has a book "A Framework for Priority Arguments" that builds a framework of priority method. However, the definitions in the book are quite involved and not written in a very formal way.

If I just want use the framework as a blackbox to construct c.e. degrees that satisfy some requirements, then which definitions and results in the book I should know at least?

For example, for forcing method, I only need to know the definition of M[G], and M[G] preserves ordinals, s.t. ZFC, and the forcing theorem that make me know how to check sentences in M[G] by M. I don't need to know how to prove them, I only need to know how to apply them. What is the case in the priority framework?

Answer 1

I'm afraid that's not really how it works. You can't really use frameworks like this as a black box. The heart of the proof is figuring out how all the requirements play nicely together and that can't really be done while treating it as a black box. Sure, if you prove certain lemmas you can show the resulting construction has certain nice properties but those lemmas inevitably require looking inside the box.

In computability theory the framework is more about helping you manage the complexity of your construction. Forcing in set theory is like a library call in a programming language. You hand over the right sort of input and you get back a forcing extension. In computability theory the construction frameworks are more akin to a technique like object orientation that helps you manage complexity but you still have to write the code yourself.

--

Others may disagree but I think that probably just plays out as a different interpretation of what it means to treat something as a black box than any disagreement over the fact that interesting constructions require thinking hard about the way the framework works with your requirements.