Matematica e logica: sintesi e sfide

Riepilogo

Questa lezione chiude la quarta unità del corso, dedicata alla matematica e alla logica. Ricostruisce la catena di principi e di meccanismi che va dal modo matematico agli alberi di deduzione, indicando in ogni anello quale principio si usa e in quale lezione viene stabilito; colloca ciò che si è ottenuto rispetto al piano del corso e precisa quali questioni, appena anticipate, restano per le unità successive; ripete nella valutazione d’uscita le competenze della valutazione d’ingresso; e termina con sei sfide, di difficoltà superiore a quella dei problemi delle lezioni, che richiedono di combinarne parecchie per comporre una dispensa con enunciati, dimostrazione e rimandi, diagnosticare documenti che compilano con difetti che nulla segnala, trasporre una notazione logica da una tradizione all’altra, costruire e correggere una deduzione con più rami, prevedere la numerazione e le grandezze di una relazione di fisica, e riunire due preamboli incompatibili.

Obiettivi di apprendimento

Ricostruire l’ordine dei meccanismi dell’unità, individuando il principio su cui ciascuno si fonda.
Spiegare perché tanti difetti della scrittura matematica compilano senza avviso, e dove cercarne la traccia nel risultato o nel log.
Distinguere ciò che l’unità ha stabilito da ciò che ha soltanto anticipato e che le unità successive svilupperanno.
Prevedere i numeri, i rimandi e le grandezze che produce un sorgente con equazioni, enunciati e unità, e correggerlo.
Progettare un preambolo che fissi la notazione, gli enunciati e l’ordine di caricamento dei pacchetti di un lavoro, e che permetta di cambiare convenzione senza toccare il corpo del testo.

Ciò che l’unità ha ottenuto

L’unità si è proposta che ogni segno di una formula sia composto secondo ciò che significa, e che la notazione di un lavoro sia la stessa in tutte le sue pagine. Lo scopo è stato raggiunto appoggiandosi su ciò che l’introduzione ha dichiarato noto dalle unità precedenti: i rimandi, che dipendono da ciò che un’etichetta registra; i comandi propri, che concentrano le decisioni di forma nel preambolo; e la lettura del log. Con ciò, il cammino percorso si può leggere come un’unica catena in cinque tratti.

Formule in linea e in display

La lezione sulle formule in linea e in display ha stabilito il principio da cui dipendono quasi tutti gli altri: nel modo matematico gli spazi del sorgente non contano, e il motore separa ogni segno secondo la sua classe, ordinario, operatore binario, relazione, punteggiatura, apertura o chiusura. Ne ha dedotto perché una variabile non si scrive con \textit, perché $3,5$ dà «3, 5» e perché la punteggiatura della frase va fuori dalla formula in linea. Ha mostrato che in LuaLaTeX una lettera greca fuori dal suo modo non produce errore, ma scompare o compare senza controllo, con un’unica riga «Missing character» nel log; ha punteggiato la formula in display come parte della frase, senza righe vuote e senza $$; ha numerato con equation, \eqref, \numberwithin e \tag; ha distinto \text da \mathrm; e ha studiato la virgola decimale, che babel in italiano non produce (a differenza di babel in spagnolo) e che si scrive tra graffe, il pacchetto icomma, e siunitx, che richiede una propria dichiarazione del separatore, locale = IT.

Simboli e notazione

La lezione sui simboli e la notazione è partita da una regola di raggruppamento: ^ e _ agiscono su un solo elemento o su un gruppo tra graffe. Ha percorso frazioni, radici, lettere greche e alfabeti, tra cui le combinazioni che con fontspec si perdono senza errore, come \mathbf{\Gamma}; gli operatori con nome, che babel in italiano non cambia né completa (sen e tg dell’uso scolastico si dichiarano nel preambolo), con ciò che vi cambia babel in spagnolo, il caso più netto (\lim con l’accento, \sen nuovo, \sin intatto), e ciò che sopprime es-minimal; i grandi operatori, i delimitatori e le loro dimensioni; la ricerca di un simbolo sconosciuto; e unicode-math, con le sue quattro precauzioni. Ha terminato portando la notazione nel preambolo, in comandi propri che si decidono una volta.

Equazioni su più righe

La lezione sulle equazioni su più righe ha sostituito le formule impilate e eqnarray con align, con la & prima della relazione, e ha stabilito che un ambiente di allineamento è una tabella: una riga per ogni \\ e una cella per ogni tratto tra due &. Ne ha dedotto i difetti silenziosi (il =&, la & di troppo, la doppia barra finale che numera una riga vuota, l’etichetta su una riga con \notag) e gli errori rumorosi; ha scelto tra gather, multline, split, aligned e gathered secondo il numero che l’insieme deve portare; ha composto definizioni per casi con cases e dcases, testo con \intertext, matrici e matrici complete; ha numerato gruppi con subequations e ha permesso l’interruzione di pagina.

Teoremi e dimostrazioni

La lezione sui teoremi e le dimostrazioni ha portato all’enunciato l’idea di dichiarare invece di imitare: con amsthm, \newtheorem fissa l’intestazione, il numero e lo stile di ogni tipo di enunciato. Ha dedotto quando conviene il contatore condiviso e quando quelli separati, quando la numerazione per sezione o per capitolo, e quale stile corrisponde a ciò che si afferma, a ciò che si stabilisce e a ciò che accompagna. Ha composto le dimostrazioni con proof, la cui intestazione viene da babel, e ha corretto con \qedhere il quadratino orfano; ha rimandato con cleveref, caricato dopo amsthm, con un \crefname per ambiente, e ha scoperto che con il contatore condiviso di \newtheorem cleveref chiama «teorema» ogni enunciato, difetto che thmtools corregge.

Logica e deduzioni

La lezione sulla logica e le deduzioni ha separato il linguaggio oggetto dal metalinguaggio, con \to di fronte a \Rightarrow e i segni \vdash, \models e \equiv; ha applicato il principio della classe del segno alla tilde della negazione, alla barra degli insiemi e ai due punti delle funzioni; ha proposto un comando per connettivo, senza argomenti per cambiare segni e con argomenti per cambiare sintassi; ha riunito i pacchetti dei segni modali; ha composto tavole di verità con array; e ha costruito alberi di deduzione naturale con bussproofs, la cui logica a pila spiega i suoi due errori, insieme alle scatole di Fitch e agli argomenti in forma standard.

La figura seguente riunisce i cinque tratti in un’unica catena. Ogni nodo della colonna è un meccanismo o una regola, numerato secondo l’ordine in cui si appoggiano gli uni sugli altri e unito da un arco agli anelli precedenti che usa; attorno fluttuano i sostegni, cioè i principi a cui la catena ricorre di continuo, ciascuno unito da un tratto pieno agli anelli che vi si appoggiano e da uno punteggiato all’anello in cui viene stabilito, salvo quelli stabiliti in unità precedenti, che si disegnano come anelli vuoti. Facendo clic su un sostegno si evidenziano tutti gli anelli che lo usano, e ogni anello rimanda alla lezione in cui si studia.

Sostegni della catena

ACiò che registra un’etichetta. Un’etichetta registra l’ultimo numero assegnato prima di essa, all’interno del suo ambiente, senza sapere a che cosa è unita. Si stabilisce nell’unità precedente. Ammesso senza dimostrazione in questa unità.
BComandi propri. Un comando proprio nomina una funzione, e la sua definizione, scritta una volta nel preambolo, ne fissa la forma; cambiarla cambia tutto il documento. Si stabilisce nell’unità precedente. Ammesso senza dimostrazione in questa unità.
COrdine di caricamento. I pacchetti si caricano nell’ordine in cui vengono letti, e uno successivo regola, conserva o disfa ciò che ha fatto uno precedente. Si stabilisce nell’unità precedente. Ammesso senza dimostrazione in questa unità.
DLa classe del segno. Nel modo matematico il motore separa ogni segno secondo la sua classe (ordinario, operatore binario, relazione, punteggiatura, apertura, chiusura) e ignora gli spazi del sorgente. Stabilito in: 1. Due modi.
ECiò che scompare senza errore. In LuaLaTeX, un segno che il font in uso non contiene non ferma la compilazione: scompare, e lascia nel log soltanto una riga «Missing character». Stabilito in: 2. Segni nel modo sbagliato.
FUn elemento o un gruppo. I pedici, gli esponenti e gli argomenti agiscono sull’elemento che segue o su un gruppo tra graffe, che non si stampano. Stabilito in: 6. Pedici ed esponenti.
GUn allineamento è una tabella. Un ambiente di allineamento costruisce una riga per ogni \\ e una cella per ogni tratto tra due &, anche se la riga resta vuota. Stabilito in: 11. Allineare con align.
HLa pila di alberi. Un’inferenza con n premesse prende gli ultimi n alberi della pila e ne restituisce uno; la prova si stampa se alla fine ne resta esattamente uno. Stabilito in: 23. Alberi di deduzione.

Tratto 1 Formule in linea e in display
- Prevedere il risultato di un segno, di una variabile o di una parola scritti nel modo sbagliato.
- Punteggiare le formule in linea e in display come parti della frase.
- Numerare le formule in display e rimandarvi.
- Scrivere decimali e grandezze secondo l’uso italiano, con siunitx o senza.
1. Due modi. Nel modo matematico le lettere sono variabili, gli spazi del sorgente non contano, la spaziatura la decide la classe di ogni segno e non è ammessa una riga vuota.
  Si appoggia su: D (La classe del segno). Dimostrato in: Formule in linea e in display.
2. Segni nel modo sbagliato. Un _ nel testo dà «Missing $ inserted»; \alpha fuori dalla formula scompare o compare attaccato; una parola dentro la formula è un prodotto di variabili e va in \text o in \mathrm, che non sono intercambiabili.
  Usa: 1. Due modi. Si appoggia su: E (Ciò che scompare senza errore). Dimostrato in: Formule in linea e in display.
3. La formula nella frase. La formula in linea limita la sua altezza e lascia fuori la punteggiatura della frase; la formula in display si punteggia dentro, senza righe vuote, con \[…\] o equation e mai con $$.
  Usa: 1. Due modi. Si appoggia su: D (La classe del segno). Dimostrato in: Formule in linea e in display.
4. Numerare e rimandare. equation numera e la sua etichetta va dentro; \eqref mette le parentesi; \numberwithin numera per sezione; \tag mette un contrassegno senza consumare numero.
  Usa: 3. La formula nella frase. Si appoggia su: A (Ciò che registra un’etichetta). Dimostrato in: Formule in linea e in display.
5. Virgola decimale. La virgola della formula è punteggiatura; babel in italiano non converte il punto in virgola (babel in spagnolo sì); {,} vale sempre, e siunitx chiede locale = IT o output-decimal-marker.
  Usa: 1. Due modi. Si appoggia su: D (La classe del segno). Dimostrato in: Formule in linea e in display.
Tratto 2 Simboli e notazione
- Raggruppare pedici ed esponenti e prevedere ciò che manca senza graffe.
- Scegliere alfabeto, variante e operatore secondo la convenzione della disciplina.
- Prevedere ciò che babel cambia negli operatori: nulla in italiano, molto in spagnolo.
- Fissare la notazione del documento nel suo preambolo.
1. Pedici ed esponenti. x^10 eleva solo l’1; x^{10} eleva il gruppo; due indici dello stesso tipo di seguito danno «Double subscript» o «Double superscript».
  Usa: 1. Due modi. Si appoggia su: F (Un elemento o un gruppo). Dimostrato in: Simboli e notazione.
2. Lettere e alfabeti. Ogni alfabeto dice quale tipo di oggetto si nomina; con fontspec, \mathbf{\Gamma} scompare e \mathbf{\alpha} non esce in grassetto, e il grassetto di un simbolo è \boldsymbol.
  Usa: 6. Pedici ed esponenti. Si appoggia su: E (Ciò che scompare senza errore). Dimostrato in: Simboli e notazione.
3. Operatori con nome. Gli operatori vanno in tondo con il loro spazio; babel in italiano non cambia nulla né definisce \sen, mentre babel in spagnolo accentua \lim, \max, \min e \inf, definisce \sen e non tocca \sin, e es-minimal sopprime tutto ciò.
  Usa: 6. Pedici ed esponenti. Si appoggia su: D (La classe del segno). Dimostrato in: Simboli e notazione.
4. Delimitatori. \left e \right misurano ciò che racchiudono e vanno in coppia; le dimensioni manuali danno un controllo fine; mathtools definisce coppie come \abs.
  Usa: 6. Pedici ed esponenti. Si appoggia su: D (La classe del segno), F (Un elemento o un gruppo). Dimostrato in: Simboli e notazione.
5. La notazione nel preambolo. \R, \vect, \dd o \abs si definiscono una volta; unicode-math va dopo amsmath, senza amssymb dietro, e richiede \symbf per il grassetto.
  Usa: 7. Lettere e alfabeti, 8. Operatori con nome, 9. Delimitatori. Si appoggia su: B (Comandi propri), C (Ordine di caricamento), E (Ciò che scompare senza errore). Dimostrato in: Simboli e notazione.
Tratto 3 Equazioni su più righe
- Allineare catene e sistemi con align, con la & prima della relazione.
- Decidere quali righe si numerano e prevedere i numeri.
- Scegliere l’ambiente secondo la struttura e il numero dell’insieme.
- Comporre definizioni per casi, matrici e testo intercalato.
1. Allineare con align. La & va prima della relazione e \\ apre una riga; =& e una & di troppo cambiano il risultato senza avviso, e una riga vuota ferma la compilazione.
  Usa: 3. La formula nella frase. Si appoggia su: G (Un allineamento è una tabella), D (La classe del segno). Dimostrato in: Equazioni su più righe.
2. Quali righe si numerano. align numera ogni riga, anche quella vuota che lascia un \\ finale; \notag toglie il numero senza consumarlo, e un’etichetta su quella riga registra quello della riga numerata successiva.
  Usa: 11. Allineare con align, 4. Numerare e rimandare. Si appoggia su: G (Un allineamento è una tabella), A (Ciò che registra un’etichetta). Dimostrato in: Equazioni su più righe.
3. Un numero per l’insieme. split dentro equation dà un numero alla catena; aligned e gathered sono blocchi senza numero; subequations dà lettere a un gruppo che consuma un solo numero.
  Usa: 11. Allineare con align, 12. Quali righe si numerano. Si appoggia su: A (Ciò che registra un’etichetta). Dimostrato in: Equazioni su più righe.
4. Casi, matrici e testo. cases ha due colonne e trasforma una & di troppo in fine riga; dcases compone a dimensione di display; le matrici ammettono dieci colonne; array traccia barre; \intertext non rompe l’allineamento.
  Usa: 11. Allineare con align. Si appoggia su: G (Un allineamento è una tabella). Dimostrato in: Equazioni su più righe.
Tratto 4 Teoremi e dimostrazioni
- Dichiarare gli enunciati con il loro stile e il loro contatore.
- Prevedere la numerazione di una serie condivisa o separata.
- Chiudere le dimostrazioni con il simbolo al suo posto.
- Rimandare agli enunciati con il loro nome.
1. Enunciati dichiarati. \newtheorem di amsthm, nel preambolo, fissa intestazione, numero e aspetto; l’intestazione la scrive l’autore, e la forma con asterisco non numera.
  Si appoggia su: B (Comandi propri). Dimostrato in: Teoremi e dimostrazioni.
2. Contatori e stili. [teorema] fa un’unica serie, il cui numero dice il posto; [section] o [chapter] numera per divisione; plain, definition e remark rispondono a ciò che si afferma, si stabilisce o accompagna.
  Usa: 15. Enunciati dichiarati. Si appoggia su: B (Comandi propri). Dimostrato in: Teoremi e dimostrazioni.
3. Dimostrazioni. proof prende l’intestazione da babel e mette il quadratino al termine dell’ultimo capoverso; se termina con una formula o un elenco, \qedhere lo mette al suo posto, salvo accanto a un numero.
  Usa: 15. Enunciati dichiarati, 11. Allineare con align. Dimostrato in: Teoremi e dimostrazioni.
4. Rimandare agli enunciati. L’etichetta va dentro l’ambiente; amsthm si carica prima di cleveref, con un \crefname per ambiente; con il contatore condiviso di \newtheorem tutto si chiama «teorema», e thmtools lo corregge.
  Usa: 16. Contatori e stili, 4. Numerare e rimandare. Si appoggia su: A (Ciò che registra un’etichetta), C (Ordine di caricamento). Dimostrato in: Teoremi e dimostrazioni.
Tratto 5 Logica e deduzioni
- Distinguere nella notazione il linguaggio oggetto dal metalinguaggio.
- Correggere la spaziatura della tilde, della barra, dei due punti e dei quantificatori.
- Cambiare tradizione dal preambolo.
- Costruire e correggere alberi di deduzione, tavole di verità e argomenti.
1. Due livelli di linguaggio. \to è il connettivo del linguaggio oggetto e \Rightarrow la freccia del metalinguaggio; \vdash afferma la deduzione e \models la conseguenza semantica.
  Usa: 8. Operatori con nome. Dimostrato in: Logica e deduzioni.
2. La spaziatura logica. \sim è una relazione e va tra graffe; la barra della tastiera è ordinaria e \mid una relazione; : è relazione e \colon punteggiatura; la portata di un quantificatore la decide una parentesi.
  Usa: 19. Due livelli di linguaggio, 5. Virgola decimale. Si appoggia su: D (La classe del segno). Dimostrato in: Logica e deduzioni.
3. Un comando per connettivo. Senza argomenti, il comando cambia il segno da una tradizione all’altra; con argomenti, la definizione decide anche l’ordine e le parentesi, e permette la notazione polacca.
  Usa: 20. La spaziatura logica, 10. La notazione nel preambolo. Si appoggia su: B (Comandi propri), F (Un elemento o un gruppo). Dimostrato in: Logica e deduzioni.
4. Segni modali e tavole di verità. \Box, \Diamond e \vDash richiedono amssymb, e latexsym caricato prima cambia il rombo; la tavola di verità è un array con V e F in tondo.
  Usa: 19. Due livelli di linguaggio, 14. Casi, matrici e testo. Si appoggia su: C (Ordine di caricamento), G (Un allineamento è una tabella). Dimostrato in: Logica e deduzioni.
5. Alberi di deduzione. In bussproofs, \AxiomC mette una foglia e le inferenze prendono gli ultimi alberi; se mancano, «Hypotheses missing!»; se avanzano, «Proof tree badly specified.» al momento di stampare.
  Usa: 19. Due livelli di linguaggio. Si appoggia su: H (La pila di alberi). Dimostrato in: Logica e deduzioni.
6. Scatole e forma standard. logicproof compone le scatole di Fitch come una tabella con subproof; un argomento in forma standard numera le premesse e separa la conclusione con un filetto e \therefore.
  Usa: 23. Alberi di deduzione, 22. Segni modali e tavole di verità. Si appoggia su: G (Un allineamento è una tabella). Dimostrato in: Logica e deduzioni.

Verso le tabelle e le figure. La catena si ferma dove le formule, gli enunciati e le deduzioni sono completi e numerati: la tabella, che qui è servita soltanto alle matrici, alle tavole di verità e alle prove, cresce nell’unità successiva fino alle tabelle e alle figure del documento, con le loro didascalie, i loro numeri e il loro posto nella pagina.