Abstract
We instantiate our syntax-independent logic infrastructure developed
in a
separate AFP entry to the FOL theory of Robinson arithmetic
(also known as Q). The latter was formalised using Nominal Isabelle by
adapting Larry
Paulson’s formalization of the Hereditarily Finite Set
theory.