Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation

Jonas Bayer, Aleksey Gonus, Christoph Benzmüller +1

This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic…