 The Metamath language has no specific logic embedded in it.Instead, it can simply be regarded as a way to prove that inference rules (asserted as axioms or proven later) can be applied.The largest database of proved theorems follows conventional ZFC set theory and classic logic, but other databases exist and others can be created.