Correcció a l'article "analisi formalment recursiva"

Publicacions Matemátiques, Vol 32 (1988), 289-291 . CORRECCIO A L'ARTICLE"ANALISI FORMALMENT RECURSIVA" En 1'article citat en el títol, publicat en aquesta mateixa revista [1], es dexnostren, basats en el formalisme AFR (aritmética formalment recursiva),els teoremes de Bolzano-Weierstrass [4 .8, pp . 63-68] i els teoremes del máxim i del mínim i de Bolzano per a funcions contínues [5 .9 i 5 .10, pp . 71-74] . Paró en les demostracions d'aquests teoremes s'utilitza sistemáticament, ja sigui de manera explícita o implícita, una forma del metateorema de minimització (p . 40) que no está justificada . Aquest metateorema afirma : per numerals bi, si aleshores també tenim F . TOMAS Ü ~- Eh(b 1 , . . . , b J= S(0), Mh(h 1 ,  E NC j i U ~- h(bi, Mh(b i )) = 0 En aquelles demostracions, peró, es suposa que 1'afirmació és carta per Unombres b i que no són numerals, i aquesta és la forma no justificada del teorema a la que ens referim . Tant a [1] con en 1'article precursor [2, p .48] s'omet senyalar que els b i han de ser numerals ; peró en la demostració del metateorema a [2] i en la correcció b) de la p .42 de [1] es suposa que ho són . L'ús incorrecta del metateorema es fa, per exemple, en el pas de (11) a (12) o de (19) a (20) en la p . 65 de [1] . El fet és que no podem demostrar 1'afirmació del metateorema si els b i són, en general, U-nombres . Per tant, les demostracions que dels teoremes esmentats es fan a [1] són incorrectas . Ara bé, els teoremes són essencialment veritables (amb enunciats un xic diferents), i sabem coin demostrar-los, si únicament modifiquen la definició del formalismeAFR de la manera que explicaren desseguida . La modificació consisteix en substituir PR .3 per el següent : PRZ . Si : 1) U és un segment de AFR i f(j i , y) E Nú(xi, y) ; 2)hi, ki, g .i E NC j (z l , . . . , z 9 ) per i  -  1, . . . , p i j  -  1, . . .,n ;  3) podem demostrar, per a qualssevol numerals d i , . . ., d q , c, que il ~- (vi!-, -h i = k i V -f(9 i ,j2) = 0 ) 1 (zi,di) ; 290  F . TOMAS 4) sabem finitáriament que U és consistent amb 1'esquema (ViP 1-hi = ki V -Ef(g,) = S(0) 1 (zi,di), per qualsevol numerals di ; alesbgres també és un seglrient de AFR el que s'obté en afegir a U 1'esquema de postulats (*) . En aquesta versió, més liberal que PR .3, cal, per¿>, en cada aplicació, demostrar finitáriament la consisténcia'del nou segment que s'obté en afegir a U 1'esquema de postulats (*) Si llegim els postulats en la forma (Ef(g_,) = S(0) =~> Vf 1 _h i = k i ) I (zi,di) veiem que PR .3' té 1'aspecte de regla d'eliminació de 3 (o "rule C" ), . ja que Ef(g,) = S(0) té el significat aproximat de "existeix e tal que f(g i . e) = 0 . Aixó és important perqué el metateorema de minimització no és cert en aquesta versió correcta de AFR (ni tan sols per numerals) . En lloc d'aquest metateorema tenim PR .3' i el següent Lema . Pera ¡ E NO : 1) Si e és numeral, U ~- f (g i , c) = 0 =~> M f (ái) = 0 V . . . V M f (ái) = e 2) Si c E Nr j , U  f (á i , c) = 0 =~> j (j i , M f (ái)) = 0 ,4) Si U ~- f (jai)) = 0, Mf(ái) E Nv . Per a poder desenvolupar 1'análisi es fa indispensable la introducció d'un llenguatge auxiliar, el °-llenguatge, o °-lógica, que ara descriurem . Partim del segment básic B . Introdi im uns quantificadors ídeals V° i 3° . Definim les ° -fórmules com les expressions produides a partir de les fórmules atómiques de AFR com si 3° i V° fossin els quantificadors del cálcul predicats . Definirem per cada A el significat de "m és una traducció de A", que escriurem m E T(A) . Escriurem les definicions només per als símbols lógics -, A i 3° . mETv(a=b)=(Vx i )[ V[-m=b(1 á-bj)] m E Tv(-A) _ (3m')[m' E Tv(A) & (Vx i )[V Im = b(m')] m E Tv(A A B) - (3m', m")[m' E Tv(A) & m" E TV(B) & (Vxi)[[- m - m' . m"]] m E Tv« 3> y)A)  (3m')(3f(xi,y))[m' E Tv(A) . & (Vxi,Y)[V F f(iii,y) = b(m') &m= Ef(x%)] En la primera de les definicions anteriors, x i són totes les variables que apareixen a á o b, en la segona totes les que apareixen a m', etc . 0 Definim ara la nació  de '-teorema com ANALISI FORMALMENT RECURSIVA  291 0 V fA- (3rn)[m E T ú (A) & (Vx ;)[V ~- m = S(0)]] No s'ha de pensar que la '-lógica auxiliar així descrita té les propietats del cálcul de predicats . No hi és válid ni tan sols el modus ponens, en general . De fet, no está demostrada la impossibilitat de tenir V ~- A i V ~- -A per alguns 0 V i A, mentre que és segur que no tenim mai V ~- -0 = 0 . Es a dir, que no está demostrat que no hi puguin haver "°-inconsisténcies locals ,' . Aquesta o-lógica és útil, per exemple, en el tractament de la tricotomia . Els detalls de tot aix6 apareixeran en un altre lloc . Referéncies 1 .  F . TOMAS, Análisi formalment recursiva, Pub . Mat . UAB 30 n . 2-3 (1986), 35-75 . 2 .  F . TOMAS, Aritmética i análisi formalment recursives, Pub . Mat . UAB 28 n . 1 (1984), 19-78 . Instituto de Matemáticas UNAM Circuito Exterior, C .U . 04510 México, D .F . MEXICO . Rebut el 20 de juny de 1988