You are here

Propositional inference rules

26 July, 2019 - 12:03
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

Abbreviation

Name

If you know all of. . .

. . .then you can infer

Table 6.2 Our propositional inference rules

∧Intro

and-introduction

\phi

\phi \wedge \psi

\psi

∧Elim

and-elimination (left)

\phi \wedge \psi

\phi

 

and-elimination (right)

\phi \wedge \psi

\psi

∨Intro

or-introduction (left)

\phi

\phi \vee \psi

 

or-introduction (right)

\psi

\phi \vee \psi

∨Elim

or-elimination

\phi \vdash \theta

\theta

\psi \vdash \theta

\phi \vee \psi

⇒Intro

if-introduction

\phi ,\psi ,...,\theta \vdash \omega

φ ∧ ψ ∧ . . . ∧ θ ⇒ ω

⇒Elim

if-elimination (modus ponens)

\phi \Rightarrow \psi

\psi

\phi

falseIntro

false-introduction

\phi

false

\dashv \phi

falseElim

false-elimination

false

\phi

RAA

reductio ad absurdum (v. 1)

\dashv \phi \vdash false

\phi

reductio ad absurdum (v. 2)

\phi \vdash false

\dashv \phi

¬Intro

negation-introduction

\phi

\dashv \dashv \phi

¬Elim

negation-elimination

\dashv \dashv \phi

\phi

CaseElim

case-elimination (left)

\phi \vee \psi

\psi

\dashv \phi

case-elimination (right)

\phi \vee \psi

\phi

\dashv \psi

 

As usual, φ, ψ, θ, ω are meta-variables standing for any WFF.

This is by no means the only possible inference system for propositional logic.

ASIDE: This set of inference rules is based upon DiscTete Mathematics with a ComputeT by Hall and O'Donnell (Springer, 2000) and The Beseme Project .