---

Step * 1 12 1 1 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. hypnum : ℕ@i
5. z : ℤ@i
6. ¬(z ∈ mFOL-freevars(concl))
7. hypnum < ||hyps||
8. (∀h∈hyps.¬(z ∈ mFOL-freevars(h)))
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = ff
11. [Dom] : Type
12. [S] : FOStruct(Dom)
13. a : FOAssignment(Dom)@i
14. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
15. B : mFOL()@i
16. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()@i
17. y : ℤ@i
18. mFOquant-var(hyps[hypnum]) = y ∈ ℤ@i
19. mFOL-sequent-evidence(<[B[z/y] / hyps], concl>)@i'
20. hyps[hypnum] = ∃y;B) ∈ mFOL()@i
⊢ Dom,S,a |= mFOL-abstract(concl)
BY
{ Assert ⌈∃d:Dom. Dom,S,a[y := d] |= mFOL-abstract(B)⌉⋅ }

1
.....assertion..... 
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. hypnum : ℕ@i
5. z : ℤ@i
6. ¬(z ∈ mFOL-freevars(concl))
7. hypnum < ||hyps||
8. (∀h∈hyps.¬(z ∈ mFOL-freevars(h)))
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = ff
11. [Dom] : Type
12. [S] : FOStruct(Dom)
13. a : FOAssignment(Dom)@i
14. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
15. B : mFOL()@i
16. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()@i
17. y : ℤ@i
18. mFOquant-var(hyps[hypnum]) = y ∈ ℤ@i
19. mFOL-sequent-evidence(<[B[z/y] / hyps], concl>)@i'
20. hyps[hypnum] = ∃y;B) ∈ mFOL()@i
⊢ ∃d:Dom. Dom,S,a[y := d] |= mFOL-abstract(B)

2
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. hypnum : ℕ@i
5. z : ℤ@i
6. ¬(z ∈ mFOL-freevars(concl))
7. hypnum < ||hyps||
8. (∀h∈hyps.¬(z ∈ mFOL-freevars(h)))
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = ff
11. [Dom] : Type
12. [S] : FOStruct(Dom)
13. a : FOAssignment(Dom)@i
14. tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps))@i
15. B : mFOL()@i
16. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()@i
17. y : ℤ@i
18. mFOquant-var(hyps[hypnum]) = y ∈ ℤ@i
19. mFOL-sequent-evidence(<[B[z/y] / hyps], concl>)@i'
20. hyps[hypnum] = ∃y;B) ∈ mFOL()@i
21. ∃d:Dom. Dom,S,a[y := d] |= mFOL-abstract(B)
⊢ Dom,S,a |= mFOL-abstract(concl)

---

Latex:



1.  hyps  :  mFOL()  List@i
2.  concl  :  mFOL()@i
3.  subgoals  :  mFOL-sequent()  List@i
4.  hypnum  :  \mBbbN{}@i
5.  z  :  \mBbbZ{}@i
6.  \mneg{}(z  \mmember{}  mFOL-freevars(concl))
7.  hypnum  <  ||hyps||
8.  (\mforall{}h\mmember{}hyps.\mneg{}(z  \mmember{}  mFOL-freevars(h)))
9.  \muparrow{}mFOquant?(hyps[hypnum])
10.  mFOquant-isall(hyps[hypnum])  =  ff
11.  [Dom]  :  Type
12.  [S]  :  FOStruct(Dom)
13.  a  :  FOAssignment(Dom)@i
14.  tuple-type(map(\mlambda{}h.Dom,S,a  |=  mFOL-abstract(h);hyps))@i
15.  B  :  mFOL()@i
16.  mFOquant-body(hyps[hypnum])  =  B@i
17.  y  :  \mBbbZ{}@i
18.  mFOquant-var(hyps[hypnum])  =  y@i
19.  mFOL-sequent-evidence(<[B[z/y]  /  hyps],  concl>)@i'
20.  hyps[hypnum]  =  \mexists{}y;B)@i
\mvdash{}  Dom,S,a  |=  mFOL-abstract(concl)


By

Assert  \mkleeneopen{}\mexists{}d:Dom.  Dom,S,a[y  :=  d]  |=  mFOL-abstract(B)\mkleeneclose{}\mcdot{}

---

Home Index