Rules

[Hughes and Cresswell, 1996]

Rule List

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<=>B (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)

Go to ...

• Logic Systems Page
• Axioms Page
• Structures Page
• Logic Page
• John Halleck's home page

© 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 June 27th, 2007.