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
Most of the time, a proposition $\phi$ 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.