Nuprl Definition : mfol-context-model

A pair <consts,funs> where consts is an association list that can assign
number n a triple such as ⌈<"pair", i, j>⌉.
funs is an association list of type ⌈(ℤ × ((ℤ × ℤ) List)) List⌉.
It can assign to number n a secondary association list.
So if 0 is assigned the list [<1,4>;<2;5>] it means that
0 is a function that maps domain element 1 to hypothesis 4 and
domain element 2 to hypothesis 5⋅

mfol-context-model() == (ℤ × Atom × ℤ × ℤ) List × ((ℤ × ((ℤ × ℤ) List)) List)

Definitions occuring in Statement : list: T List, product: x:A × B[x], int: ℤ, atom: Atom
FDL editor aliases : mfol-context-model
mfol-context-model() == (\mBbbZ{} \mtimes{} Atom \mtimes{} \mBbbZ{} \mtimes{} \mBbbZ{}) List \mtimes{} ((\mBbbZ{} \mtimes{} ((\mBbbZ{} \mtimes{} \mBbbZ{}) List)) List) Date html generated: 2015_07_17-AM-07_57_32 Last ObjectModification: 2014_06_13-PM-06_10_26 Home Index