Tags: proof-by-refutation-2 math concept inference-rule

proof-by-refutation-2 (math concept)

Definition

proof-by-refutation-2 is the inference-rule:

\[\left( \boldsymbol{\mathcal{H}} \: \textit{assume} \: \boldsymbol{x} = \boldsymbol{y}, \; Inc\left( \boldsymbol{\mathcal{H}} \right) \right) \vdash \boldsymbol{x} \neq \boldsymbol{y}\]

Where:

In straightforward language, if from the hypothesis that x is equal to y, it follows that the hypothesis is inconsistent, it follows that x is not equal to y (or alternatively that the parent theory is itself inconsistent).

Note

Note the possibility that the base theory-derivation from which the hypothesis is elaborated is inconsistent.

Synonyms

  • proof of negation [Bau10]

  • refutation by contradiction [nLab17]

Sources