Nuprl Definition : K-uforces
K-uforces(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:World]. (frca j a) ⇒ (frcb j a) supposing i ≤ j
fi ;
mFOquant(isall,z,body)⇒ frcbody.if isall
then λi,a. ∀[j:World]. ∀v:Dom(j). (frcbody j a[z := v]) supposing i ≤ j
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,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
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 ,
uall: ∀[x:A]. B[x],
K-world: World,
uimplies: b supposing a,
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-uforces
Latex:
K-uforces(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:World]. (frca j a) {}\mRightarrow{} (frcb j a) supposing i \mleq{} j
fi ;
mFOquant(isall,z,body){}\mRightarrow{} frcbody.if isall
then \mlambda{}i,a. \mforall{}[j:World]. \mforall{}v:Dom(j). (frcbody j a[z := v]) supposing i \mleq{} j
else \mlambda{}i,a. \mexists{}v:Dom(i). (frcbody i a[z := v])
fi )
Date html generated:
2019_10_16-AM-11_45_28
Last ObjectModification:
2018_10_16-AM-10_42_38
Theory : minimal-first-order-logic
Home
Index