Nuprl Definition : mFO_uniform_evidence
mFO_uniform_evidence{i:l}(fmla) == ⋂Dom:Type. ⋂S:FOStruct(Dom). ∀a:ℤ ⟶ Dom. Dom,S,a |= fmla
Definitions occuring in Statement :
FOSatWith: Dom,S,a |= fmla,
FOStruct: FOStruct(Dom),
all: ∀x:A. B[x],
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
universe: Type
Definitions occuring in definition :
universe: Type,
isect: ⋂x:A. B[x],
FOStruct: FOStruct(Dom),
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
FOSatWith: Dom,S,a |= fmla
FDL editor aliases :
mFO_uniform_evidence
Latex:
mFO\_uniform\_evidence\{i:l\}(fmla) == \mcap{}Dom:Type. \mcap{}S:FOStruct(Dom). \mforall{}a:\mBbbZ{} {}\mrightarrow{} Dom. Dom,S,a |= fmla
Date html generated:
2019_10_16-AM-11_38_54
Last ObjectModification:
2018_10_14-PM-04_50_23
Theory : minimal-first-order-logic
Home
Index