Some results in computability and the proof theory of predicate modal logi

In the first part we develop a syntactic proof theory for the first order modal logic systems M3 (and BM) [53, 54] and ML3 by demonstrating their respective equivalence to two modal Gentzen predicate calculi that we introduce and call GTKS and GLTS --- a result that very much relies on proving cut-derivability in both of these Gentzen systems; we then use this equivalence to give a syntactic proof of a conservation theorem (CT) and weak reflection (WR) for both M3 (and BM) and ML 3.;We then proceed to show that ML3 shares some of the properties of the system GL [40] --- namely, we introduce a suitable definition of an arithmetical interpretation of a ML3 formula which allows us to obtain a soundness lemma; and we also prove the semantic completeness of ML3 with respect to well-capped and transitive Kripke models [28].;Finally, we have devised another method, involving formula mappings, to obtain a proof of the CT and WR for both ML and ML3.;The second part is on the power of iteration. We first demonstrate that the class of primitive recursive functions can be obtained by using the schema of pure iteration rather than that of primitive recursion ; we then introduce the schema of infinite iteration and show that closing the class of primitive recursive functions under it, yields the class of partially recursive functions.1.;1These results were published in [44].