---

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


1. [fmla] : mFOL()
2. mFOL-proveable(<[], fmla>)@i
3. mFOL-sequent-evidence(<[], fmla>)
4. [Dom] : Type
5. [S] : FOStruct(Dom)
6. a : FOAssignment(Dom)@i
⊢ 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>)@i
3. [Dom] : Type
4. [S] : FOStruct(Dom)
5. a : FOAssignment(Dom)@i
6. ∩S:FOStruct(Dom). ∀a:FOAssignment(Dom). Dom,S,a |= mFOL-sequent-abstract(<[], fmla>)
7. Dom,S,a |= mFOL-sequent-abstract(<[], fmla>)
⊢ Dom,S,a |= mFOL-abstract(fmla)

---

Latex:



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


By

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

---

Home Index