# nLab inconsistency

foundations

## Foundational axioms

foundational axiom

# Contents

## Idea

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.

## Examples

Revised on August 11, 2013 17:22:03 by Urs Schreiber (89.204.135.38)