variabili libere

weblog italiano di filosofia analitica

Le metavariabili colpiscono ancora!

Posted by Elia Zardini su febbraio 12, 2007

Non posso resistere questo. In uno dei più importanti libri “scolastici” di teoria della dimostrazione (“Basic Proof Theory”, CUP), gli emeriti autori A. Troelstra e H. Schwichtenberg dicono all’inizio di usare ‘x’, ‘y’ etc come metavariabili. Ma poi il libro è pieno di asserzioni del tipo che, data una dimostrazione di forma:

.
.
.
Ax Px
.
.
.
Ay Qy
.
.
.

ci sono almeno due variabili distinte in essa. Questo è come dire che se uno dice ‘x è bello e y è forte’ uno si sta riferendo ad almeno due oggetti diversi! Se uno ha avuto la pazienza di leggersi il libro, è stupefacente che, con tutta la cura messa nelle varie sottili distinzioni sintattiche richieste dalla teoria della dimostrazione, gli autori si siano lasciati scappare una svista così clamorosa…

Annunci

26 Risposte to “Le metavariabili colpiscono ancora!”

  1. giuliano torrengo said

    Forse si può accettare come implicatura conversazionale cancellabile che

    (XX, YY … meta-meta variabili
    X,Y… meta-variabili)

    Per ogni XX e YY, se XX si riferisce a X e YY si riferisce a Y, e Non (XX = YY) allora Non (X = Y).

    Certo, dal punto di vista sociologico, questo la dice lunga sul tipo di conversazione che si può avere con un autore di un manuale di teoria della dimostrazione.

  2. Sono sconvolto da una simile notizia! 🙂

    Ma sei sicuro che non vi siano convenzoni tipografiche per cui due segni diversi si riferiscono a variabili diverse?

  3. Fabrizio Cariani said

    A pagina 4 (almeno nella mia edizione, la seconda) Troelstra e Switchenberg scrivono: “Also it is never a real restriction to assume that distinct quantifier occurrences are followed by distinct variables, and that the sets of bound and free variables of a formula are disjoint”.

    Credo questo sia sufficiente a prendersi cura del problema (correggimi se sbaglio).

    Tuttavia, va anche detto che, se non ricordo male, nella prefazione T&S scrivono che le prime sezioni del libro non vanno lette “di fila” ma usate come “reference” (controllate qualora ve ne sia la necessita’). Il che rende abbastanza buffo che il commento in questione avvenga due pagine dopo la caratterizzazione dei vari tipi di metavariabile .

  4. A Giuliano. Di solito non c’è tale implicatura per metavariabili. Considera: da A & B si può dedurre B — uno ovviamente vuole includere il caso in cui A=B. Nel caso di T&S, io piuttosto la chiamerei erronea associazione psicologica 😉

    A Fabrizio. Ciao, non penso ci conoscessimo prima! Non mi sembra che il passo tu adduci giustifichi la seguente prassi che adottano, dato che in esso stanno parlando solo del linguaggio-oggetto (così come le osservazione precedenti al passo riguardano solo alpha-conversion di formule del linguaggio-oggetto). Non chiedermi quale sia il linguaggio oggetto in specifico: un altro degli aspetti strabilianti del libro è che esso non viene mai specificato!!!

  5. Elia e a me non dici niente? 🙂 Senti, ma che cavolo di immagine hai, sei tu che stai a magna’?

  6. Ah, ah geloso 🙂 Lontani solo 2 mesi e già mi desideri nostalgicamente (I mean, “long” (ing), o “sehnen” (ted), come si dice in italiano?).

    No, comunque seriamente loro non esplicitano mai quello che avrebbero dovuto rendere esplicito — rendono tutto esplicito ciò che riguarda le convenzioni per le variabili del linguaggio-oggetto (che, per il resto, come ho detto non è mai specificato, per cui uno non sa neanche di che simboli stanno parlando), come devono dato i problemi di book-keeping che costituiscono la croce e delizia della teoria della dimostrazione, ma l’uso del metalinguaggio è lasciato completamente vago e impreciso, abbandonato alla carità del lettore. Ma dato che i teoremi vengono poi dimostrati nel metalinguaggio, questa imprecisione inevitabilmente si trasmette un po’ sulle loro dimostrazioni (nonostante of course è probabile aspettarsi che, una volta che siano completate con le distinzioni necessarie, le dimostrazioni dei teoremi rimangano corrette).

    Elia

    PS Non posso credere non ti riconosci la foto — le lasagne ti dicono niente?! Ho scelto questa per questo blog perché il soggiacente spirito italiota mi sembrava adatto… molto meglio di metterne una con una lavagna (ehm…) 😉

  7. Eh si, mi manchi molto, Silvia è quasi gelosa (btw: questo scambio, credo sia una delle perle dei posts di questo blog).

    Per la foto ho capito: era quella della cena italiaota del mio farewell party a St. Andrews!

    Effettivamente dovrei forse cambiare la mia foto della lavagna…

  8. fcariani said

    Elia, no non ci conosciamo, penso di averti visto una volta al workshop sulla vaghezza a Bologna che credo fosse a fine 2003 o a inizio 2004, ma ero un “turista” di passaggio in quel workshop! Comunque Ciao!

    Giusto per capire meglio il tuo punto: quandi dici che “stanno parlando del linguaggio oggetto” intendi che la convenzione che distinte occorrenze dei quantificatori sono seguite da variabili distinte vale soltanto in relazione a formule singole…

    e.g. la formula ‘Ax Ey (R(x,y))’ contiene, secondo la convenzione, due variabili.
    Ma la convenzione non determina che la dimostrazione:

    Ay Py
    _____
    Ex Px

    contiene due variabili?

  9. eliazardini said

    Ciao Fabrizio, scusa per il ritardo della risposta, ma sono stato in viaggio nelle ultime due settimane.

    Mi sembrerebbe che sia meglio per loro che la convenzione che tu citi sia ristretta a formule singole, altrimenti: AxP, AxP -> Q |- Q non è un’esempio di modus ponens! Uno potrebbe pensare che il problema non si darebbe qui per loro, dato che almeno ufficialmente “identificano” formule modulo renaming of bound variables (ma come si dice in italiano?!). Ma in realtà leggendo il libro sembra che quella identificazione sia solo assunta nella prova di cut-elimination, e anche lì cum grano salis e non letteralmente (non possono intendere che p. es. ‘A’ – che usano come metavariabile per formule qualsiasi – abbia come valori classi di equivalenza under renaming of bound variables, perché altrimenti molte loro enunciazioni non sarebbero ben definite. Pensa p. es. a \forall-elim:

    \forall x A,

    Therefore

    A[x/t]

    A che variabile del linguaggio oggetto si riferirebbe ‘x’ nella conclusione? Loro non lo dicono, quando invece c’è bisogno di dirlo se ‘\forall x A’ si riferisce in realtà a una classe di equivalenza.) Mi sembra più caritatevole leggerli come limitantisi a formule singole (tale pare d’altronde il contesto del passo che citi, e tale è la prassi in generale in teoria della dimostrazione) – anche se così vanno incontro al mio lamento originario!

    Un problema ancora più “grosso” (si fa’ per dire!) emerge comunque piuttosto con le variabili libere (in questo senso il mio esempio originario per illustrare il mio generale lamento era un po’ fuorviante), dato che chiaramente assumono che differenti metavariabili libere si riferiscono a differenti variabili (altrimenti molte loro applicazioni p. es. di \forall-intro non sarebbero valide).

    Tanto per aggiungere un’osservazione alla convenzione che tu citi, anche se ristretta a formula singole è sistematicamente violata dagli autori stessi, dato che spesso usano la stessa metavariabile dopo due distinte occorrenze di un quantificatore in una stessa formula (si spera infatti che l’interpretazione di una metavariabile rimanga costante in una formula!). Se l’intepretazione è costante in tutta una dimostrazione (come di nuovo si spera che sia!) essi violano anche le loro convenzioni autoimposte (variable convention e pure variable). Insomma – un disastro di imprecisioni!

  10. Fabrizio Cariani said

    ehehe che casino! comunque un libro interessante!

  11. eliazardini said

    Sì. Però quando uno vede tutto il casino di book-keeping matematicamente superficiale che l’uso di variabili introduce, uno prova qualche forte simpatia per Schönfinkel e la logica combinatorica — abbasso le variabili!!!

    E

    PS Tra l’altro, a proposito di delusioni, io pensavo che Anne Troelstra fosse un’avvenente proof-theorist dai capelli biondi e gl’occhi azzurri — ti lascio immaginare la delusione quando ho googolato il nome…

  12. A Elia:

    >gli emeriti autori A. Troelstra e H. Schwichtenberg dicono all’inizio di usare ‘x’, ‘y’ etc >come metavariabili. Ma poi il libro è pieno di asserzioni del tipo che, data una dimostrazione >di forma: Ax Px … Ay Qy ci sono almeno due variabili distinte in essa. Questo è come dire >che se uno dice ‘x è bello e y è forte’ uno si sta riferendo ad almeno due oggetti diversi!

    Questo non è corretto in quanto due variabili distinte possono riferirsi allo stesso oggetto. L’unica restrizione è che una variabile deve mantenere lo stesso significato nel medesimo contesto (vedi su questo punto la ‘bibbia, ossia lo Shoenfield, che anche se ormai datato …).

    Per esempio, l’espressione x=x si riferisce a espressioni come 2=2 ma anche genericamente n=n (se il dominio dell’interpretazione è l’insieme dei naturali, ad esempio), mentre l’espressione x=y ha tra le sue interpretazioni sia 2=2 e i vari n=n che 2=5.

    Quello che non capisco molto è la questione delle metavariabili (penso intendano variabili sintattiche) che variano su espressioni, non su variabili.

    In generale il linguaggio oggetto è semplicemente un linguaggio formale L specificato inizialmente nel modo solito. Come metalinguaggio si usa il linguaggio naturale, dunque per metavariabili penso intendano davvero variabili sintattiche, ossia lettere che variano su espressioni del linguaggio oggetto. Forse questo ha generato confusione.

    PS Anne Sjerp Troelstra poteva forse anche essere bionda con occhi azzurri, ma certamente un po’ avanti con gli anni visto che ha fatto il dottorato (1966) con Heyting….

  13. eliazardini said

    Ciao Giuseppina,

    assumo che il tuo primo commento esprime accordo con me.

    Riguardo al secondo, loro hanno anche metavariabili che variano su espressioni appartenenti ad altre categorie sintattiche. Per quanto mi ricordo, il linguaggio-oggetto, sfortunatamente, non è mai specificato, nemmeno per dire che è il solito (di contro a ciò che avviene in quasi ogni pubblicazione in logica!). In ogni caso, dicono chiaramente che le lettere che usano (‘x’, ‘y’… ‘P’… ‘R’… ‘A’, ‘B’…) sono metavariabili (e quindi *non* espressioni del linguaggio-oggetto). Ed è proprio per questa strana decisione che incorrono nei problemi che ho che ho evidenziato.

    E

    PS Sapevo che Troelstra non era più nel fior della gioventù, ma dato il mio amore per le donne mature ciò non mi ha impedito di fantasticare su di lui (de re!) fra un sequente e l’altro, fino alla ferale scoperta 😉

  14. Ciao Elia,

    in realtà non ero d’accordo con te, ossia la tua conclusione è sbagliata (se ho capito bene il tuo problema). Non ho il testo e non posso verificare ma dire che

    “data una dimostrazione di forma:

    Ax Px
    .
    .
    .
    Ay Qy

    ci sono almeno due variabili distinte in essa”

    non è come dire (come dici tu) che se ‘x è bello e y è forte’ uno si sta riferendo ad almeno due oggetti diversi (come dici tu) perché la x e la y della sequenza possono riferirsi allo stesso oggetto anche se sono variabili distinte.

    Per quanto riguarda l’uso delle metavariabili, da quello che tu dici mi sembra di capire che quello che loro intendono e ciò che si chiama (anche) ‘variabili sintattiche’, che spesso vengono scritte in neretto. Spesso si usano lettere minuscole per (meta)variabili che variano su tutte le espressioni del linguaggio oggetto (= sequenze finite di simboli del linguaggio oggetto), oppure lettere maiuscole che variano sulle formule del linguaggio oggetto. La x e la y nell’esempio che riporti sono evidentemente variabili del linguaggio oggetto, e, ripeto, dire che una dimostrazione come quella dell’esempio contiene almeno due variabili distinte non significa dire che si riferiscono necessariamente a due oggetti distinti. Quindi non vedo il problema ma, ripeto, non ho il libro (o forse non ho capito bene il tuo problema).

    Per quanto riguarda il fatto che non sia descritto il linguaggio formale, mi sembra un po’ strano, forse c’è almeno scritto che per quanto concerne il linguaggio si adottano le usuali convenzioni (un insieme contabile di variabili, simboli per funzioni / predicati + costanti logiche) ?

    PS forse ti interesserà sapere che AT, in pensione, ora si dedica alla botanica e non più alla logica.

  15. eliazardini said

    Ciao Giuseppina,

    probabilmente il mio post originale non era molto chiaro, per cui provo a chiarificare qual’era il mio punto. T&S sono univoci che stanno usando ‘x’, ‘y’ etc come variabili metalinguistiche che variano sull’insieme delle variabili (individuali) del linguaggio-oggetto (che ahimè non viene mai specificato), così come d’altronde sono univoci che stanno usando tutte le espressioni che usano come variabili metalinguistiche che assumono come valori entità di un appropriato tipo sintattico. Per cui, quando scrivono qualcosa come:

    .
    .
    .
    … Px…
    .
    .
    .
    …Qy…
    .
    .
    .

    (con ‘x’ e ‘y’ libere o vincolate, v. discussione con Fabrizio), quello che hanno scritto *non è* una dimostrazione (che è definita solo per alberi adornati con formule del linguaggio-oggetto), ma una (complicata) espressione del metalinguaggio che può assumere come valori specifiche dimostrazioni (che usano formule del linguaggio-oggetto). In particolare, ‘x’ e ‘y’ si riferiscono a variabili del linguaggio-oggetto (ovviamente, “si riferiscono” a esse nel senso che “variano su” il loro insieme).

    Ora è un fatto che da molto di ciò che T&S scrivono si può inferire che essi assumono che se le variabili metalinguistiche ‘x’ e ‘y’ sono sintatticamente distinte, allora assumono come valori variabili differenti del linguaggio-oggetto. Il mio punto era che, come tu stessa noti, questa assunzione è completamente sbagliata — è come assumere che l’enunciato aperto ‘x è bello e y è forte’ si riferisca a due oggetti differenti (semplicemente perché ‘x’ e ‘y’ sono sinttaticamente distinti).

    E

    PS Ben prima di vedere che era incorso in questo veniale howler, AT aveva già perso ogni significato nella mia vita da quando avevo scoperto la sua vera identità!

  16. sascia said

    Ciao Elia.

    Non ho mai lavorato su quel libro, ma potrei provare a darci un’occhiata, ma potresti dare qualche riferimento, cioè indicare dove per esempio i due autori commettono la fallacia che tu imputi loro? Anche ammettendo che tu abbia ragione, dalla descrizione che ne dai, l’errore sembrerebbe veramente facile da correggere. Poniamo che io asserisca ‘Px’ e ‘Qy’. Questo non mi consente di dedurre ‘x≠y’, ma, se ne ho bisogno, posso sempre aggiungerlo come assunzione supplementare. Questo però suggerisce la seguente lettura caritatevole dei passaggi incriminati. Quando tu dici che loro hanno illegittimamente dedotto ‘x≠y’ da ‘Px’ e ‘Qy’, in realtà l’hanno semplicemente assunto. C’è qualcosa che impedisce di integrare ogni loro argomento incriminato in questo modo?

  17. A Elia:

    dunque, mi sembra che ci siano dei fraintendimenti (forse comunque causati dal testo, non so).

    Non ho il testo, ma grazie a Google Print ho potuto leggerne alcune parti (by the way, con un po’ di pazienza e tempo, e un piccolo trucco, si riescono a leggere interi libri con google print).

    1. La questione del linguaggio oggetto: il linguaggio oggetto è descritto a pagina 2, ossia

    section 1.1.1. The Language of First-order logic

    Forse vengono introdotti anche altri linguaggi formali, non so, ho letto un po’ rapidamente.

    2. La questione delle metavariabili, sempre intodotte a p. 2. Dunque, come dici, ci sono metavariabili per tutte le CATEGORIE sintattiche (per variabili, costanti, formule, termini, funzioni, ecc).

    Ora, quando tu dici che:

    “Ora è un fatto che da molto di ciò che T&S scrivono si può inferire che essi assumono che se le variabili metalinguistiche ‘x’ e ‘y’ sono sintatticamente distinte, allora assumono come valori variabili differenti del linguaggio-oggetto.”

    mi viene il dubbio che interpreti male la distinzione a cui loro (forse) si riferiscono, che probabilmente è una distinzione di CATEGORIA sintattica.

    Mi spiego, loro introducono ad esempio:

    x e y come metavariabili per la CATEGORIA sintattica delle variabili (del linguaggio oggetto, ossia un linguaggio logico del primo ordine)

    t,s,… come metavariabili per la CATEGORIA sintattica dei termini (del linguaggio oggetto..)

    chiaramente: x e t sono variabili appartenenti a diverse categorie sintattiche, sono distinte in questo senso.

    invece: x e y NON sono metavariabili distinte sintatticamente, ossia non appartengono a diverse categorie sintattiche, bensì alla stessa (delle metavariabili per variabili)

    Non è che loro dicono qualcosa come

    metavariabili sintatticamente distinte (= appartententi a diverse categorie sintattiche) si riferiscono distinte categorie di segni del linguaggio-oggetto.”

    Magari sarebbe utile che indicassi in quali pagine si crea il fraintendimento.

    Ciao

  18. … dimenticavo, comunque (banalmente) anche se ci fosse la convenzione che a distinte metavariabili corrispondono distinte variabili del linguaggio oggetto nulla vieta che queste poi vengono interpretate sullo stesso oggetto. Ma ripeto occorrerebbe avere i riferimenti precisi che hanno causato questa confusione.

    A proposito: potresti indicare esattamente dove hai trovato questa situazione:

    “[…] spesso usano la stessa metavariabile dopo due distinte occorrenze di un quantificatore in una stessa formula […]”

    grazie

    PS scusa l’insistenza, non è che non ti creda o che non mi fidi, vorrei solo rendermi conto.

  19. eliazardini said

    A Sascia: certo, questo è il modo in cui uno deve leggere il libro in modo da renderlo sensato, e, per quel che posso vedere, tutte le prove funzionano comunque una volta che si sia fatta questa assunzione aggiuntiva. Come ho detto a Giuliano, data la (benvenuta!) cura che essi mostrano nello specificare altre sottigliezze, l’ipotesi psicologica (secondo me) più probabile riguardo a ciò che passava nella loro testa quando hanno scritto il libro è che non si siano accorti del problema piuttosto che che se ne siano accorti, abbiano formulato nella loro testa la (non-triviale) assunzione aggiuntiva e deciso di non dire niente al lettore. (Un esempio di dove fanno l’errore–o assumono l’assunzione aggiuntiva senza dirci niente–è p. 67, terza riga a sx della prova con Cut).

    A Giuseppina:

    – non mi sembra il linguaggio sia molto specificato: quel che dicono letteralmente è addirittura compatibile con il fatto che sia in realtà di ordine superiore (i “relation symbols” potrebbero essere “relation variables”), o qualche pazzo linguaggio infinitario del primo ordine. Non danno nemmeno le regole di costruzione! Data la cura negli altri dettagli, mi sembra una scelta un po’ sconcertante, anche perché si sarebbero potuti salvare dal loro howler se avessero detto che ‘x’ e ‘y’ sono anche variabili del linguaggio-oggetto (allora avremmo potuto disambiguarli caritatevolmente nei casi in questione).

    – Sono d’accordo con (e avevo già capito) quello che dici fino a “Non è che loro…”, ma non vedo come aiuti T&S. Purtroppo non capisco il punto che fai dopo. Quello che posso dire per quel che capisco è che:

    (*) metavariabili sintatticamente distinte (= appartententi a diverse categorie sintattiche) si riferiscono distinte categorie di segni del linguaggio-oggetto.”

    è vero, ma che non serve molto ad alleviare il problema. Se c’è qualcosa che mi sfugge in quello che hai scritto, ti sarei grato me lo potessi rispiegare (sono un po’ tonto). Capisco anche quello che dici nell’ultimo post, ma — di nuovo — non vedo come aiuti col problema in discussione.

    E

    PS Se mi credi e ti fidi cosa vuoi di più? 😉 Comunque un es. è a p. 53, prima wff a sx della penultima riga dell’ultima deduzione.

  20. Ciao Elia, molto velocemente alcune cose:

    sul linguaggio: quello che dicono non è compatibile con il fatto che sia un linguaggio del secondo oridine o superiore ecc. per il semplice fatto che il paragrafo si intitola “The language of first-order logic” e che, almeno mi sembra di ricordare, è anche specificato inizialmente che il libro contiene discussioni su vari tipi di formalizzazioni del *primo ordine*.
    Dunque is simboli per funzioni e relazioni sono da intendersi conseguentemente. Le regole di costruzione forse mancano (non ho il tempo per controllare ora con Google print) ma questo libro non è un libro di introduzione alla logica, è un libro di proof theory anzi di *structural proof theory*, che, in ogni caso, richiede che uno abbia già avuto un corso di logica matematica o studiato un testo appropriato (Enderton, Shoenfield, ecc. )

    Mi procuro il testo, per guardare l’esempio che citi di p. 53, ma mi ci vogliono un po’ di giorni (biblioteca fuori mano, non sono in una città in cui posso prendere libri in prestito e devo chiedere a qualcuno di prenderlo in prestito per me): quando ho il testo ti rispondo anche sull’altro punto.

    Ciao

  21. eliazardini said

    Ciao,

    – confesso che la discussione sulla questione se il linguaggio sia “specificato” o meno mi sembra stia diventando un po’ tediosa. FWIW, se per specificare un linguaggio X in una sezione basta mettere come titolo della sezione “Il linguaggio X”, no matter cosa poi una scrive nella sezione, mi sembra siamo arrivati alla frutta… È come se uno intitola una sezione “The axioms of predicative 2OL” e poi non mette nessuna restrizione su comprehension… Se non lo sai c’è comunque anche un capitolo su linguaggi del secondo ordine, e, ironicamente, il modo (molto sloppy) con cui “aumentano” il linguaggio all’inizio del capitolo è strettamente parlando corretto solo se si assume che i “relation symbols” di cui parlano quando “specificano” il linguaggio di 1OL includano anche “relation variables”, altrimenti hanno introdotto quantificatori di secondo ordine in un linguaggio dove non ci sono variabili di secondo ordine da vincolare.

    – L’es. a p. 53 è:

    \forall x(A -> B) -> (A -> \forall x B)

    Secondo la mia personale opinione è un caso dove “usano la stessa metavariabile dopo due distinte occorrenze di un quantificatore in una stessa formula”, ma forse mi sbaglio.

  22. ciao Elia,

    sicuramente la questione sul linguaggio è noiosa, ma il fatto è che tu hai puntualizzato molte volte (anche con una certa enfasi) che il *linguaggio oggetto* non viene mai specificato, cosa non vera.

    Ribadisco (e concludo sulla questione *linguaggio*) che il libro non è un libro di introduzione alla logica e dunque si presuppone che uno sappia cosa sia un linguaggio del primo ordine. Si mette lo stesso un paragrafo per stabilire la terminologia. Forse glia autori avrebbero potuto essere più espliciti, ma per quello che ho potuto vedere non mi sembra ci siano omissione tali a compromettere la leggibilità e comprensione .

    Per quanto riguarda l’esempio di p. 53 mi serve anche ovviamente conoscere il contesto, e verificare le convenzioni che come tu dici risultano ambigue. Ho chiesto già il libro e quando lo avrò se ti interessa ti dirò la mia opinione, se no me la tengo.

    Non sto *difendendo* T&S, capita a volte di notare sviste o errori in libri di logica, sebbene i logici sia meticolosi allo spasimo. Comunque prima di dire che qualcuno sbaglia occorre verificare. Se sei sicuro di quello che dici dovresti segnalarlo agli autori che sicuramente sarebbere molto grati per questo. Se è come dici tu, si tratta di una svista che sicuramente danneggia la qualità del testo.

    Peraltro nella home page di Troelstra ci sono gli errata alle pubblicazioni compreso un errata a Basic Proof Theory (La HP di AS è in olandese, se ti interessa sapere cosa c’è scritto posso tradurtela)

  23. … (poi per oggi chiudo),

    mi sembra che ci sia una gran confusione:

    *ironicamente, il modo (molto sloppy) con cui “aumentano” il linguaggio all’inizio del capitolo è strettamente parlando corretto solo se si assume che i “relation symbols” di cui parlano quando “specificano” il linguaggio di 1OL includano anche “relation variables”, altrimenti hanno introdotto quantificatori di secondo ordine in un linguaggio dove non ci sono variabili di secondo ordine da vincolare*

    dunque, non ho il libro e controllerò, quello che penso è che loro dicono che il linguaggio del primo ordine viene *esteso* con l’aggiunta … no ?

    “\forall x(A -> B) -> (A -> \forall x B)
    Secondo la mia personale opinione è un caso dove “usano la stessa metavariabile dopo due distinte occorrenze di un quantificatore in una stessa formula”, ma forse mi sbaglio.”

    le due occorenze del quantificatore sono indipendenti (il secondo quantificatore non è nello scopo del primo, da come scrivi tu). Non vedo alcun problema in questa formula, se vuoi puoi anche rinominare una delle due variabili, ma non c’è alcuna necessità. (l’unica condizione è che A non deve contenere x libera, in particolare sarebbe più conveniente scrivere “\forall x(A ->B(x)) -> A -\forall x (B)”; l’implicazione vale anche nell’altro senso.) Ciao (e scusa la pedanteria)

  24. eliazardini said

    Ciao Giuseppina,

    per carità ci tengo alla tua opinione, però cerca di esercitare un po’ di carità interpretativa anche nei miei cf (v. soprattutto due ultimi punti sotto).

    – Mi dispiace che dici che io ho detto una cosa non vera senza affrontare nessuna delle ragioni che ho dato per supportare la mia asserzione. L’unico argomento che tu hai dato mi sembra sia che “Il titolo della sezione è ‘Linguaggio del primo ordine’; perciò nella sezione viene specificato un linguaggio del primo ordine usuale’. Questo non mi sembra proprio un buon argomento, come ho cercato di spiegare nel post precedente. Il fatto rimane che quello che dicono effettivamente del linguaggio oggetto è compatibile con il fatto che esso sia infinitario del primo ordine, del secondo ordine o ordini superiori, o perfino l’insieme vuoto. Non dicono quali siano i simboli del linguaggio, né quali ne siano le regole di formazione. Tra l’altro, l’hanno specificato così bene che si sono dimenticati pure le parentesi (per aggiungere buffamente nella pagina seguente convenzioni per risparmiarle!).

    Per inciso, il mio punto non è mai stato che tale omissione costituisce un serio ostacolo all’intelligibilità del libro, solo che data la precisione che la materia richiede è un po’ sorprendente che gli autori siano così sloppy nel dire qual’è il linguaggio oggetto.

    – Loro dicono che aggiungono semplicemente al “linguaggio del primo ordine” i quantificatori \forall X, \exists X. Per ripetermi, dato che uno non sa esattamente cosa sia il “linguaggio del primo ordine”, non è nemmeno chiaro cosa sia il nuovo linguaggio, ma il mio punto era che se non ci sono variabili di secondo ordine nel linguaggio di partenza non precedute immediatamente da un quantificatore non ci saranno nemmeno una volta che ci aggiungi semplicemente \forall X, \exists X, e così non hai niente che \forall X, \exists X possano vincolare in modo non vacuo — cioè non hai un linguaggio del secondo ordine usuale.

    – Conosco anch’io le convenzioni usuali sulle variabili — ma il punto esemplificato dall’esempio non aveva niente a che fare con questo. Mi permetto di rimandarti al thread per vedere in che contesto l’esempio è rilevante.

    E

    PS Adoro la tua pedanteria, era per questo che AT mi aveva leggermente deluso ancora prima di scoprire la sua vera identità.

  25. eliazardini said

    Ciao Sascia,

    preparandomi per la prossima sessione sul libro (lo stiamo leggendo qui a St Andrews con Roy Dyckhoff) ho scoperto di aver detto una vaccata — scambiando un L\forall per un R\forall — quando ti ho indicato l’esempio che ho indicato (probabilmente stavo leggendo il libro upside down!). Un esempio giusto è a p. 370, 3.1.3D, prova in basso a sx, 4a linea, che non è un’applicazione valida di R\forall se z=x.

    Comunque se sei interessato alla teoria della dimostrazione consiglio caldamente il libro: ci sono un sacco di sistemi e varianti interessanti spiegati molto bene. Magari da accompagnare col libro (ancora da uscire da quel che so) di Restall per una discussione di alcuni aspetti filosofici della teoria della dimostrazione (il mio amico Anne dice adamantinamente nell’intro: “Another complaint was that our account was lacking in motivation and philosophical background. This has not been remedied in the present edition, although a few words of extra explanation have been added here and there” — fair enough! ;-)).

    Ciao,

    Elia

  26. sascia said

    Ciao Elia,

    scusa per il ritardo con cui rispondo, ma stavolta ero io in viaggio. Quanto alla dimostrazione di p. 370, sembra proprio che tu abbia ragione. Se x e y sono metavariabili che variano su variabili, manca l’assunzione che x≠y.

    Ti ringrazio per i suggerimenti bibliogrfici.

    Sascia

Rispondi

Inserisci i tuoi dati qui sotto o clicca su un'icona per effettuare l'accesso:

Logo WordPress.com

Stai commentando usando il tuo account WordPress.com. Chiudi sessione / Modifica )

Foto Twitter

Stai commentando usando il tuo account Twitter. Chiudi sessione / Modifica )

Foto di Facebook

Stai commentando usando il tuo account Facebook. Chiudi sessione / Modifica )

Google+ photo

Stai commentando usando il tuo account Google+. Chiudi sessione / Modifica )

Connessione a %s...

 
%d blogger hanno fatto clic su Mi Piace per questo: