Derivation Systems for Propositional and Predicate Logics: Philosophy Forums

Philosophy Forums » Logic and Philosophy of Math » Logic Homework » Derivation Systems for Propositional and Predicate Logics » Derivation Systems for Propositional and Predicate Logics

Derivation Systems for Propositional and Predicate Logics

Derivation Systems for Propositional and Predicate Logics

AKG
Tenured Poster

Usergroup: Members
Joined: Jan 15, 2004
Location: Berkeley, CA
Total Topics: 87
Total Posts: 3325

1 of 1 people found this post helpful
Posted 01/05/06 - 11:26 PM:
Subject: Derivation Systems for Propositional and Predicate Logics

There are numerous derivation systems, here are some, from "The Logic Book" by Merrie Bergmann.

First, some notation:

For rules of inference, I will use the notation <{P₁, ..., P_n}, C> to say that given P₁, ..., P_n, you may infer C.

For rules of replacement, I will use the notation P <> Q to say that P and Q are interchangeable.

SD

Reiteration (R): <{P}, P>
Conjunction Introduction (&I): <{P, Q}, P&Q>
Conjunction Elimination (&E): <{P&Q}, P> or <{P&Q}, Q>
Conditional Introduction (→I): If you assume P, and derive Q within the scope of assumption P, then you may infer P→Q just outside the scope of the assumption P
Conditional Elimination (→E): <{P→Q, P}, Q>
Negation Introduction (~I): If you assume P, and derive both Q and ~Q (for any sentence Q) within the scope of assumption P, you may infer ~P just outside the scope of assumption P
Negation Elimination (~E): If you assume ~P, and derive both Q and ~Q (for any sentence Q) within the scope of assumption ~P, you may infer P just outside the scope of assumption ~P
Disjunction Introduction (vI): <{P}, PvQ> or <{P}, QvP>, for any Q
Disjunction Elimination (vE): <{PvQ, P→R, Q→R}, R>
Biconditional Introduction (≡I): <{P→Q, Q→P}, P≡Q>
Biconditional Elimination (≡E): <{P≡Q, P}, Q> or <{P≡Q, Q}, P>

SD+

All the rules of SD plus three extra rules of inference:

Modus Tollens (MT): <{P→Q, ~Q}, ~P>
Hypothetical Syllogism (HS): <{P→Q, Q→R}, P→R>
Disjunctive Syllogism (DS): <{PvQ, ~P}, Q> or <{PvQ, ~Q}, P>

and 10 rules of replacement:

Commutation (Com): P&Q <> Q&P, and PvQ <> QvP
Association (Assoc): P&(Q&R) <> (P&Q)&R, and Pv(QvR) <> (PvQ)vR
Implication (Impl): P→Q <> ~PvQ
Double Negation (DN): P <> ~~P
De Morgan (DM): ~(P&Q) <> ~Pv~Q, and ~(PvQ) <> ~P&~Q
Idempotence (Idem): P <> P&P, and P <> PvP
Transposition (Trans): P→Q <> ~Q→~P
Exportation (Exp): P→(Q→R) <> (P&Q)→R
Distribution (Dist): P&(QvR) <> (P&Q)v(P&R), and Pv(Q&R) <> (PvQ)&(PvR)
Equivalence (Equiv): P≡Q <> (P→Q)&(Q→P), and P≡Q <> (P&Q)v(~P&~Q)

PD

All the rules of SD, plus four extra rules of inference:

Universal Introduction (∀I): <{P(a/x)}, (∀x)P>, provided that a does not occur in an undischarged assumption, and a does not occur in (∀x)P
Universal Elimination (∀E): <{(∀x)P}, P(a/x)>, for any a
Existential Introduction (∃I): <{P(a/x)}, (∃x)P>, for any a
Existential Elimination (∃E): <{(∃x)P, P(a/x)→Q}, Q> provided that a does not occur in an undischarged assumption, a does not occur in (∃x)P, and a does not occur in Q

PD+

All the rules of SD+ and PD, plus a rule of replacement:

Quantifier Negation (QN): ~(∀x)P <> (∃x)~P, and ~(∃x)P <> (∀x)~P

"The only reason we die... is because we accept it as an inevitability." -- Stewie

"To enslave nuance to dogma is folly." -- Lord Hillyer

This thread is closed, so you cannot post a reply.