% % mar99a.dn % % (find-fline "feb98.tex") % (find-fline "mar99b.dn") % (find-fline "tese2.sty") % (find-fline "Makefile") % Esse bloquinho ‚ pra parametricidade: % \Ta2\T_{a^2} \Tb2\T_{b^2} \6-a=>\ldots \6a=>\5 \5-b=>\ldots \5b=>(\4) \4(a->b)->(\2) \2a^{[]}->b^{[]} ->^{\ton{ ->\to  \/\lor  /\\land  \n\nn  pi1{\pi_1} pi2{\pi_2} RF\ruleF a{\alpha} b{\beta} c{\gamma} yP->yy|_{Pxy}->y yP->õy|_{Pxy}->õ_{Pxy} yP1[y|_{Pxy}]1 yP[y|_{Pxy}]1 []:[]  [][\;] ]1]^1 ]2]^2 \A\cpoV  \B\cpoDois  ÐÐ\Lambda  ==>\funto  &&\LAND  =>\TO  \TN\mathrm{TN} \*s\nss \*\ns %%% % % 5: O teorema da dedu‡Æo % %%% x/\y ---- x/\y x x->(y->z) ---- ------------ y y->z ------------- z ^td-treeA V W V W ==== ========= ==== ========= x/\y x->(y->z) x/\y x->(y->z) =============== ---------------\ruleT\DN\treeA z z ^td-dbar ^td-TA [x/\y]^{1A} ----------- [x/\y]^{1A} x [x->(y->z)]^{1B} ----------- ----------------------- V W y y->z ==== ========= ------------------------- x/\y x->(y->z) z ------------------------------1:\ruleTe\DN z ^td-TeA V ==== V x/\y W ==== ---- ========= x/\y x x->(y->z) ---- ------------- y y->z ------------- z ^td-Adireto [a]2 [b]1 ------------ a/\b [a/\b->c]^{3A} ------------------------- c ------1 b->c ------------2 a/\b->c a/\b->c a->(b->c) ------------\cur ----------------------------3:\ruleTe\DN a->(b->c) a->(b->c) ^td-CCCcur ^td-DNcur a/\b a/\b õ->a/\b õ->a/\b ---- ---- -------\ruleTCCC -------\ruleTCCC b a õ->b õ->a ------- ------------------------\ruleTCCC b/\a õ->b/\a ^DN->CCC.1 ^DN->CCC.2 ---------- [abc]^2 abc_2=>abc ------- ------ ---------- ---------- [a]^1 ab [abc]^2 a_1=>a abc_2=>ab abc_2=>abc ---------- ------- ----------------- ---------- b bc a_1&&abc_2=>b abc_2=>bc -------------- ---------------------------- c a_1&&abc_2=>c --1 -------------1 ac abc_2=>ac -------2 ----------2 abc->ac õ=>abc->ac ^tdex1 ^tdex2 a_1&&a_2=>b a_2&&a_3=>b->c ---------------------------- a_1&&a_2&&a_3=>c ^tdnum-1 a_1&&a_2&&a_3=>b a_1&&a_2&&a_3=>b->c -------------------------------------- a_1&&a_2&&a_3=>c ^tdnum-2 õ->b õ->(b->c) --------------- ------------------ õ->(b/\(b->c)) b/\(b->c)->^{\ev}c ----------------------------------- õ->b ^tdnum-3 -------------- a1/\abc2->abc2 abc2->bc ------------------------ a1/\abc2->b a1/\abc2->bc ------------------------- -------- a1/\abc2->b/\bc b/\bc->c --------------------------------- a1/\abc2->c ^tdex-step %%% % % 6: A  lgebra dos valores de verdade % %%% [a]1 a->b ------------- b b->c --------------- [a]1 c ------1 ------1 a->a a->c ^a->a ^a->c - - õ a õ õ->a -----1 -----1 -------- a->õ õ->a a ^a->T ^T->a ^T->a=>a [a_1]1 a_1->a_2 [b_1]1 b_1->b_2 ------------------- ------------------- a_2 b_2 ---------- ---------- [a_1\/b_1]2 a_2\/b_2 a_2\/b_2 -----------------------------------------------1 a_2\/b_2 ----------------------2 a_1\/b_1->a_2\/b_2 ^a1vb1->a2vb2 [©]1 - ---- õ a -----1 -----1 a->õ ©->a ^a<=T ^0<=a [a]1 a->b/\c [a]1 a->b [a]1 a->c --------------- ------------- ------------- b/\c b c ---- ---------------- b/c b/\c -------1 ----------1 a->b/c a->b/\c ^hey-andE ^hey-andI [b]1 [b]1 b->d [c]1 c->d ---- ----------- ----------- b\/c b\/c->d [b\/c]2 d d -------------- ----------------------------1 d d -----1 --------2 b->d b\/c->d ^hey-orE ^hey-orI [a/\b]1 [a]2 [b]1 -------- ----------- [a/\b]1 a a->(b->c) a/\b a/\b->c -------- ----------------- ------------------- b b->c c ------------------- ----1 c b->c --------1 ----------2 a/\b->c a->(b->c) ^hey-uncur ^hey-cur [a/\b]1 [a/\b]1 ------- ------- ------- ------- b a a/\b->b a/\b->a ---------- ---------------- b/\a a/\b->b->a ^Heyting1 ^Heyting2 0 1 0 A --- \A100 -- 0 0 ----- A ªA 1 0 0 1 \A100 \A001 ----- --------- ------------- A\/ªA 0 \A101 1 1 ^AvnA ^AvnA.w3 0 1 B --- \B01 -- 0 ---- ªB 0 \B00 --- --- ---- B ªªB 0 1 \B01 \B11 ------ 1 1 ---------- B->ªªB ----- \B01 0 ^B->nnB 1 ^B->nnB.w2 0 0 0 0 1 0 0 1 1 0 0 1 C D C D --------- --- --- \A100 \A001 \A100 \A001 ---- -- -- 0 0 0 ------------ ----- ----- C/\D ªC ªD 0 0 0 1 1 0 \A000 \A001 \A100 ------ ------ --- --------- ----- ------------ ª(C/\D) ªC\/ªD 1 0 \A111 \A101 ----------------- 1 1 1 1 ------------------- ª(C/\D)->(ªC\/ªD) --------------- \A101 0 ^demorgan 1 1 ^demorgan.w3 % (find-fline "~/LATEX/99feb11.dnt" "demorgan") %%% % % 7: An lise nÆo-standard % %%% a b \ii->a \ii->b ----\ruleF{(+)} --------------\ruleF{\ii->(+)} c \ii->c ^transf-1 ^transf-2 \*{a} \*{b} ------------\ruleF{\*s{(+)}} \*{c} ^transf-3 [\ii]1 \ii->a [\ii]1 \ii->b -------------- -------------- a b -----------------\ruleF{(+)} c ------1 \ii->c ^transf-4 a_1 \ldots a_n f -------------------\ruleF{\app} f(a_1,\ldots,a_n) ^transfapp-1 \ii->a_1 \ldots \ii->a_n \ii->f ----------------------------------\ruleF{\ii->\app} \ii->f(a_1,\ldots,a_n) ^transfapp-2 \*{a_1} \ldots \*{a_n} \*{f} -------------------------------\ruleF{\*s{\app}} \*{f}(\*{a_1},\ldots,\*{a_n}) ^transfapp-3 y f ---- x f(y) Q ---------- x P Q(x,f(y)) \t->^{ª}\t ---- --------------------- P(x) ªQ(x,f(y)) \t,\t->^{/\}\t ------------------------------------------- P(x)/\ªQ(x,f(y)) ^transfex-1 y f ---- [x]1 f(y) Q ------------- [x]1 P Q(x,f(y)) \t->^{ª}\t ------- ---------------------- P(x) ªQ(x,f(y)) \t,\t->^{/\}\t ----------------------------------------------- P(x)/\ªQ(x,f(y)) ---------------------1 Ðx.(P(x)/\ªQ(x,f(y))) ^transfex-2 %%% % % ?: Onde gostar¡amos de chegar % %%% %%% % % ?.?: O teorema da fun‡Æo inversa e seus amigos % %%% x x->y \ldots ---------------\TFI y->x ^tfi1 t->x/\y ======= t t->x --------\TFI x->t t->x/\y =================== x->y ^tfi-tflsub x/\y->f ========== x/\y x/\y->x/\f ----------------\TFI x/\y x/\y->f x/\f->x/\y ------------- ========== f x/\f->y ===================== x->y ^tfi-tfimp %%% % % ?.?: Uma migalha de l¢gica linear % %%% [a]1 a->b [a]1 a->(b->c) [x]1 2 [x]1 3 ---------- --------------- ------- ------- b b->c 2x 3x ---------------- ----------- c 6x^2 ----1 -------------1 a->c x\mapsto6x^2? ^linear1 ^linear2 dx dx --- ---------------- !dx !dx÷dy (dx,dx^2,\ldots) (y_x,\frac{y_{xx}}{2},\ldots) ----------- ------------------------------------------------ dy dy=y_x{}dx+\frac{y_{xx}}{2}dx^2+\ldots ^lineardx1 ^lineardx2 a->b a->c a->(b->c) ---------- --------- a->b/\c a/\b->c ^lineare1 ^lineare2 a÷b a÷c a÷(b÷c) --------- ------- a÷(b¾c) (aÏb)÷c ^lineare3 ^lineare4 %%% % % ?.?: Parametricidade % %%% [(a/\b)^2]^1 [(a/\b)^2]^1 ------------ ------------ a^2 a^P b^2 b^P ------------ ------------ a^{P2} b^{P2} ----------------------- a^{P2}/\b^{P2} ------------------------1 (a/\b)^2->a^{P2}/\b^{P2} ------------------------\eta (a/\b)^P ^param-anddef [a^{[]:2}]^1 a^P ================= a^{[]P2} ------------------1 a^{[]:2}->a^{[]P2} -----------------\eta a^{[]P} ^param-listdef [a^2]^1 [(a->b)^2]^3 --------------------- [a^2]^1 a^P b^2 b^P ------------ ------------------- a^{P2} b^{P2} ---------------------------- a^{P2}->b^{P2} ---------------------1 ìa^2.(a^{P2}->b^{P2}) -------------------------------3 (a->b)^2->ìa^2.(a^{P2}->b^{P2}) -------------------------------\eta (a->b)^P ^param-todef [\T_{a^2}]^3 [(a=>a^F)^2]^4 [a^P]^1 ---------------------------- ======= a^{F2} a^{FP} ---------------------------- a^{FP2} ------------1 ìa^P.a^{FP2} ----------------------3 ì\T_{a^2}.ìa^P.a^{FP2} ----------------------------------4 (a=>a^F)^2->ì\T_{a^2}.ìa^P.a^{FP2} ----------------------------------\eta (a=>a^F)^P ^param-polidef [a^P]^1 [b^P]^2 ======= ======= [a^P]^1 [b^P]^2 a^{[]P} b^{[]P} ================ ================ (a->b)^P (\2)^P =================== [\Tb2]^3 [(\5-)^2]^3 (\4)^P ============================3 [\Ta2]^1 [(\6-)^2]^1 (\5)^P ===================================1 (\6)^P ^param-map1 %%% % % ?: Extra: abstract de Itatiaia % %%% x f x x->y ----- ------- x f(x) x y -------- ------- (x,f(x)) h x/\y x/\y->z ----------- --------------- h(x,f(x)) z ^tat1 ^tat1-t [x]1 f [x]1 x->y ------- --------- [x]1 f(x) [x]1 y ----------- ----------- (x,f(x)) h x/\y x/\y->z ----------- --------------- t w h(x,f(x)) t t->x z ---- ------------ ------- ----1 w(t) Ðx.h(x,f(x)) x x->z ------------------ ------------- h(w(t),f(w(t))) z ^tat2 ^tat2-t t w t t->x ---- ------- t w w(t) f t t->x x x->y ---- ------- ------- ---------- w(t) f(w(t)) x y -------------- -------------- (w(t),f(w(t))) h x/\y x/\y->z ----------------- ------------------ h(w(t),f(w(t))) z ^tat3 ^tat3-t x_0 \phi \ldots x x->y \ldots ------------------D ---------------D (\ddx\phi(x))(x_0) y_x ^tat-d1 ^tat-d1t [x]1 [y]2 ---------- x/\y x/\y->z --------------- z ----1 x x->z -------- x x->y z_x ------ ------2 y y->z_x ----------- z_{xy} ^tat-dtot1t