Nuprl Definition : K-forces
K-forces(K;fmla) ==
mFOL_ind(fmla;
mFOatomic(R,vars)⇒ λi,a. i,a |= R(vars);
mFOconnect(knd,a,b)⇒ frca,frcb.if knd =a "and" then λi,a. ((frca i a) ∧ (frcb i a))
if knd =a "or" then λi,a. ((frca i a) ∨ (frcb i a))
else λi,a. ∀j:{j:World| i ≤ j} . ((frca j a) ⇒ (frcb j a))
fi ;
mFOquant(isall,z,body)⇒ frcbody.if isall
then λi,a. ∀j:{j:World| i ≤ j} . ∀v:Dom(j). (frcbody j a[z := v])
else λi,a. ∃v:Dom(i). (frcbody i a[z := v])
fi )
Definitions occuring in Statement :
K-sat: i,a |= fmla,
K-dom: Dom(i),
K-le: i ≤ j,
K-world: World,
mFOL_ind: mFOL_ind,
mFOatomic: name(vars),
update-assignment: a[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
token: "$token"
Definitions occuring in definition :
mFOL_ind: mFOL_ind,
K-sat: i,a |= fmla,
mFOatomic: name(vars),
and: P ∧ Q,
eq_atom: x =a y,
token: "$token",
or: P ∨ Q,
implies: P ⇒ Q,
ifthenelse: if b then t else f fi ,
set: {x:A| B[x]} ,
K-world: World,
K-le: i ≤ j,
all: ∀x:A. B[x],
lambda: λx.A[x],
exists: ∃x:A. B[x],
K-dom: Dom(i),
apply: f a,
update-assignment: a[x := v]
FDL editor aliases :
K-forces
Latex:
K-forces(K;fmla) ==
mFOL\_ind(fmla;
mFOatomic(R,vars){}\mRightarrow{} \mlambda{}i,a. i,a |= R(vars);
mFOconnect(knd,a,b){}\mRightarrow{} frca,frcb.if knd =a "and" then \mlambda{}i,a. ((frca i a) \mwedge{} (frcb i a))
if knd =a "or" then \mlambda{}i,a. ((frca i a) \mvee{} (frcb i a))
else \mlambda{}i,a. \mforall{}j:\{j:World| i \mleq{} j\} . ((frca j a) {}\mRightarrow{} (frcb j a))
fi ;
mFOquant(isall,z,body){}\mRightarrow{} frcbody.if isall
then \mlambda{}i,a. \mforall{}j:\{j:World| i \mleq{} j\} . \mforall{}v:Dom(j). (frcbody j a[z := v])
else \mlambda{}i,a. \mexists{}v:Dom(i). (frcbody i a[z := v])
fi )
Date html generated:
2019_10_16-AM-11_45_03
Last ObjectModification:
2018_10_15-PM-06_38_13
Theory : minimal-first-order-logic
Home
Index