Is it possible to construct different systems of logic in Coq or Agda?
I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, relevant logics, and conditional logics in Graham Priest's 2nd edition of An Introduction to Non-Classical Logic (I keep going back to over the years in my free time).
It seems like intuitionistic logic is definitely possible in Coq given it was developed alongside the calculus of constructions, but I'm curious if Coq (or Agda) could be used for other logics.
A part of my gut says, "It wouldn't be possible to do logics that use fewer rules of inference or swap out intuitionistic rules for incompatible rules (eg, removing the principle of explosion)." However, another part of my gut says, "Machines using binary gates can still represent & simulate quantum processes, so it may be possible for Coq to represent logics incompatible with it's own implementation."
Any references to good papers/books/lectures/etc. are happily welcome. 🙏
Axiom
keyword. But them again, this is only for things you can represent as statements in the Coq programming language, so you can't really have an impossibly weird logic $\endgroup$