Standard rules used in the systems:

- US: Uniform substitution:
- EQ: Substitution of equivalents.
- EQ' (Substitution of proved strict equivalents)
- EQS: Substitution of strict equivalents.
- MP: Modus Ponens: Given |- A and |- A>B, infer |- B [Also called material detachment] Also called Modus Ponens for >
- MP=>: Strict Modus Ponens: Given |- A and |- A=>B, infer |- B [also called Strict detachment] Also called Modus Ponens for =>
- MT: Modus Tolens (From |- p>q, infer |- ~q>~p)
- MTR: Modus Tolens Reductiona (From |- ~p>~q, infer |- q>p
- N: Necessitation: Given |- A, infer |- LA
- N': if A is a tautology in PC, infer |- LA
- N'': If A is a Tautology in PC, infer |- A
- N'a: If A is a tautology in PC, or is an axiom, infer |- LA
- PC-Taut (Tautology Necessitation): If A is a tautology in PC, infer |- LA
- BR (Becker's Rule): Given |- L(A>B), infer |- LA>LB
- RE: Given |- a==b, infer |- La==Lb
- REM: Given |- a==b, infer |- Ma==Mb
- RS: Given |- A<=>B, infer |- LA<=>LB (This is the strict form of RE. Chellas calls this RE.)
- R*: Given |- A>B infer |- LA>LB
- AD (Adjunction): Given |- A, and |- B, |- infer A&B
- UQ (Universal Quantification): Given |- A containing a variable "a" not bound by any quantifier, infer |- (forall a, A)

© Copyright 2004 by John Halleck, All Rights Reserved.

This page is http://www.cc.utah.edu/~nahaj/logic/structures/rules/index.html

This page was last modified on November 10th, 2009.