Rules of inference
Conjunction
and-introduction
adjunction
conjunction introduction
and-elimination
two rules, one for each assumption: and
Disjunction
Disjunction introduction
∨I
and
Disjunction elimination, ∨EL and ∨ER
implication
implication introduction:
implication elimination:
(modus ponens, implies-elimination, arrow-elimination)
modus tollens:
implication introduction
implication elimination (modus ponens, implies-elimination, conditional elimination)
conditional proof (conditional introduction)
modus tollens
Modus ponens
Modus ponens (modus ponendo ponens i.e. "mode that affirms by affirming", or implication elimination, or elimination) is a rule of inference in propositional logic that can be summarized as: "if p then q; there is a p, therefore there is a q".
As a sequent: where is a metalogical symbol meaning that q is a syntactic consequence of and in some logical system.
As the statement of a truth-functional tautology or theorem of propositional logic: , where , and are propositions expressed in some formal system.
Negation
Negation introduction (Reductio ad absurdum)
double negation
double negation introduction:
double negation elimination:
De Morgan's laws
The negation of conjunction rule may be written in sequent notation:
The negation of disjunction rule may be written as:
De Morgan's duality can be generalised to quantifiers, the universal quantifier and existential quantifier are duals:
Rules of propositional calculus
https://en.wikipedia.org/wiki/Propositional_calculus
Negation introduction
Negation elimination
Double negative elimination
Conjunction introduction
Conjunction elimination and
Disjunction introduction and
Disjunction elimination
Biconditional introduction From and infer
Biconditional elimination and
Modus ponens (conditional elimination) From p and (p\to q), infer q.
Conditional proof (conditional introduction) From, assumption that allows a proof of , infer
Last updated
Was this helpful?