Nuprl Definition : FOL-sequent-abstract
FOL-sequent-abstract(s) ==
let hyps,concl = s
in λDom,S,a. (tuple-type(FOL-hyps-meaning(Dom;S;a;hyps)) ⟶ Dom,S,a +|= FOL-abstract(concl))
Definitions occuring in Statement :
FOL-hyps-meaning: FOL-hyps-meaning(Dom;S;a;hyps),
FOL-abstract: FOL-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),
FOL-hyps-meaning: FOL-hyps-meaning(Dom;S;a;hyps),
FOSatWith+: Dom,S,a +|= fmla,
FOL-abstract: FOL-abstract(fmla)
FDL editor aliases :
FOL-sequent-abstract
Latex:
FOL-sequent-abstract(s) ==
let hyps,concl = s
in \mlambda{}Dom,S,a. (tuple-type(FOL-hyps-meaning(Dom;S;a;hyps)) {}\mrightarrow{} Dom,S,a +|= FOL-abstract(concl))
Date html generated:
2016_05_15-PM-10_27_02
Last ObjectModification:
2015_09_23-AM-08_25_32
Theory : minimal-first-order-logic
Home
Index