Isabelle/Lower Order Logic
A complete and novel formalization of Lower-Order Logic (LOL) in Isabelle.
Lower-Order Logic supports arbitrary functions of arity zero.