Nuprl Definition : mFOL-sequent-abstract

The abstract meaning of a sequent is a function
from the tuple of abstract meanings of the hypotheses to
the abstract meaning of the conclusion.⋅
mFOL-sequent-abstract(s) ==
  let hyps,concl = s 
  in λDom,S,a. (tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps)) ─→ Dom,S,a |= mFOL-abstract(concl))


Definitions occuring in Statement :  mFOL-abstract: mFOL-abstract(fmla),  FOSatWith: Dom,S,a |= fmla,  tuple-type: tuple-type(L),  map: map(f;as),  lambda: λx.A[x],  function: x:A ─→ B[x],  spread: spread def
FDL editor aliases :  mFOL-sequent-abstract
mFOL-sequent-abstract(s)  ==
    let  hyps,concl  =  s 
    in  \mlambda{}Dom,S,a.  (tuple-type(map(\mlambda{}h.Dom,S,a  |=  mFOL-abstract(h);hyps))
                            {}\mrightarrow{}  Dom,S,a  |=  mFOL-abstract(concl))


Date html generated: 2015_07_17-AM-07_56_29
Last ObjectModification: 2012_09_11-PM-05_45_32

Home Index