Nuprl Lemma : K_forces_quant_lemma
∀body,z,isall,K:Top.
(K-forces(K;mFOquant(isall;z;body)) ~ if isall
then λi,a. ∀j:{j:World| i ≤ j} . ∀v:Dom(j). (K-forces(K;body) j a[z := v])
else λi,a. ∃v:Dom(i). (K-forces(K;body) i a[z := v])
fi )
Proof
Definitions occuring in Statement :
K-forces: K-forces(K;fmla),
K-dom: Dom(i),
K-le: i ≤ j,
K-world: World,
mFOquant: mFOquant(isall;var;body),
update-assignment: a[x := v],
ifthenelse: if b then t else f fi ,
top: Top,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
K-forces: K-forces(K;fmla),
mFOquant: mFOquant(isall;var;body),
mFOL_ind: mFOL_ind,
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
inhabitedIsType,
hypothesisEquality,
universeIsType,
introduction,
extract_by_obid
Latex:
\mforall{}body,z,isall,K:Top.
(K-forces(K;mFOquant(isall;z;body)) \msim{} if isall
then \mlambda{}i,a. \mforall{}j:\{j:World| i \mleq{} j\} . \mforall{}v:Dom(j). (K-forces(K;body) j a[z := v])
else \mlambda{}i,a. \mexists{}v:Dom(i). (K-forces(K;body) i a[z := v])
fi )
Date html generated:
2019_10_16-AM-11_45_12
Last ObjectModification:
2018_10_15-PM-06_44_38
Theory : minimal-first-order-logic
Home
Index