This thesis explores the potential of classical higher-order logic (HOL) as a general-purpose meta-language capable of representing and formally reasoning about diverse domain-specific object languages. To demonstrate its versatility, we have developed a library composed of combinator-based modular building blocks within the Isabelle/HOL proof assistant, but easily translatable to other HOL-based systems. We propose that this library exemplifies a universal mathematical language layered over HOL, sufficiently powerful to capture and represent a broad range of logical formalisms—whether classical or non-classical—as well as their underlying classes of mathematical structures. To support this claim, we provide relevant references, primarily drawn from previous research. Moreover, we delve into the domain of multi-agent systems (MAS), introducing the concept of Argumentative Reasoning Agents (ARAs). This kind of agents, we suggest, are particularly well-suited to leverage the expressive power of the proposed library. In this manner, HOL emerges as an ideal common language—a lingua franca—for facilitating effective reasoning and interaction among argumentative reasoning agents in artificial intelligence.
