more from this thinker
|
more from this text
Single Idea 13524
[filed under theme 4. Formal Logic / B. Propositional Logic PL / 2. Tools of Propositional Logic / c. Derivation rules of PL
]
Full Idea
Deduction Theorem: If T ∪ {P} |- Q, then T |- (P → Q). This is the formal justification of the method of conditional proof (CPP). Its converse holds, and is essentially modus ponens.
Gist of Idea
Deduction Theorem: T∪{P}|-Q, then T|-(P→Q), which justifies Conditional Proof
Source
Robert S. Wolf (A Tour through Mathematical Logic [2005], 1.3)
Book Ref
Wolf,Robert S.: 'A Tour Through Mathematical Logic' [Carus Maths Monographs 2005], p.31
The
14 ideas
with the same theme
[basic rules used in proofs of propositional logic]:
|
9396
|
DN: Given A, we may derive ¬¬A
[Lemmon]
|
|
9393
|
A: we may assume any proposition at any stage
[Lemmon]
|
|
9399
|
∧E: Given A∧B, we may derive either A or B separately
[Lemmon]
|
|
9398
|
∧I: Given A and B, we may derive A∧B
[Lemmon]
|
|
9397
|
CP: Given a proof of B from A as assumption, we may derive A→B
[Lemmon]
|
|
9394
|
MPP: Given A and A→B, we may derive B
[Lemmon]
|
|
9401
|
∨E: Derive C from A∨B, if C can be derived both from A and from B
[Lemmon]
|
|
9402
|
RAA: If assuming A will prove B∧¬B, then derive ¬A
[Lemmon]
|
|
9395
|
MTT: Given ¬B and A→B, we derive ¬A
[Lemmon]
|
|
9400
|
∨I: Given either A or B separately, we may derive A∨B
[Lemmon]
|
|
13500
|
Conditional Proof: infer a conditional, if the consequent can be deduced from the antecedent
[Hart,WD]
|
|
14273
|
Conditional Proof is only valid if we accept the truth-functional reading of 'if'
[Edgington]
|
|
10987
|
Three traditional names of rules are 'Simplification', 'Addition' and 'Disjunctive Syllogism'
[Read]
|
|
13524
|
Deduction Theorem: T∪{P}|-Q, then T|-(P→Q), which justifies Conditional Proof
[Wolf,RS]
|