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(mFOL-hyps-meaning(Dom;S;a;hyps)) ⟶ Dom,S,a |= mFOL-abstract(concl))

Definitions occuring in Statement : mFOL-hyps-meaning: mFOL-hyps-meaning(Dom;S;a;hyps), mFOL-abstract: mFOL-abstract(fmla), FOSatWith: Dom,S,a |= fmla, tuple-type: tuple-type(L), lambda: λx.A[x], function: x:A ⟶ B[x], spread: spread def
Definitions occuring in definition : spread: spread def, lambda: λx.A[x], function: x:A ⟶ B[x], tuple-type: tuple-type(L), mFOL-hyps-meaning: mFOL-hyps-meaning(Dom;S;a;hyps), FOSatWith: Dom,S,a |= fmla, mFOL-abstract: mFOL-abstract(fmla)
FDL editor aliases : mFOL-sequent-abstract

Latex:
mFOL-sequent-abstract(s) == let hyps,concl = s in \mlambda{}Dom,S,a. (tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps)) {}\mrightarrow{} Dom,S,a |= mFOL-abstract(concl)) Date html generated: 2016_07_08-PM-05_21_04 Last ObjectModification: 2015_09_23-AM-08_25_29 Theory : minimal-first-order-logic Home Index