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, nat: ℕ, product: x:A × B[x], atom: Atom
Definitions occuring in definition : atom: Atom, list: T List, product: x:A × B[x], nat: ℕ
FDL editor aliases : mfol-context-model

Latex:
mfol-context-model() == (\mBbbN{} \mtimes{} Atom \mtimes{} \mBbbN{} \mtimes{} \mBbbN{}) List \mtimes{} ((\mBbbN{} \mtimes{} ((\mBbbN{} \mtimes{} \mBbbN{}) List)) List) Date html generated: 2016_07_08-PM-05_26_41 Last ObjectModification: 2015_09_24-PM-02_21_52 Theory : minimal-first-order-logic Home Index