20 – 22. PL Proofs

Question 1

Syntactic Validity

Answer 1

A) Notation: α1, . . . , αn ⊢ γ
B) Exists derivation: starts with α1, . . . , αn & ends with γ

Question 2

Rules of Proof System

Answer 2

A) Motivated by semantic considerations (Truth-preservation)
B) Deal with sentences regardless of truth or falsity
C) Pure Syntax, isolated from the world.

Question 3

RULES OF PROOF SYSTEM

Answer 3

A) 8 introduction and elimination rules:
Conjunction, Disjunction, Negation and Conditional
B) 1 special rule that is specific to classical PL
Double negation Elimination
C) 2 Non-necessary rules that make our life easy
Iteration and Explosion Rule

Question 4

Conjunction Introduction (∧I)

Answer 4

1) One can introduce a conjunction for any given WFF with any other WFF (even if not give?)
A) α… β … α ∧ β
B) β… α… α ∧ β

Semantic Justification: α, β ⊨ α ∧ β

Question 5

Conjunction Elimination (∧E)

Answer 5

1) Any conjunction can be separated as one of its WFF
A) α ∧ β… α
B) α ∧ β… β

Semantic Justification: α ∧ β ⊨ α

Question 6

Negation Introduction (Abs)

Answer 6

1) Absurdity rule (Abs)
2) Given wff’s α and ¬α, we can derive ⊥
3) Introduction rule for ⊥ Falsum
A) α… ¬α… ⊥
B) ¬α… α… ⊥

Sem. Justification: if Γ, α ⊨ ⊥ then Γ ⊨ ¬α

Question 7

Negation Elimination (RAA)

Answer 7

1) Reductio ad absurdum (RAA)
2) Given a subderrivation from α to ⊥, we can derive ¬α
3) Elimination rule for ⊥ Falsum
4) RAA and DN are often used together
A) [α|… ⊥…] ¬α In a [subderrivation] & Prem/Supp|

Sem. Justification: α, ¬α ⊨ ⊥

Question 8

Disjunction Introduction (∨I)

Answer 8

1) One can introduce a disjunction for any given WFF with any other WFF
A) α… α ∨ β
B) β… α ∨ β

Sem Justification: α ⊨ α ∨ β

Question 9

Disjunction Elimination (∨E)

Answer 9

1) If the two WFF in the conjunction have subderrivations with the same result we can derive it to the main derivation.
2)
A) α ∨ β… [α|…γ] … [β|…γ] …γ
B) α ∨ β… [β|…γ] … [α|…γ] …γ

Semantic Justification:
If Γ, α ⊨ γ and Γ, β ⊨ γ, then Γ, α ∨ β ⊨ γ

(Γ to abbreviate a list of wff’s)

Question 10

Conditional Introduction (→I / CP)

Answer 10

1) Conditional Proof rule
2) given a subderivation from α to γ, we can derive α → γ
A) [α|… γ]… α → γ

Sem. Justification: if Γ, α ⊨ γ, then Γ ⊨ α → γ

Question 11

Conditional Elimination (→E)

Answer 11

1) Modus Ponens
2) given wff’s α and α → γ, we can derive γ
A) α… α → γ… γ
B) α → γ… α… γ

Sem. Justification: α, α → γ ⊨ γ

Question 12

Double Negation (DN)

Answer 12

1) This rule shows ¬¬P ⊢ P
2) Not redundant, nor introductory, nor eliminatory
3) RAA and DN are often used together
A) ¬¬α… α

Sem. Justification: ¬¬α ⊨ α

Question 13

Iteration Rule (Iter)

Answer 13

A redundant rule, where a WFF can be reiterated yet it makes derivations a bit shorter
A) α… α
Sem. Justification: α ⊨ α

Question 14

Ex Falso Quodlibet (EFQ)

Answer 14

1) From falsum anything WFF can be introduced
2) This rule is redundant, but nevertheless useful
A) ⊥… α

Sem. Justification: ⊥ ⊨ α

Question 15

Good Book-Keeping

Answer 15

At a given line in a derivation:
A) the available wff’s are precisely the earlier wff’s which are not in a finished subderivation
B) the available subderivations are precisely the earlier finished subderivations which are not nested inside a finished subderivation