Tags: inference-rule

Inference rules reference table

Unabridged name

Abridged name

Formula

absorption

abs.

\(\left(\boldsymbol{P} \implies \mathbf{Q}\right) \vdash \left(\boldsymbol{P} \implies \boldsymbol{P} \land \mathbf{Q}\right)\)

axiom-interpretation

ai

\(\boldsymbol{\mathcal{A}} \vdash \boldsymbol{P}\)

biconditional-elimination-1

be1

\(\left( \boldsymbol{P} \iff \mathbf{Q} \right) \vdash \left( \boldsymbol{P} \implies \mathbf{Q} \right)\)

biconditional-elimination-2

be2

\(\left( \boldsymbol{P} \iff \mathbf{Q} \right) \vdash \left( \mathbf{Q} \implies \boldsymbol{P} \right)\)

biconditional-introduction

bi

\(\left( \left( \boldsymbol{P} \implies \mathbf{Q} \right), \left( \mathbf{Q} \implies \boldsymbol{P} \right) \right) \vdash \left( \mathbf{Q} \iff P \right)\)

conjunction-elimination-1

ce1

\(\left( \boldsymbol{P} \land \mathbf{Q} \right) \vdash \boldsymbol{P}\)

conjunction-elimination-2

ce2

\(\left( \boldsymbol{P} \land \mathbf{Q} \right) \vdash \mathbf{Q}\)

conjunction-introduction

ci

\(\boldsymbol{P}, \boldsymbol{Q} \vdash \left( \boldsymbol{P} \land \boldsymbol{Q} \right)\)

constructive-dilemma

cd

\(\left( \left( \boldsymbol{P} \implies \boldsymbol{Q} \right), \left( \boldsymbol{R} \implies \boldsymbol{S} \right), \left( \boldsymbol{P} \lor \boldsymbol{R} \right) \right) \vdash \left( \boldsymbol{Q} \lor \boldsymbol{S} \right)\)

definition-interpretation

di

\(\boldsymbol{\mathcal{D}} \vdash \boldsymbol{P}\)

destructive-dilemma

dd

\(\left( \left( \boldsymbol{P} \implies \boldsymbol{Q} \right), \left( \boldsymbol{R} \implies \boldsymbol{S} \right), \left( \neg \boldsymbol{Q} \lor \neg \boldsymbol{S} \right) \right) \vdash \left( \neg \boldsymbol{P} \lor \neg \boldsymbol{R} \right)\)

disjunction-introduction-1

di1

\(\boldsymbol{P} \vdash \left( \mathbf{Q} \lor \boldsymbol{P} \right)\)

disjunction-introduction-2

di2

\(\boldsymbol{P} \vdash \left( \boldsymbol{P} \lor \mathbf{Q} \right)\)

disjunctive-resolution

dr

\(\left( \left( \boldsymbol{P} \lor \boldsymbol{Q} \right), \left( \neg \boldsymbol{P} \lor \boldsymbol{R} \right) \right) \vdash \left( \boldsymbol{Q} \lor \boldsymbol{R} \right)\)

disjunctive-syllogism-1

ds1

\(\left( \left( \boldsymbol{P} \lor \boldsymbol{Q} \right), \neg \boldsymbol{P} \right) \vdash \boldsymbol{Q}\)

disjunctive-syllogism-2

ds2

\(\left( \left( \boldsymbol{P} \lor \boldsymbol{Q} \right), \neg \boldsymbol{Q} \right) \vdash \boldsymbol{P}\)

double-negation-elimination

dne

\(\lnot \left( \lnot \left( \boldsymbol{P} \right) \right) \vdash \boldsymbol{P}\)

double-negation-introduction

dni

\(\boldsymbol{P} \vdash \lnot \left( \lnot \left( \boldsymbol{P} \right) \right)\)

equal-terms-substitution

ets

\(\left( \boldsymbol{P}, x = y \right) \vdash \mathbf{Q}\)

equality-commutativity

ec

\(\left( x = y \right) \vdash \left( y = x \right)\)

hypothetical-syllogism

hs

\(\left( \left( \boldsymbol{P} \implies \boldsymbol{Q} \right), \left( \boldsymbol{Q} \implies \boldsymbol{R} \right) \right) \vdash \left( \boldsymbol{P} \implies \boldsymbol{R} \right)\)

inconsistency-introduction-1

ii1

\(\left( \boldsymbol{P}, \neg \left(\boldsymbol{P}\right) \right) \vdash Inc\left(\mathcal{T}\right)\)

inconsistency-introduction-2

ii2

\(\left(\left(x = y\right), \left(x \neq y\right)\right) \vdash Inc\left(\mathcal{T}\right)\)

inconsistency-introduction-3

ii3

\(\left( \boldsymbol{P} \neq P \right) \vdash Inc\left(\mathcal{T}\right)\)

modus-ponens

mp

\(\left( \left( \boldsymbol{P} \implies \boldsymbol{Q} \right), P \right) \vdash \boldsymbol{Q}\)

modus-tollens

mt

\(\left( \left( \boldsymbol{P} \implies \boldsymbol{Q} \right), \neg Q \right) \vdash \neg \boldsymbol{P}\)

proof-by-contradiction-1

pbc1

\(\left( \boldsymbol{\mathcal{H}} \: \text{assume} \: \neg \boldsymbol{P}, \mathit{Inc}\left( \boldsymbol{\mathcal{H}} \right) \right) \vdash \boldsymbol{P}\)

proof-by-contradiction-2

pbc2

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

proof-by-refutation-1

pbf1

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

proof-by-refutation-2

pbf2

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

variable-substitution

vs

\(\left( \boldsymbol{P}, \boldsymbol{\Phi} \right) \vdash \boldsymbol{Q}\)

See also

Bibliography