phl245 derivation rules

Modus Ponens (MP)

from P→Q and P, infer Q

for conditional: If I have the antecedent, I can infer the consequent

Modus Tollens (MT)

from P→Q and ~Q, infer ~P

for conditional: If i have the negation of the consequent, I can infer the antecedent

Double Negation (DN)

From P, infer ~~P. From ~~P, infer P.

Repetition (R)

From P, infer P.

Simplification (S)

From P∧Q, infer P or Q

Adjunction (ADJ)

From P and Q, infer P∧Q

Addition (ADD)

From P, infer P∨Q

Modus Tollendo Ponens (MTP)

From P∨Q and ~P, infer Q. From P∨Q and ~Q, infer P.

Biconditional-conditional (BC)

From P↔Q, infer P→Q and Q→P

Conditional-biconditional (CB)

From P→Q and Q→P, infer P↔Q

Negation of Conditional (NC)

~(P→Q) = P∧~Q

Negation of the biconditional (NB)

~(P↔Q) = (P∧~Q)∨(~P∧Q)

De Morgens (DM)

~(P∧Q) = ~P∨~Q

~(P∨Q) = ~P∧~Q

Universal Instantiation (UI)

From ∀x P(x), infer P(a)

Existenial Instantiation (EI)

From ∃x P(x), infer P(c) —> has to be a new variable i-z!!!!!

Existential Generalization (EG)

From P(a), infer ∃x P(x)

Quantifier Negation

¬∀x P(x) ≡ ∃x ¬P(x); ¬∃x P(x) ≡ ∀x ¬P(x)