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

proof-by-refutation-1 (math concept)

Definition

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

\[\left( \boldsymbol{\mathcal{H}} \: \textit{assume} \: \boldsymbol{P}, Inc\left( \boldsymbol{\mathcal{H}} \right) \right) \vdash \neg \boldsymbol{P}\]

Where:

  • \(\boldsymbol{\mathcal{H}}\) is an hypothesis

  • \(\boldsymbol{P}\) is a formula-statement

  • \(\mathit{Inc}\) is the inconsistency function

In plain language, it consists in posing the hypothesis that a proposition \(\boldsymbol{P}\) is true, refuting that hypothesis by proving \(\neg \boldsymbol{P}\), inferring the inconsistency of that hypothesis from this contradiction, and finally inferring \(\boldsymbol{P}\) (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