Regular Derivations
Solve this derivation
{ Fa, Ja → ~Fa, Ma ↔ Ja } |– ~Ma
arrow: horseshoe
double-arrow: triple bar
1. Fa P
2. Ja → ~Fa P
3. Ma ↔ Ja P
4. Ma A
5. Ja 3,4, ↔E
6. ~Fa 2,5, →E
7. Fa & ~Fa 1,6, &I
8. ~Ma 4-7, ~I
Complete the derivation:
1. {(Ajj → Bc)} Ajj → (Bc ◦ Gh)
arrow: horseshoe
circle: wedge
1. Ajj → Bc P
2. Ajj A
3. Bc 1,2, →E
4. Bc ◦ Gh 3, ◦I
5. Ajj → (Bc ◦ Gh) 2-4, →I
Solve the theorem
(Ga&Fb)→(Ja→Fb)
arrow:horseshoe
1. Ga & Fb A
2. Ja A
3. Fb 1, &E
4. Ja → Fb 2-3, →I
5. (Ga&Fb)→(Ja→Fb) 1-4, →I
solve this derivation
{ Fa & Gb, (Jd o Ha) → ~Db } |– ( Fa → Ha ) → ~Db
circle: wedge
arrow: horseshoe
1. Fa & Gb P
2. (Jd o Ha) → ~Db P
3. Fa → Ha A
4. Fa 1, &E
5. Ha 3,4, →E
6. Jd o Ha 5, oI
7. ~Db 2,6, →E
8. ( Fa → Ha ) → ~Db 3-7, →I
Complete the derivation:
4. {(Bg → Jg)} (Bg → (Hg → Jg))
arrow: horseshoe
1. Bg → Jg P
2. Bg A
3. Hg A
4. Jg 1,2, →E
5. Hg → Jg 3-4, →I
6. Bg → (Hg → Jg) 2-5,
Solve the theorem:
Hb → (Ja → (Ja → Hb))
arrow: horseshoe
1. Hb A
2. Ja A
3. Ja A
4. Hb 1, R
5. Ja → Hb 3-4, →I
6. Ja → (Ja → Hb) 2-5, →I
7. Hb → (Ja → (Ja → Hb)) 1-6, →I
solve this derivation
{ ~Ab, (Jf o Fa) → Ab} |– ~Fa
circle: wedge
arrow: horseshoe
1. ~Ab P
2. (Jf o Fa) → Ab P
3. Fa A
4. Jf o Fa 3, oI
5. Ab 2,4, →E
6. Ab & ~Ab 1,5, &I
7. ~Fa 3-6, ~I
Complete the derivation
{(F a → (Ka & Ba)),(Ka → ∼Ba)} ∼Fa
Arrow: horseshoe
1. F a → (Ka & Ba) P
2. Ka → ∼Ba P
3. F a A
4. Ka & Ba 1,3, →E
5. Ka 4, &E
6. ∼Ba 2,5, →E
7. Ba 4, &E
8. Ba & ∼Ba 6,7, &I
9. ∼F a 3-8 ∼I
Solve the theorem:
∼Fa → (Fa → Gb)
1. ~Fa A
2. Fa A
3. ~Gb A
4. Fa & ~Fa 1, 2, &I
5. ~ ~Gb 3-4, ~I
6. Gb 5, ~E
7. Fa → Gb 2-6, →I
8. ∼Fa → (Fa → Gb) 1-7, →I
Solve this derivation:
{ ~(Ha & Ba), ~Ha → Jd } |– Ba → Jd
arrow: horseshoe
1. ~(Ha & Ba) P
2. ~Ha → Jd P
3. Ba A
4. Ha A
5. Ha & Ba 3,4, &I
6. (Ha & Ba) & ~(Ha & Ba) 1,5, &I
7. ~Ha 4-6, ~I
8. Jd 2,7, →E
9. Ba → Jd 3-8, →I
Complete the derivation:
{(Ha → Jk),(Jk ↔ ∼Ab)} ∼(Ha & Ab)
arrow: horseshoe
double arrow: triple bar
1. Ha → Jk P
2. Jk ↔ ∼Ab P
3. Ha & Ab A
4. Ha 3, &E
5. Jk 1,4, →E
6. ∼Ab 2,5, ↔E
7. Ab 3, &E
8. Ab & ∼Ab 6,7, &I
9. ∼(Ha & Ab) 3-8, ∼I
Solve the theorem:
∼[(Eb & (Gb ↔ Eb)) & ∼Gb]
double arrow: triple bar
1. (Eb & (Gb ↔ Eb)) & ∼Gb A
2. Eb & (Gb ↔ Eb) 1, &E
3. Eb 2, &E
4. Gb ↔ Eb 2, &E
5. Gb 3, 4, ↔E
6. ~Gb 1, &E
7. Gb & ~Gb 5, 6, &I
8. ∼[(Eb & (Gb ↔ Eb)) & ∼Gb] 1-7, ~I
Solve this derivation
{ Jd o Ld, Ld → Kd, Kd → Jd } |– Jd
circle: wedge
arrow: horseshoe
1. Jd o Ld P
2. Ld → Kd P
3. Kd → Jd P
4. Jd A
5. Jd → Jd 4-4, →I
6. Ld A
7. Kd 2,6, →E
8. Jd 3,7, →E
9. Ld → Jd 6-8, →E
10. Jd 1,5,9, oE
Complete the derivation:
{((F a → F a) → F a),(Gb → ∼F a)} ∼Gb
arrow: horseshoe
1. (F a → F a) → F a P
2. Gb → ∼F a P
3. Gb A
4. F a A
5. F a → F a 4-4, →I
6. F a 1,5, →E
7. ∼F a 2,3, →E
8. F a & ∼F a 6,7, &I
9. ∼Gb 3-8, ∼I
Solve theorem
∼Hd → (Fg → ∼(Fg → Hd))
arrow: horseshoe
1. ~Hd A
2. Fg A
3. Fg → Hd A
4. Hd 2, 3, →E
5. Hd & ~Hd 1, 4, ~I
6. ~(Fg → Hd) 3-5, ~I
7. Fg → ~(Fg → Hd) 2-6, →I
8. ∼Hd → (Fg → ∼(Fg → Hd)) 1-7, →I