inference rule (introduction of conjunction (∧Intro))
From φ and ψ infer φ ∧ ψ.
Applications of the rule looks like this:
φ
ψ
_____
φ ∧ ψ
Inference Rule (elimination of conjunction 1 (∧Elim1))
From φ ∧ ψ infer φ.
Inference Rule (elimination of conjunction 2 (∧Elim2))
From φ ∧ ψ infer ψ.
Inference Rule (elimination of conjunction 1 (∧Elim1))
From φ ∧ ψ infer φ. Applications of this rule look as follows: φ ∧ ψ \_\_\_\_\_ φ
Inference Rule (elimination of conjunction 2 (∧Elim2))
From φ ∧ ψ infer ψ. Applications of this rule look as follows: φ ∧ ψ \_\_\_\_\_ ψ
Example ((P → R3), Q, R ` (P → R3) ∧ Q ∧ R)
- P → R3 - premise
- Q - premise
- R - premise
- (P → R3) ∧ Q - ∧Intro 1,2
- (P → R3) ∧ Q ∧ R - ∧Intro 3,4
- We write down the premises.
- We infer the conjunction of previous steps using ∧Intro.
- We infer the conjunction of previous steps using ∧Intro again.
- We have a proof of (P → R3) ∧ Q ∧ R from our three premises:
(P → R3), Q, and R.
Example ((P ∨ Q) ∧ (R ∨ Q) ` R ∨ Q)
- (P ∨ Q) ∧ (R ∨ Q) - premise
- R ∨ Q - ∧Elim2 1
- We write down the premise.
- We infer the right conjunct using ∧Elim2.
- We have a proof of R ∨ Q from our premise (P ∨ Q) ∧ (R ∨ Q)
Example (P ∧ Q, R ` Q ∧ R)
- P ∧ Q - premise
- R - premise
- Q - ∧Elim2 1
- Q ∧ R - ∧Intro 2,3
Inference Rule (introduction of the conditional (→Intro))
From ψ and the assumption that φ infer φ → ψ and discharge this assumption.
Applications of the rule looks like this:
φ
ψ
______
φ → ψ
→Intro
→Intro is a rule of inference that requires an assumption that needs to be discharged when we apply the rule.
- This assumption is always the antecedent of the introduced conditional.
- We indicate that an assumption has been discharged and where by enclosing all steps between the assumption and the last step before the discharge in a left square bracket.
- The list of sentences wrapped around the square bracket is a closed subproof. A sentence φ is available in a step of a proof if it occurs before this step outside all closed subproofs.
Example (P ∧ Q ` R → P ∧ R)
- P ∧ Q = premise
- R = assumption
- P = ∧Elim1 1
- P ∧ R = ∧Intro 2,3
- R → P ∧ R = →Intro 2,4
- We write down our premise.
- We assume the antecedent of the conditional we want to prove.
- We infer the left conjunct using ∧Elim1.
- We infer the consequent using ∧Intro.
- We infer the conditional that has our assumption that R as antecedent and a sentence we derived as
the consequent and discharge our assumption of the antecedent by →Intro.
- We have a proof of R → P ∧ R from our premise, P ∧ Q.
Inference Rule (elimination of the conditional (→Elim))
From φ and φ → ψ infer ψ. Applications of the rule looks like this: φ φ → ψ \_\_\_\_\_ ψ
Example ((P ∨ Q) ∧ (R → Q), R ` Q)
- (P ∨ Q) ∧ (R → Q) = premise
- R = premise
- R → Q = ∧Elim2 1
- Q = →Elim 2,3
Inference Rule (introduction of disjunction 1 (∨Intro1))
From φ infer φ ∨ ψ.
Inference Rule (introduction of disjunction 2 (∨Intro2))
From ψ infer φ ∨ ψ.
Example (¬P ∧ Q, Q ∨ R → ¬R5 ` P ∨ ¬R5)
- ¬P ∧ Q = premise
- Q ∨ R → ¬R5 =premise
- Q = ∧Elim2 1
- Q ∨ R = ∨Intro1 3
- ¬R5 = →Elim 2,4
- P ∨ ¬R5 = ∨Intro2 5
Inference Rule (elimination of disjunction (∨Elim))
From φ ∨ ψ, φ → χ, and ψ → χ infer χ.
applications of this rule look like this:
φ ∨ ψ
φ → χ
ψ → χ
\_\_\_\_\_
χfurther explanation of elimination of disjunction (VElim)
From a disjunction, i.e. of the form ‘A or B’, one cannot simply infer A or infer B.
What one can do is show that from each A and B a third claim, C, follows.
Thus, either way, C will be true.
Example (P ∨ Q, P → Q, Q → R ` R)
- P ∨ Q premise
- P → Q premise
- Q → R premise
- P assumption
- Q →Elim 2,4
- R →Elim 3,5
- P → R →Intro 4,6
- R ∨Elim 1,3,7
We write down all our premises.
We assume the first disjunct of the disjunction we want to eliminate.
We infer Q using →Elim.
We infer R using →Elim.
We infer P → R using →Intro and discharge P.
We infer R using ∨Elim
Example (R ∨ Q, R → Q ` Q)
- R ∨ Q premise
- R → Q premise
- Q assumption
- Q → Q →Intro 3
- Q ∨Elim 1,2,4
