Nuprl Definition : ex-do-Elim
In the case for impE (implies elimination)
we update the function F to
λM.F M?exname:e.if e is a pair then let a,b = e
in if (a =z m) then b else exception(exname; e) fi otherwise exception(exname; e)
That is bad because it introduces a catch of the exception.
Why can't we simply use λM.(snd(m')) ?
It doesn't work for the example ⌜<¬(¬(P ∨ ¬(P))), λh.(h (inr (λx.(h (inl x))) ))>⌝
Why that is can be seen by comparing
proof-generation-for-example-5 and alt-proof-generation-for-example-5
I think we need to use
λM.F M?nnn:e.e
where nnn is a fresh name, and the model has been updated so that
ModelEval(M,m) = ⌜λx.(exception(nnn; x))⌝⋅
ex-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ if deq-mFO() G P(vars) then <hyp, []> else <falseE on hnum, []> fi ;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵ note-is-function(B;numhyps;M[m:= λx.numhyps])
in <impE on hnum
, [<λM.F M?exname:e.if e is a pair
then let a,b = e
in if (a =z m)
then b
else exception(exname; e)
fi otherwise exception(exname; e)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ⟵ note-is-function(A;numhyps + 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ⟵ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ⟵ note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ⟵ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' ⟵ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
ex-do-Elim(exname;H;G;numhyps;m';fullevd) ==
fix((λex-do-Elim,m'.
let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL_ind(hyp;
mFOatomic(P,vars)⇒ if deq-mFO() G P(vars)
then <hyp, []>
else <falseE on hnum, []>
fi ;
mFOconnect(knd,A,B)⇒ _,__.if knd =a "imp"
then let M' ⟵
note-is-function(B;numhyps;M[m:= λx.numhyps])
in <impE on hnum
, [<λM.F
M?exname:e.if e is a pair
then let a,b = e
in if (a =z m)
then b
else ...
fi
otherwise exception(...; e)
, M
>;
<F, M'>]
>
if knd =a "and"
then let M' ⟵ note-is-function(A;numhyps
+ 1;note-is-function(B;numhyps;M[m:= <numhyps + 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 ⟵ note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 ⟵ note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1>; <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body)⇒ _.if isall
then eval a = snd(m') in
let M' ⟵ note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim m'
else eval j = new-mFO-var([G / H]) in
let M' ⟵ note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi ) ))
m'
Definitions occuring in Statement :
note-is-function: note-is-function(A;hnum;M),
modelUpdate: M[fnum(x) :=n],
modelAdd: M[n:= lbl,i,j],
new-mFO-var: new-mFO-var(H),
fRulefalseE: falseE on hypnum,
fRuleexistsE: existsE on hypnum with var,
fRuleallE: allE on hypnum with var,
fRuleimpE: impE on hypnum,
fRuleorE: orE on hypnum,
fRuleandE: andE on hypnum,
fRulehyp: hyp,
deq-mFO: deq-mFO(),
mFOL_ind: mFOL_ind,
mFOatomic: name(vars),
select: L[n],
cons: [a / b],
nil: [],
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t),
ispair: if z is a pair then a otherwise b,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
subtract: n - m,
add: n + m,
natural_number: $n,
token: "$token"
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
cons: [a / b],
new-mFO-var: new-mFO-var(H),
callbyvalue: callbyvalue,
apply: f a,
nil: [],
pair: <a, b>,
fRuleallE: allE on hypnum with var,
modelUpdate: M[fnum(x) :=n],
note-is-function: note-is-function(A;hnum;M),
pi2: snd(t),
ifthenelse: if b then t else f fi ,
token: "$token",
fRuleorE: orE on hypnum,
natural_number: $n,
modelAdd: M[n:= lbl,i,j],
eq_atom: x =a y,
fRuleandE: andE on hypnum,
add: n + m,
eq_int: (i =z j),
spread: spread def,
ispair: if z is a pair then a otherwise b,
lambda: λx.A[x],
fRuleimpE: impE on hypnum,
fRulefalseE: falseE on hypnum,
fRulehyp: hyp,
mFOatomic: name(vars),
deq-mFO: deq-mFO(),
mFOL_ind: mFOL_ind,
select: L[n],
subtract: n - m,
pi1: fst(t),
fix: fix(F),
fRuleexistsE: existsE on hypnum with var
FDL editor aliases :
ex-do-Elim
Latex:
ex-do-Elim(exname;H;G;numhyps;m';fullevd)
==r let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL\_ind(hyp;
mFOatomic(P,vars){}\mRightarrow{} if deq-mFO() G P(vars)
then <hyp, []>
else <falseE on hnum, []>
fi ;
mFOconnect(knd,A,B){}\mRightarrow{} $_{}$,\_$_{}$.if knd \000C=a "imp"
then let M' \mleftarrow{}{}
note-is-function(B;numhyps;M[m:= \mlambda{}x.numhyps])
in <impE on hnum
, [<\mlambda{}M.F
M?exname:e.if e is a pair
then let a,b = e
in if (a =\msubz{} m)
then b
else ...
fi
otherwise exception(...; e)
, M
>
<F, M'>]
>
if knd =a "and"
then let M' \mleftarrow{}{} note-is-function(A;numhyps
+ 1;note-is-function(B;numhyps;M[m:= <numhyps + 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 \mleftarrow{}{} note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 \mleftarrow{}{} note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1> <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body){}\mRightarrow{} $_{}$.if isall
then eval a = snd(m') in
let M' \mleftarrow{}{} note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a
, [<F, M'>]
>?exname:m'.ex-do-Elim(exname;H;G;numhyps;m';fullevd)
else eval j = new-mFO-var([G / H]) in
let M' \mleftarrow{}{} note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi )
Latex:
ex-do-Elim(exname;H;G;numhyps;m';fullevd) ==
fix((\mlambda{}ex-do-Elim,m'.
let F,M = fullevd
in eval m = if m' is a pair then fst(m') otherwise m' in
eval hnum = numhyps - m + 1 in
eval hyp = H[hnum] in
mFOL\_ind(hyp;
mFOatomic(P,vars){}\mRightarrow{} if deq-mFO() G P(vars)
then <hyp, []>
else <falseE on hnum, []>
fi ;
mFOconnect(knd,A,B){}\mRightarrow{} $_{}$,\_$_{\000C}$.if knd =a "imp"
then let M' \mleftarrow{}{}
note-is-function(B;numhyps;...)
in <impE on hnum
, [<\mlambda{}M.F M?exname:e....
, M
>
<F, M'>]
>
if knd =a "and"
then let M' \mleftarrow{}{} note-is-function(A;numhyps
+ 1;note-is-function(B;numhyps;M[m:= <numhyps
+ 1,numhyps>]))
in <andE on hnum, [<F, M'>]>
if knd =a "or"
then let M1 \mleftarrow{}{} note-is-function(A;numhyps;M[m:= inl(numhyps)])
in let M2 \mleftarrow{}{}
note-is-function(B;numhyps;M[m:= inr(numhyps)])
in <orE on hnum, [<F, M1> <F, M2>]>
else "funny connective??"
fi ;
mFOquant(isall,v,body){}\mRightarrow{} $_{}$.if isall
then eval a = snd(m') in
let M' \mleftarrow{}{} note-is-function(body;numhyps;M[m(a) :=numhyps])
in <allE on hnum with a, [<F, M'>]>?exname:m'.ex-do-Elim m'
else eval j = new-mFO-var([G / H]) in
let M' \mleftarrow{}{}
note-is-function(body;numhyps;M[m:= <dj,numhyps>])
in <existsE on hnum with j, [<F, M'>]>
fi ) ))
m'
Date html generated:
2016_07_08-PM-05_26_48
Last ObjectModification:
2015_11_24-PM-04_38_24
Theory : minimal-first-order-logic
Home
Index