Philosophy Forums
Forums Links Articles Gallery Chat
Style:



Register | Forgot Password

Derivation Systems for Propositional and Predicate Logics

printPrint
locked


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
quote post
#1
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 <{P1, ..., Pn}, C> to say that given P1, ..., Pn, 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
Download thread as
locked


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

4 total queries
This page was created in 0.42 seconds
Memory used: 2579728 bytes
Server Status: time since last reboot is 150 days, 22:58, load average: 2.01, 1.73, 1.53