Laboratorio del corso di Logica

Anno accademico 2018/2019

Turno C (cognomi P-Z)

Docente: Alberto Momigliano

Avvisi

Date appelli

Le informazioni sugli esami (orari, esiti, ecc.) sono pubblicate sulla pagina del corso di Logica.

Orario delle lezioni

Giovedì, 13:45-16:30, laboratorio sigma.
Sono previste 11 lezioni:
Eventuali variazioni saranno comunicate in questa pagina.

Ricevimento

Nel mio ufficio, Celoria 18, 4009 su appuntamento (momigliano@di.unimi.it).

Libro di testo di riferimento

Dave Barker-Plummer, Jon Barwise and John Etchemendy, Language, Proof and Logic, second edition, CSLI publications.

Materiale relativo alle lezioni

Esercizi del libro di testo: Cap. 2-8 (pdf), Cap. 9-14 (pdf), Cap. 16 (pdf).

Lezioni

28 Feb - Laboratorio 1

Introduzione all'uso delle applicazioni Tarski's World e Fitch. Documentazione on-line: FAQ, Support, and Feedback .
Definizione di modelli in Tarski. Esercizi: 3.3, 3.13.
Contromodelli in Tarski. Esercizi: 2.25, 2.26
Derivazioni in Fitch usando regole di uguaglianza. Esercizi: 2.17, 2.18.

14 marzo - Laboratorio 2

Traduzione da linguaggio naturale.
Esercizi 3.21 e 3.22 (i due esercizi sono collegati), tradurre almeno 5 frasi (traduzione in italiano).
Costruzione di tavole di verità con Boole; nozioni di tautologia, equivalenza logica, conseguenza tautologica.
Esercizi. Tautologie: 4.2, 4.3 (annotare risposta su file di testo). Equivalenze tautologiche: 4.12. Conseguenze tautologiche: 4.21 (casa: 4.17, 4.20).
Derivazioni in Fitch usando regole per i connettivi and/or/=: 6.2, 6.3, 6.4 (casa: 6.5, 6.6). Non si usi la regola Taut Con.

21 marzo - Laboratorio 3

Nei seguenti esercizi, se il ragionamento è valido costruire una derivazione in Fitch, altrimenti costruire un controesempio in Tarski. è possibile usare Ana Con solo per introdurre ⊥ avendo come assunzioni due proposizioni atomiche che nel mondo dei blocchi si contraddicono l'un l'altra (ad esempio, Cube(a) e Tet(a)): 6.11, 6.12, 6.13.
Costruire una derivazione in Fitch per i seguenti ragionamenti (sono tutti validi): 6.8 (da completare). Sottoprove annidate: 6.18, 6.19, (casa: 6.20). Formali vs. informali: 6.24, 6.25, (casa: 6.36).

28 marzo - Laboratorio 4

Verifica dell'equivalenza tatutologica di due proposizioni mediante le tavole di verità (da costruire usando Boole): 7.2, 7.5.
Traduzione di proposizioni da linguaggio naturale (scrivere le proposizioni in Tarski): 7.12; tradurre almeno 1,2,3,5,6,7,8 (traduzione in italiano).
Per controllare la soluzione, vedere esercizio 7.13.
Costruzione di un modello (in Tarski): 7.14.
I seguenti ragionamenti possono essere veri o falsi. Se veri, costruire una derivazione in Fitch, altrimenti costruire un contromodello in Tarski (in quest'ultimo caso le formule A, B e C vanno istanziate con opportune formule del linguaggio di Tarski): 8.20, 8.21, 8.22, 8.23, 8.24.
Derivazioni in Fitch di ragionamenti validi. Non usare Taut Con e neppure Ana Con. Si raccomanda di impostare su carta lo schema della dimostrazione prima di scriverla in Fitch: 8.26, 8.28.
Nei seguenti esercizi è possibile usare TautCon per introdurre istanze del principio del terzo escluso: 6.40, 6.41.

4 aprile - Laboratorio 5

Esercizi riassuntivi sulla logica proposizionale (derivazioni in Fitch, controesempi). Si raccomanda di impostare su carta lo schema della dimostrazione prima di scriverla in Fitch.

Derivazioni in Fitch di ragionamenti validi (vedasi 8.3 -- 8.9): se potete, non usate Taut Con, ma lemmi precedentemente dimostrati, per esempio il terzo escluso: 8.31, 8.32 , 8.33, 8.34 (è possibile usare Ana Con per derivare ⊥ da due proposizioni atomiche), 8.35.
Se il ragionamento è valido, costruire una derivazione in Fitch, altrimente fornire un controesempio con Tarski. È possibile usare Ana Con per derivare ⊥ da due proposizioni atomiche: 8.44, 8.45, 8.46, 8.47, 8.48, 8.52.
Da svolgere a casa: 8.49, 8.50, 8.51, 8.53.

11 aprile - Laboratorio 6

Simulazione di esame in classe: collegarsi su UPLOAD.

2 Maggio - Laboratorio 7

Semantica dei quantificatori.

Costruzione di modelli: 9.9, 9.11, 9.14.
Esercizi di traduzione: 9.16 (1-8, traduzione in italiano), 9.17 (1-8, traduzione in italiano); completare gli esercizi a casa, facendo le verifiche suggerite dal testo.
Forma vero-funzionale di un enunciato: 10.1.
Analisi vero-funzionale di argomentazioni valide (conseguenza tautologica, conseguenza al primo ordine (FO), conseguenza nel mondo dei blocchi).
Se la argomentazione è valida nel mondo dei blocchi ma non al primo ordine, definire un contromodello su carta o su un file testo (txt).
Esercizi: 10.10, 10.11, 10.12, 10.13, 10.14, 10.17.

9 Maggio - Laboratorio 8

Esercizi da svolgere in LOGI.
Analisi vero-funzionale di argomentazioni valide (conseguenza tautologica, conseguenza al primo ordine (FO), conseguenza nel mondo dei blocchi).
Per le seguenti argomentazione valida nel mondo dei blocchi ma non al primo ordine, definire un contromodello usando LOGI.
Esercizi: 10.11, 10.14, 10.17.

Verificare la validità delle seguenti argomentazioni. Se il ragionamento è valido costruire una derivazione in Fitch, altrimenti costruire un contromodello con Tarski. Nelle derivazioni in Fitch è possibile usare TautCon per giustificare i passaggi che richiedono solo regole proposizionali.
Esercizi 13.2, 13.3, 13.4, 13.5, 13.11, 13.12, 13,13, 13.14, 13.15, 13.16.

Esercizi di traduzione da linguaggio naturale: 11.16, utilizzando il file Montague's Sentences (traduzione in italiano), 11.17 (traduzione in italiano).
Per casa facendo le verifiche suggerite dal testo.

16 maggio - Laboratorio 9

Breve verifica degli esercizi assegnati la volta scorsa

Altri esercizi da svolgersi con LOGI:

Verificare la validità delle seguenti argomentazioni al prim'ordine. Se il ragionamento è valido costruire una derivazione in Fitch, altrimenti costruire un contromodello con Tarski. Nelle derivazioni in Fitch è possibile usare TautCon per giustificare i passaggi che richiedono solo regole proposizionali.
Esercizi 13.24, 13.25, 13.26, 13.27.

Costruire una derivazione in Fitch delle seguenti argomentazioni;
Esercizi 13.28, 13.30, 13.31.

23/30 maggio - Laboratorio 10/11

Costruire una derivazione in Fitch delle seguenti argomentazioni:
Esercizi 13.43, 13.44, 13.45, 13.46, 13.47, 13,48, 13.49, 13.50. Potete usare TautCon.

Derivazioni in Fitch con principio di induzione (Peano Induction). Esercizi 16.29, 16.30, 16.31, 16.33 (vedere il suggerimento sul libro). Esercizi 16.34 (suggerimento sul libro), 16.35 (induzione su z).

Derivazioni in Fitch con uso di definizioni.
Esercizi che non richiedono l'induzione: 16.39, 16.40, 16.41, 16.42. Esercizio 16.43, aggiungendo fra le premesse la formula ∀ x (0 + x = x) (già dimostrata usando l'induzione nell'esercizio 16.29). Occorre usare induzione (regola Peano Induction).
Per aggiungere una premessa: usare il comando Add Premise del menu Proof; va prima attivata l'opzione Author mode del menu Edit.
Esercizio 16.44, senza induzione; aggiungere la premessa ∀x ∀y (x + s(y) = s(x) +y) (esercizio 16.33).

Esercizio di traduzione: 14.3 (traduzione in italiano e commenti).

Esercizi da svolgersi con LOGI con interpretazione du funzioni.