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
basic constructions:
strong axioms
further
Most of the time, a proposition is a contradiction if assuming it there is a proof of false, hence if the hypothetical judgement
is valid.
In paraconsistent logic, however, one sometimes reserves the term “contradiction” for the situation when both a proposition and its negation hold. This is often a contradiction in the above sense, but not always.
A system of formal logic that proves a contradiction is called inconsistent.
Last revised on September 22, 2012 at 13:48:23. See the history of this page for a list of all contributions to it.