Piano di studi di Logica Matematica I

Scopo

Tutti i corsi di matematica richiedono di dimostrare, e tutti quelli di filosofia richiedono di argomentare; eppure nessuno di essi fa del ragionamento stesso il proprio oggetto, e tutti danno per inteso che cosa significhi che una conclusione segua da certe premesse. Questo corso prende tale domanda come proprio argomento. Il suo scopo è costruire, per il linguaggio più semplice della logica, la prima teoria matematica completa il cui oggetto è il ragionamento, con i suoi quattro pezzi in vista: un linguaggio, le cui formule si riconoscono e si leggono senza ambiguità; un calcolo, che produce deduzioni senza badare al significato dei simboli; un significato, che assegna a ogni formula il suo valore di verità sotto ogni assegnazione delle sue variabili; e la dimostrazione che il calcolo e il significato coincidono.

Se così è, il corso non è una raccolta di regole per manipolare simboli, ma una teoria con un risultato centrale, il teorema di completezza, che tutto ciò che precede prepara. Per un insieme di formule $\Gamma$ e una formula $\varphi$, la deducibilità $\Gamma \vdash \varphi$ dice che esiste una successione finita di formule, costruita con assiomi e regole, che termina con $\varphi$; la conseguenza semantica $\Gamma \models \varphi$ dice che ogni assegnazione che rende vere le formule di $\Gamma$ rende vera $\varphi$. Le due relazioni nascono da idee opposte, l’una sintattica ed esistenziale, l’altra semantica e universale; il corso dimostra tuttavia che $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$. Ne segue che ogni domanda su ciò che segue da certe premesse può ricevere risposta dal lato più facile: esibendo una deduzione, percorrendo una tavola o, come insegna l’ultima lezione di contenuto, refutando per risoluzione.

Destinatari e conoscenze preliminari

Il corso si rivolge a chi inizia studi di matematica, di informatica o di filosofia, e a chi, in qualunque fase della propria formazione, voglia sapere con esattezza che cos’è una dimostrazione e perché ci si può fidare di essa: studenti che si avvicinano alla matematica universitaria e inciampano nelle dimostrazioni, studenti di informatica che hanno bisogno della logica dei circuiti, dei programmi e dei problemi di soddisfacibilità, e studenti di filosofia che vogliono passare dalla logica degli argomenti alla sua teoria.

È un corso di livello 1, senza prerequisiti e autosufficiente. Non presuppone di aver studiato logica, né di conoscere la teoria degli insiemi, né di aver mai dimostrato un teorema. Ciò che usa degli insiemi (appartenenza, inclusione, unione, insiemi di formule), delle funzioni (un’assegnazione è una funzione dalle variabili in $\{0, 1\}$), delle stringhe di simboli e dell’induzione, lo insegna nel punto in cui ne ha bisogno: gli insiemi e le stringhe, nella lezione dell’unità 1 sul linguaggio, e l’induzione, nella lezione seguente, prima di usarla. Presuppone soltanto due cose: leggere con attenzione, perché in un linguaggio formale un simbolo aggiunto o omesso cambia la stringa, e l’aritmetica elementare dei numeri naturali, che in questo corso, come nel resto del sito, cominciano da $1$.

Dove conduce

Da quanto precede segue il posto del corso nel sito. Non ha prerequisiti ed è meta di tre percorsi di studio, Matematica, Informatica e Filosofia, perché in tutti e tre il ragionamento è insieme strumento e oggetto. Ha tre corsi complementari, che si possono seguire prima, in parallelo o dopo, in qualunque ordine. Logica Aristotelica studia la logica dei termini e il sillogismo, la cui validità dipende da parole come «tutti» e «qualche», che questo corso lascia fuori, e mostra da quale tradizione si è giunti al calcolo. Algebra e Geometria I innalza un edificio deduttivo a partire dagli assiomi di Peano, e mette in pratica, sui numeri, il metodo assiomatico e l’induzione che questo corso studia come oggetto; il suo piano raccomanda di aver studiato prima questo corso, o di studiarlo in parallelo. Programmazione in C++ I, infine, porta alla pratica ciò che qui è teoria: decidere se una stringa è ben formata, percorrere una tavola di verità, calcolare una forma normale o cercare una refutazione sono procedure che si possono scrivere come programmi.

Ora, il corso lascia aperta una questione di espressività: il suo linguaggio non può dire «tutti» né «qualche», e la formalizzazione degli argomenti dell’italiano perde, fin dall’unità 1, i quantificatori. Pertanto, la sua continuazione prevista è la Logica Matematica II, dedicata alla logica dei predicati, che percorrerà lo stesso cammino con quantificatori e variabili che variano su oggetti: conserverà la correttezza, la completezza e la compattezza, con metodi che questo corso anticipa, ma in essa la conseguenza cesserà di essere decidibile.

Obiettivi di apprendimento globali

Gli obiettivi seguenti descrivono che cosa deve saper fare chi completa il corso. Ciascuno è formulato come una prestazione osservabile, in modo che si possa verificare con un compito concreto; ogni lezione di contenuto dichiara a sua volta i propri obiettivi, che servono uno o più di quelli globali, e la lezione di chiusura mostra in quali unità e lezioni si lavora su ciascuno. I sette obiettivi sono numerati perché si possano citare.

1. Obiettivo 1. Distinguere il linguaggio oggetto dal metalinguaggio, e decidere con le regole di formazione se una stringa è una formula.
2. Obiettivo 2. Formalizzare enunciati e argomenti del linguaggio naturale, indicando che cosa la formalizzazione conserva e che cosa perde.
3. Obiettivo 3. Costruire deduzioni nel sistema del corso (gli assiomi di Łukasiewicz, il modus ponens e la sostituzione della doppia negazione), combinando assiomi, regole primitive e regole derivate.
4. Obiettivo 4. Dimostrare metateoremi per induzione sui numeri naturali, sulla complessità delle formule e sulla lunghezza delle deduzioni.
5. Obiettivo 5. Decidere validità, soddisfacibilità, conseguenza ed equivalenza semantiche, con tavole di verità e con equivalenze.
6. Obiettivo 6. Trasformare formule in forme normali ed esprimere con esse funzioni di verità e circuiti.
7. Obiettivo 7. Spiegare e applicare la correttezza, la completezza e la compattezza, e decidere l’insoddisfacibilità per risoluzione.

Gli obiettivi 3 e 7 hanno ciascuno la propria unità, la deduzione e la metateoria; gli obiettivi 5 e 6 si spartiscono l’unità di semantica, il primo nella sua prima metà, il secondo nella seconda. L’obiettivo 2 ha una lezione propria, quella della formalizzazione, e si esercita poi ogni volta che un problema viene posto a parole. Gli obiettivi 1 e 4, invece, sono trasversali: la distinzione tra ciò che si dice dentro il linguaggio e ciò che si dice su di esso attraversa le quattro unità, e l’induzione è la forma di tutte le dimostrazioni importanti del corso, dalla leggibilità unica delle formule fino alla correttezza del sistema e al lemma di Kalmár. Ne segue che il loro raggiungimento non può essere attribuito a una sola lezione, e che conviene coltivarli lungo l’intero corso.

Il sistema del corso e le sue decisioni

Un corso di logica proposizionale si può costruire in molti modi, e i testi abituali differiscono nel linguaggio, nei connettivi primitivi e nel sistema deduttivo. Questo corso prende tre decisioni che conviene conoscere fin dall’inizio, perché spiegano ciò che, a prima vista, può sembrare strano.

Una lingua di cerchi e dischi

Il linguaggio del corso ha un alfabeto di soli due simboli, il cerchio $\sigO$ e il disco $\sigI$. La $n$-esima variabile è la stringa di $n$ cerchi seguiti da un disco, $v_{n} = \sigO^{n}\sigI$, sicché $v_{1} = \sigO\sigI$ e $v_{2} = \sigO\sigO\sigI$; e c’è una sola regola di formazione: se $\varphi$ e $\psi$ sono formule, lo è anche $\sigI\varphi\psi$, che si abbrevia $(\varphi \downarrow \psi)$ e si legge «né $\varphi$ né $\psi$». La negazione congiunta $\downarrow$ è dunque l’unico connettivo primitivo, e tutti gli altri sono abbreviazioni definite una sola volta: $\neg\varphi$ è $(\varphi \downarrow \varphi)$, la disgiunzione $(\varphi \vee \psi)$ è $\neg(\varphi \downarrow \psi)$, e a partire da esse si definiscono la congiunzione, l’implicazione, la doppia implicazione e la disgiunzione esclusiva. Qualsiasi altro modo di scriverle è un teorema, che si dimostra, e non una definizione.

La scelta ha un prezzo, la leggibilità, che il corso paga nel metalinguaggio: nessuno scrive quotidianamente stringhe di cerchi e dischi, ma i loro nomi abbreviati, espandibili in qualunque momento fino alla stringa che designano. Ora, essa rende molte volte. Due simboli bastano per infinite variabili, sicché ogni formula è una stringa finita su un alfabeto di due elementi. Il connettivo si scrive davanti ai suoi argomenti, e perciò non servono parentesi: la leggibilità unica si dimostra con un argomento di peso, che assegna $+1$ a ogni variabile e $-1$ a ogni disco connettivo. E poiché ogni formula composta è una negazione congiunta, ogni dimostrazione per induzione sulla complessità ha un solo caso composto, il che abbrevia tutte quelle delle unità successive. Che un solo connettivo basti per esprimere qualunque altro non si presuppone: l’unità di semantica lo dimostra.

Una seconda regola primitiva

Il sistema deduttivo parte da quello di Jan Łukasiewicz: tre schemi di assiomi, scritti con la negazione e l’implicazione, e il modus ponens come unica regola. Questi schemi furono formulati per linguaggi i cui connettivi primitivi sono la negazione e l’implicazione; nella lingua di cerchi e dischi, una formula come $(v_{1} \downarrow v_{2})$ non è né l’una né l’altra, e per gli assiomi è opaca. La prima lezione dell’unità di deduzione dimostra, con un marchio che tutti gli assiomi possiedono, che il modus ponens conserva e che la formula non possiede, che il sistema di Łukasiewicz non deduce $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$.

Se così è, il sistema va completato, e il rimedio naturale sembra dimostrare la doppia negazione, $\varphi \dashv\vdash \neg\neg\varphi$, che la seconda lezione deduce dai tre schemi. Il marchio mostra che ciò non basta: i teoremi della doppia negazione lo conservano e, tuttavia, nemmeno con essi si scambia $v_{1}$ con $\neg\neg v_{1}$ dentro una negazione congiunta. Pertanto, dopo aver dimostrato la doppia negazione, la seconda lezione aggiunge una seconda regola primitiva, la sostituzione della doppia negazione: da una formula $\chi$ si inferisce quella che risulta sostituendo in essa un’occorrenza di una sottoformula $\theta$ con $\neg\neg\theta$, o una di $\neg\neg\theta$ con $\theta$. Il sistema del corso consta, dunque, dei tre schemi di Łukasiewicz, del modus ponens e di questa regola.

Altri sistemi per la negazione congiunta ottengono lo stesso con schemi di assiomi fatti su misura. Il corso preferisce una regola per due ragioni: è ancora più semplice del modus ponens, perché prende una sola riga e cambia una sola occorrenza, e non ha nulla di artificioso, perché esprime ciò che la doppia negazione già dice, che $\theta$ e $\neg\neg\theta$ sono intercambiabili, esteso a ogni punto di una formula. È, inoltre, corretta, perché conserva il valore di verità di ogni riga, e preserva il teorema di deduzione, con un caso in più nella sua dimostrazione. Che con essa basti per dedurre tutto ciò che deve essere dedotto è il teorema di completezza dell’ultima unità.

La compattezza prima della completezza forte

La completezza ammette tre gradi: la debole dice che ogni tautologia è un teorema; la finita, che ogni conseguenza di un insieme finito di premesse si deduce da esso; la forte, che lo stesso vale per un insieme qualsiasi, anche infinito. Il metodo del corso, il lemma di Kalmár, lavora con le variabili, in numero finito, di una formula e con premesse finite, e perciò raggiunge i primi due gradi e non il terzo. Per arrivarci basta che, se $\Gamma \models \varphi$, qualche parte finita $\Gamma_{0}$ di $\Gamma$ soddisfi già $\Gamma_{0} \models \varphi$; ora, questo è precisamente ciò che afferma il teorema di compattezza.

Molti testi dimostrano prima la completezza forte con un altro metodo e ne deducono la compattezza. In questo corso, invece, la completezza forte è ciò che si cerca, e ottenere da essa la compattezza sarebbe circolare. Donde l’ordine si inverte: la lezione sulla compattezza la dimostra dentro la semantica, senza menzionare alcuna deduzione, fissando uno a uno i valori di $v_{1}, v_{2}, \ldots$, e solo dopo, in tre righe, ottiene la completezza forte, cioè $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ per ogni insieme $\Gamma$.

Contenuti

Il corso si organizza in sei unità: questa presentazione, quattro unità di contenuto e una chiusura. Ogni unità di contenuto si apre con una lezione di introduzione, che presenta le sue lezioni, il suo posto nel corso, ciò che dà per noto e il problema che risolve, e comincia con una valutazione d’ingresso; si chiude con una lezione di sintesi, che ricostruisce la catena deduttiva dell’unità, la collega al resto del corso, ripete in una valutazione d’uscita le abilità di quella d’ingresso e propone sei sfide di difficoltà superiore a quella dei problemi delle lezioni.

Unità 0. Presentazione del corso

Consta di questa lezione, che fissa lo scopo, gli obiettivi globali, le decisioni, i contenuti, l’impegno e la progettazione del corso.

Unità 1. Linguaggio

Il suo obiettivo è costruire il linguaggio che il corso studia, dimostrare che ogni formula si legge in un solo modo e collegarlo agli argomenti dell’italiano.

1. Linguaggio: introduzione.
2. Che cos’è la logica matematica: la validità di fronte alla verità, il controesempio, i paradossi e la distinzione tra linguaggio oggetto e metalinguaggio.
3. Il linguaggio della logica proposizionale: insiemi e stringhe, la lingua di cerchi e dischi, la sua regola di formazione e le sue abbreviazioni.
4. Induzione sui numeri naturali e sulle formule: induzione semplice, forte e strutturale, il lemma del peso, la leggibilità unica e le definizioni per ricorsione.
5. Formalizzazione del linguaggio naturale: il dizionario, la traduzione di enunciati e argomenti, e ciò che perde il condizionale materiale.
6. Linguaggio: sintesi e sfide.

Unità 2. Deduzione

Il suo obiettivo è dare al linguaggio un calcolo, il sistema del corso, e derivare in esso, una sola volta ciascuna, le forme di ragionamento che la matematica usa senza nominarle.

1. Deduzione: introduzione.
2. Sistemi deduttivi formali: il sistema di Łukasiewicz, la deduzione con premesse, il teorema di deduzione e il marchio che ne mostra il limite.
3. Quattro tecniche di deduzione: il sillogismo ipotetico, lo scambio delle premesse, la doppia negazione, la contrapposizione e la sostituzione della doppia negazione.
4. Le simmetrie dei connettivi: il lemma fondamentale della negazione congiunta, la sostituzione di equivalenti, le forme equivalenti della disgiunzione e della congiunzione e le loro cinque simmetrie.
5. Le tecniche della logica classica: le regole di ogni connettivo, il terzo escluso, la prova per casi e la riduzione all’assurdo, con premesse.
6. Leggi di De Morgan e leggi distributive: le loro dimostrazioni in entrambi i sensi e la sostituzione di equivalenti dentro altre formule.
7. Deduzione: sintesi e sfide.

Unità 3. Semantica

Il suo obiettivo è dare alle formule un significato, decidere con esso la validità e la conseguenza, e ridurre ogni formula a forme normali.

1. Semantica: introduzione.
2. Semantica della logica proposizionale: le assegnazioni e la loro estensione per ricorsione, il lemma di coincidenza, le tavole di verità, la validità e la soddisfacibilità.
3. Conseguenza ed equivalenza semantica: la conseguenza a partire da insiemi, il teorema di deduzione semantico, la sostituzione semantica e la sostituzione uniforme.
4. Leggi generalizzate di De Morgan e distributive: congiunzioni e disgiunzioni di $n$ termini e le loro leggi, per induzione.
5. Completezza funzionale: ogni funzione di verità ha una formula, la negazione congiunta basta da sola, e gli insiemi adeguati di connettivi.
6. Forme normali: letterali, clausole, forme disgiuntiva e congiuntiva, la loro dualità e la loro esistenza.
7. L’algoritmo delle forme normali e le sue applicazioni: un algoritmo corretto e che termina, e la progettazione e la semplificazione di circuiti di interruttori.
8. Semantica: sintesi e sfide.

Unità 4. Metateoria

Il suo obiettivo è dimostrare che la deduzione e la conseguenza coincidono, prima per premesse finite e poi per premesse qualsiasi, e offrire un terzo modo di deciderle.

1. Metateoria: introduzione.
2. Correttezza e completezza: la correttezza per induzione sulle righe, la coerenza, il lemma di Kalmár e la completezza debole e finita.
3. Il teorema di compattezza: la sua dimostrazione semantica, le sue forme equivalenti, la completezza forte che ne segue e le sue applicazioni combinatorie.
4. Il metodo di risoluzione: la forma a clausole, la regola di risoluzione, la sua correttezza e la sua completezza refutazionale, e il suo costo.
5. Metateoria: sintesi e sfide.

Unità 5. Chiusura del corso

Consta della lezione Bilancio finale di Logica Matematica I, che richiama i sette obiettivi globali, mostra in una figura in quali unità e lezioni si lavora su ciascuno, riunisce per obiettivo il primo tentativo delle valutazioni d’uscita e indica dove prosegue lo studio.

Impegno e crediti

L’impegno di un corso non si misura in ore di lezione frontale, che in un corso asincrono non esistono, ma nel lavoro totale di chi lo studia: leggere, seguire le dimostrazioni e le deduzioni, risolvere problemi e ripassare. La stima segue lo stesso metodo in tutti i corsi del sito: conta il tempo di lettura del testo di ogni lezione a cento parole al minuto, contando ogni formula come una parola, venti minuti per problema risolto, trentacinque per problema proposto, quarantacinque per sfida e dodici per valutazione d’ingresso o d’uscita, e aggiunge un margine di un decimo per il ripasso.

Risultati

Le lezioni del corso contengono nel complesso $90$ problemi risolti, $90$ problemi proposti e $24$ sfide, oltre a otto valutazioni di unità. L’impegno stimato per unità, arrotondato all’ora, è il seguente:

• Unità 0, presentazione del corso: meno di $1$ ora.
• Unità 1, linguaggio: $30$ ore.
• Unità 2, deduzione: $36$ ore.
• Unità 3, semantica: $43$ ore.
• Unità 4, metateoria: $25$ ore.
• Unità 5, chiusura del corso: meno di $1$ ora.

Il totale è di circa $137$ ore di lavoro. Conviene leggere questa cifra per ciò che è: una stima per chi studia tutte le dimostrazioni e risolve tutti i problemi e le sfide. Chi abbia già studiato logica, o si limiti ai problemi proposti senza affrontare le sfide, impiegherà parecchio meno; chi non abbia mai dimostrato un teorema può averne bisogno di più, soprattutto nelle unità di deduzione e di semantica, che sono anche le più estese.

Ora, la cifra è nominale: è quella che fissa i crediti del corso, e presuppone una lettura a ritmo costante e tre quarti d’ora per sfida. Finché non sarà misurata con studenti reali, conviene accompagnarla con un intervallo realistico. Se la lettura procedesse a metà del ritmo supposto, come accade quando si ricopia ogni deduzione con carta e matita e si scompone a mano ogni stringa di cerchi e dischi, e ogni sfida richiedesse settantacinque minuti invece di quarantacinque, lo stesso metodo darebbe circa $174$ ore. Pertanto, l’impegno prevedibile si colloca tra circa $137$ e circa $174$ ore. L’estremo superiore è una stima prudente, non una misurazione; l’intervallo sarà corretto quando si conoscerà il tempo che impiegano coloro che studiano il corso, e fino ad allora i crediti si calcolano con la cifra nominale.

Ritmo suggerito

Per denominare i ritmi, questo piano segue lo stesso criterio degli altri piani del sito: l’impegno a tempo pieno è quello di un anno accademico di $60$ crediti, circa $1650$ ore distribuite in una quarantina di settimane, cioè circa $40$ ore settimanali, e l’impegno a tempo parziale ne è la metà, circa $20$ ore settimanali. Ne segue un ritmo raccomandato di un semestre di sedici settimane, con circa $8$ o $9$ ore settimanali di studio, poco più della quinta parte del tempo pieno; con l’intervallo realistico, da $9$ a $11$ ore settimanali. Questo semestre si può condividere con Algebra e Geometria I, le cui dimostrazioni si leggono meglio quando la deduzione è già un oggetto noto.

Un ritmo intensivo, di circa $20$ ore settimanali, cioè a tempo parziale, conclude il corso in sette settimane. Un ritmo più disteso, di circa $4$ o $5$ ore settimanali, lo porta a due semestri, che lo ripartiscono quasi a metà: le unità da 0 a 2, il linguaggio e la deduzione, occupano circa $67$ ore, e le unità da 3 a 5, la semantica, la metateoria e la chiusura, circa $69$.

Equivalenza in crediti trasferibili

I sistemi di crediti trasferibili misurano un corso in base al lavoro totale che richiede a chi lo segue, e non alle ore di lezione in presenza, affinché gli studi compiuti in un’istituzione possano essere riconosciuti in un’altra. Il Sistema europeo di trasferimento e accumulazione dei crediti, adottato dalle università europee a partire dalla Dichiarazione di Bologna, assegna $60$ crediti a un anno accademico a tempo pieno, e fissa ogni credito tra $25$ e $30$ ore di lavoro. Il Sistema di crediti trasferibili del Cile, adottato dalle università cilene con un impianto analogo, assegna anch’esso $60$ crediti all’anno accademico e fissa ogni credito tra $24$ e $31$ ore di lavoro.

Ora, dividendo le $137$ ore stimate per gli estremi di ciascun intervallo, il corso equivale a circa $5$ crediti europei (da 4,6 a 5,5), e a tra $4$ e $6$ crediti trasferibili cileni (da 4,4 a 5,7). Prendendo come riferimento il valore centrale di entrambi gli intervalli, 27,5 ore per credito, si ottiene nei due sistemi lo stesso numero, 4,98, che si arrotonda a 5. Per i crediti europei, il numero $C$ di crediti risulta così delimitato:

Pertanto, si raccomanda di assegnare al corso $5$ crediti europei e $5$ crediti trasferibili cileni, cioè la dodicesima parte di un anno accademico a tempo pieno, poco meno di un insegnamento semestrale corrente di sei crediti.

Progettazione del corso

Modalità

Il corso è asincrono, online e a ritmo autonomo: non ha date, sessioni dal vivo né scadenze, e ogni studente avanza alla velocità che gli consentono la sua preparazione e il suo tempo. È offerto nelle quattordici lingue del sito, con la stessa logica in tutte: le formule, le deduzioni e i passi delle dimostrazioni sono identici in ogni versione, e si traduce soltanto il testo. Le lezioni dichiarano quali altre lezioni conviene aver studiato prima, sicché l’ordine raccomandato è esplicito.

La struttura di una lezione

Tutte le lezioni di contenuto seguono la stessa struttura. Cominciano con un riassunto e con un elenco di obiettivi di apprendimento propri, formulati come prestazioni osservabili. Seguono la teoria, con le definizioni, i risultati enunciati con precisione e le loro dimostrazioni, e gli esempi. Le dimostrazioni si presentano come riproduttori passo per passo: ogni passo scrive una riga, illumina ciò che cambia e, quando si appoggia su un risultato precedente, vi ritorna. Le deduzioni del sistema si scrivono con le righe numerate e la giustificazione di ciascuna a destra (un assioma, una premessa, il modus ponens con le righe che usa, o una regola derivata), e avanzando si illuminano le righe citate. Chiudono la lezione cinque problemi risolti, con la loro soluzione passo per passo, e cinque problemi proposti, ciascuno con un suggerimento ripiegato e, poi, la risposta finale; i problemi proposti di dimostrazione aggiungono, ripiegata dopo la risposta, una soluzione svolta, che conviene aprire solo dopo aver redatto la propria.

Ogni lezione si può inoltre ascoltare ad alta voce con il lettore del sito, che pronuncia a parole i simboli delle formule, compresi il cerchio, il disco e i simboli della deduzione e della conseguenza.

Valutazione

Il corso non assegna voti: la sua valutazione è formativa e si basa sull’autovalutazione. I problemi proposti permettono di verificare il raggiungimento degli obiettivi di ogni lezione, e le sfide, quello degli obiettivi di ogni unità. A ciò si aggiungono le valutazioni di unità: quella d’ingresso, all’inizio dell’introduzione, misura il punto di partenza con da undici a quindici domande, perché a quelle dell’unità ne aggiunge alcune su ciò che l’unità dà per noto; quella d’uscita, nella sintesi e prima delle sfide, misura quanto raggiunto con dodici domande e si confronta con quella d’ingresso. Entrambe si correggono nel browser stesso, con una spiegazione per ogni risposta e un rinvio alla lezione che conviene ripassare; i loro risultati si conservano soltanto nel browser di chi le compila, e il bilancio finale riunisce il primo tentativo di ogni valutazione d’uscita in un profilo per obiettivo globale.

Come studiare questo corso

Il corso è stato pensato per essere studiato in ordine. Ogni unità presuppone le precedenti: la deduzione si scrive con il linguaggio della prima, la semantica dà valore alle sue formule, e la metateoria confronta la seconda con la terza; saltare una lezione obbliga, prima o poi, a tornarvi.

In ogni lezione conviene leggere prima il riassunto e gli obiettivi; studiare poi la teoria con carta e matita, ricopiando le stringhe di cerchi e dischi, separandone le variabili e i dischi, e anticipando ogni riga di una deduzione prima che il riproduttore la scriva; tentare i problemi risolti prima di guardarne la soluzione, e risolvere i proposti senza aiuto, aprendo il suggerimento solo quando il tentativo si è esaurito. Un problema la cui risposta si è consultata prima di tentarlo non è stato risolto, ma letto.

Infine, conviene distinguere sempre di quale livello è ogni affermazione: se dice qualcosa dentro il linguaggio, come una formula, o qualcosa su di esso, come $\Gamma \vdash \varphi$ o $\Gamma \models \varphi$. Questa distinzione, che è il primo degli obiettivi del corso, è anche quella che permette di capire il suo risultato centrale, che si può enunciare soltanto nel metalinguaggio.