Contradiction & Inconsistency
Intuition
A contradiction is a situation where a statement is assigned two distinct truth values. A logical system is inconsistent when it proves a contradiction.
Because the principle of explosion (ex falso quodlibet or EFQ) is an axiom ax-efq, any proof of falsehood is enough to show that the entire system is inconsistent and would reveal that at least one of our axioms ought to be removed. We will focus our discussion on this principle.
The relation {gai'o} is uninhabited. We take this as a principle at first:
by sheer intuition of the words, {cei'i} has exactly one inhabitant and
{gai'o} has zero inhabitants. In light of that principle, we have a theorem
na-gaiho supported by a short list of axioms:
| Name | Statement |
|---|---|
| ax-mp | broda & ganai broda gi brode ⇒ brode |
| ax-k | ganai broda gi ganai brode gi broda |
| ax-s | ganai ganai broda gi ganai brode gi brodi gi ganai ganai broda gi brode gi ganai broda gi brodi |
| ax-ge-le | ganai ge broda gi brode gi broda |
| ax-ge-re | ganai ge broda gi brode gi brode |
| ax-ge-in | ganai broda gi ganai brode gi ge broda gi brode |
| df-go | ge ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda gi ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode |
| df-naku | go naku broda gi ganai broda gi gai'o |
| na-gaiho | naku gai'o |
So, from that principle and those axioms, we have a theorem: {gai'o} is
uninhabited. Any proof of {gai'o} would directly contradict that theorem and
lead to inconsistency, after which we could prove anything using efqii.
This also gives a metatheorem whose proof does not fit here: the axioms MP, K,
S, and EFQ, as well as the definitions of {ge}, {go}, and {naku} (and
{ganai}) are beyond impeachment. Any attempt to refute them has to use them.
This should not be seen as a problem because, aside from the definition of
negation and the principle of explosion, these axioms and definitions are
ratified by the simply-typed lambda calculus
(WP,
nLab), which is consistent
due to having Cartesian-closed categories
(WP,
nLab) as models.
Known Obstacles
We will say that a statement is impossible when its proof would provably lead to inconsistency by contradiction, and we will say that such a proof is an obstacle for that statement. Since Metamath operates on axiom schemata, the obstacles in the database are actually collections of obstacles for many individual impossible statements. Here are all obstacles currently in the database:
Note that lnci formally asserts that no bridi is both inhabited and uninhabited. As such, it is a formalization of our earlier intuition. It is only meaningful if our axioms are consistent, but it does prevent our axioms from proving any further inconsistencies. As such, it is known as the law of non-contradiction.
Known Refutations
The following obstacles are refutations to the existence of certain objects. An object is refuted if its existence would imply a contradiction; such an object is self-defeating. Like EFQ, this principle of refuting self-defeating objects is included as an axiom ax-sdo.
| Name | Statement |
|---|---|
| nomei-gaiho | ko'a cmima le nomei ku ⇒ gai'o |
| succ-zero-ref | ko'a kacli'e li no ⇒ gai'o |
| gt-zero-ref | ko'a kacme'a li no ⇒ gai'o |