basic constructions:
strong axioms
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
A system in formal logic is called inconsistent if it admits a proof of a contradiction (that is, usually, a proof of false, or an inhabitant of the empty type).
Accordingly an axiom is called inconsistent or to lead to an inconsistency if adding it to an (implicitly understood) ambient logical system makes that system inconsistent.
In most usual logical systems, it follows that an inconsistent system admits a proof of every proposition, by the rule ex falso quodlibet (which is just the elimination rule for the empty type). For this reason, sometimes (especially in type theory), the adjective “inconsistent” is used to mean a system with this property instead. If we want to distinguish, then a system which admits a proof of every proposition may be called trivial. Of course, a trivial system is inconsistent, but a paraconsistent logic can be inconsistent without being trivial.