Biçimsel kanıt örnekleri
David Pierce
Aralık
Gözden geçirilmiş Aralık
Problem . P ↔ Q gerektirir P → Q.
Kanıt.
. P ↔ Q hipotez
. (P → Q) ∧ (Q → P ) ()’e denk
. P → Q ()’den basitleştirme ile Problem . P ∨ Q → R gerektirir P → R.
Kanıt.
. P ∨ Q → R hipotez
. ¬(P ∨ Q) ∨ R ()’e denk
. (¬P ∧ ¬Q) ∨ R ()’den De Morgan ile
. (¬P ∨ R) ∧ (¬Q ∨ R) ()’ten dağılma ile
. ¬P ∨ R ()’ten basitleştirmeyle
. P → R ()’ten
Aralık , :
Problem . P ↔ Q ∨ R gerektirir R → P . Kanıt.
. P ↔ Q ∨ R hipotez
. (P → Q ∨ R) ∧ (Q ∨ R → P )
. Q ∨ R → P basitleştirme
. ¬(Q ∨ R) ∨ P
. (¬Q ∧ ¬R) ∨ P
. (¬Q ∨ P ) ∧ (¬R ∨ P )
. ¬R ∨ P basitleştirme
. R → P
Problem . P → Q gerektirir P → Q ∨ R.
Kanıt.
. P → Q hipotez
. ¬P ∨ Q
. (¬P ∨ Q) ∨ R ekleme
. ¬P ∨(Q ∨ R)
. P → Q ∨ R
Problem . P → Q ve P → R gerektirir P → Q ∧ R.
Kanıt.
. P → Q hipotez
. P → R hipotez
. (P → Q) ∧ (P → R) bağlama
. (¬P ∨ Q) ∧ (¬P ∨ R)
. ¬P ∨(Q ∧ R)
. P →(Q ∧ R)
Aralık , :
Problem . P → Q ve P → Q → R gerektirir P → R.
Kanıt.
. P → Q → R hipotez
. ¬P ∨(Q → R)
. ¬P ∨(¬Q ∨ R)
. (¬Q ∨ ¬P ) ∨ R
. (1 ∧ (¬Q ∨ ¬P )) ∨ R
. (P ∨ ¬P ) ∧ (¬Q ∨ ¬P )
∨R
. (P ∧ ¬Q) ∨ ¬P
∨R yutma
. (¬¬P ∧ ¬Q) ∨ ¬P ∨ R
. ¬(¬P ∨ Q) ∨ (P → R)
. (¬P ∨ Q) → (P → R)
. (P → Q) → (P → R)
. P → Q hipotez
. P → R ayırma
veya
. P → Q hipotez
. P → Q → R hipotez
. (P → Q) ∧ (P → Q → R) bağlama
. (¬P ∨ Q) ∧ (¬P ∨ ¬Q ∨ R)
. ¬P ∨(Q ∧ (¬Q ∨ R))
. ¬P ∨(Q ∧ R)
. (¬P ∨ Q) ∧ (¬P ∨ R)
. ¬P ∨ R basitleştirme
. P → R
Aralık , :
Problem . P ↔ Q ve P → R gerektirir Q → R.
Kanıt.
. P ↔ Q hipotez
. Q → P [basitleştirme]
. P → R hipotez
. Q → R hipotetik tasım
Problem . P ↔ Q ∨ R ve P → S gerektirir Q → S.
Kanıt.
. P ↔ Q ∨ R hipotez
. Q ∨ R → P [basitleştirme]
. ¬(Q ∨ R) ∨ P
. (¬Q ∧ ¬R) ∨ P
. (¬Q ∨ P ) ∧ (¬R ∨ P )
. ¬Q ∨ P basitleştirme
. Q → P
. P → S hipotez
. Q → S hipotetik tasım
