---

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


1. [fmla] : mFOL()
2. mFOL-proveable(<[], fmla>)
3. mFOL-sequent-evidence(<[], fmla>)
4. [Dom] : Type
5. [S] : FOStruct(Dom)
6. a : FOAssignment(mFOL-freevars(fmla),Dom)
⊢ Dom,S,a |= mFOL-abstract(fmla)
BY
{ (With ⌜Dom⌝ (D 3)⋅ THEN Auto THEN (InstHyp [⌜S⌝;⌜a⌝] (-1)⋅ THENA Auto)) }

1
1. [fmla] : mFOL()
2. mFOL-proveable(<[], fmla>)
3. [Dom] : Type
4. [S] : FOStruct(Dom)
5. a : FOAssignment(mFOL-freevars(fmla),Dom)
6. ⋂S:FOStruct(Dom). ∀a:FOAssignment(mFOL-sequent-freevars(<[], fmla>),Dom). Dom,S,a |= mFOL-sequent-abstract(<[], fmla>\000C)
7. Dom,S,a |= mFOL-sequent-abstract(<[], fmla>)
⊢ Dom,S,a |= mFOL-abstract(fmla)

---

Latex:

---

Latex:

1.  [fmla]  :  mFOL()
2.  mFOL-proveable(<[],  fmla>)
3.  mFOL-sequent-evidence(<[],  fmla>)
4.  [Dom]  :  Type
5.  [S]  :  FOStruct(Dom)
6.  a  :  FOAssignment(mFOL-freevars(fmla),Dom)
\mvdash{}  Dom,S,a  |=  mFOL-abstract(fmla)


By

---

Latex:
(With  \mkleeneopen{}Dom\mkleeneclose{}  (D  3)\mcdot{}  THEN  Auto  THEN  (InstHyp  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index