Laboratorio del corso di Logica

Anno accademico 2022/23

Turno B

Docente: Camillo Fiorentini

Avvisi

A partire da martedì 9 maggio, la lezione di laboratorio si svolgerà nel laboratorio 307.

Orario delle lezioni

Per le informazioni sull'organizzazione del corso (suddivisione in turni, esami, ecc.) fare riferimento alla pagina del corso di Logica (vedere anche gli avvisi pubblicati su Ariel).

Sono previste 11 lezioni:
28 febbraio; 7, 14, 21, 28 marzo; 4 aprile.
2, 9, 16, 23, 30 maggio.

Eventuali variazioni di orario verranno comunicate nella sezione Avvisi di questa pagina.

Ricevimento

Si raccomando di usare il proprio indirizzo di posta di ateneo (della forma nome.cognome@studenti.unimi.it) e di indicare il proprio nome e cognome.

Libro di testo di riferimento

Materiale relativo alle lezioni

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

Tabella dei predicati del linguaggio dei blocchi (pdf).

Regole in Fitch (pdf).

• 28 febbraio - Laboratorio 1
  Introduzione all'uso di Tarski's World. Documentazione online (in inglese).
• 7 marzo - Laboratorio 2
  
  • Parte 1.
    • Definizione di modelli in Tarski: 3.3, 3.13.
    • Traduzione da linguaggio naturale: 3.21, tradurre almeno 5 frasi (traduzione in italiano). L'esercizio 3.22 propone dei test per verificare la correttezza delle traduzioni fatte.
  • Parte 2.
    • Costruzione tavole di verità in Bool, verificare se le proposizioni sono tautologie: 4.2.
    • Continuazione esercizio 4.2: 4.3 (annotare risposte su file .txt).
  • Parte 3.
    • Esercizio 4.9.1 (stabilire enunciati tautologicamente possibili: 1,2,3,5,6,7,8,10): costruire la tabella come file .txt.
    • Esercizio 4.9.2 (stabilire enunciati possibili nel mondo dei blocchi: 1,2,3,5,6,7,8,10): costruire la tabella come file .txt.
    • Facoltativo 4.9.3.
• 14 marzo - Laboratorio 3
  • Dimostrare in Fitch le seguenti argomentazioni, non vanno usate regole Ana Con e Taut Con: 6.5, 6.6, 6.8 (da completare).
  • 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, è possibile derivare il ⊥ dalle assunzioni Cube(a) e Tet(a), in quanto un blocco non può essere contemporaneamente un cubo e un tetraedro): 6.11, 6.12, 6.13, 6.36.
  • Costruire una derivazione in Fitch per i seguenti ragionamenti (sono tutti validi); non vanno usate regole Ana Con e Taut Con: 6.18, 6.19, 6.20, 6.24, 6.25.
• 21 marzo - Laboratorio 4
  • Parte 1
    • 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).
      Facoltativo: per controllare la soluzione, vedere esercizio 7.13.
    • Costruzione di un modello (in Tarski): 7.14.
  • Parte 2
    • I seguenti ragionamenti possono essere veri o falsi. Se veri, costruire una derivazione in Fitch, senze usare Taut Con né Ana Con, 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 né 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.
• 28 marzo - Laboratorio 5
  Esercizi riassuntivi sulla logica proposizionale (derivazioni in Fitch, controesempi). Nelle derivazioni in Fitch, usare Taut Con e Ana Con solo se esplicitamente consentito. Si raccomanda di impostare su carta lo schema della dimostrazione prima di scriverla in Fitch.
  
  • Parte 1
    Derivazioni in Fitch di ragionamenti validi (nota): 8.33 (esercizio svolto, traduzione formale del ragionamento dell'esercizio 8.5), 8.31 (traduzione formale di 8.3; è possibile usare Taut Con per introdurre una istanze del principio del terzo escluso), 8.32 (traduzione di 8.4), 8.34 (è possibile usare Ana Con per derivare ⊥ da due proposizioni atomiche), 8.35.
  • Parte 2
    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 (il ragionamento è valido, usare TautCon per introdurre una opportuna istanza del principio del terzo escluso), 8.46, 8.47, 8.48, 8.52.
    Ulteriori esercizi: 8.49, 8.50, 8.51, 8.53.
    
• 4 aprile - Laboratorio 6
  Semantica dei quantificatori. Tutti gli esercizi richiedono l'uso di Tarski.
  • Parte 1
    • Verifica sintassi formule (Tarski): 9.1.
  • Parte 2
    • Valutazione della validità di un enunciato in un mondo, con uso di Play Game: 9.5 (1,2,3,12,13,14,15,20,23,25).
      Ulteriori esercizi: 9.5 (4,5,6,7,8,9,10,11,16,17,18,19,21,22,24,26,27,28,29,30)
  • Parte 3
    • Costruzione di modelli: 9.9.
    • Validità di enunciati in un modello e traduzione (con uso Play Game) : 9.10.
    • Costruzione di modelli o mostrare che non esistono: 9.11.
    • Completare modello: 9.14.
• 2 maggio - Laboratorio 7
  Semantica dei quantificatori.
  • Parte 1
    • Esercizi di traduzione (da svolgere usando Tarski): 9.16 (esistenziali), frasi 1-8 (traduzione in italiano).
      9.17 (universali), frasi 1-8 (traduzione in italiano).
      Come ulteriore esercizio, tradurre le rimanenti frasi.
  • Parte 2
    • Le seguenti argomentazioni sono valide. Distinguere se sono (a) conseguenza tautologica, (b) conseguenza del primo ordine (FO) ma non conseguenza tautologica, (c) conseguenza nel mondo dei blocchi ma non conseguenza tutologica e neppure conseguenza al primo ordine. In quest'ultimo caso, descrivere in un file di testo un controesempio.
      Esercizi: 10.10, 10.11, 10.12, 10.13, 10.14, 10.17
      Facoltativo: costruire le derivazioni in Fitch delle precedenti argomentazioni; se necessario, usare la regola Ana Con per derivare ⊥ da due proposizioni atomiche.
  • Parte 3
    • Determinare se le formule sono (a) tautologie, (b) verità logiche, (c) non vere. Usare Fitch con Taut Con e FO Con per controllare le risposte.
      Esercizi 10.1 (1-5).
      Ulteriori esercizi: 10.1 (6-10).
      Facoltativo: costruire le derivazioni in Fitch delle precedenti argomentazioni; se necessario, usare la regola Ana Con per derivare ⊥ da due proposizioni atomiche.
• 9 maggio - Laboratorio 8
  • Parte 1
    Esercizi di traduzione (alternanze di quanticatori, verica con Tarski): 11.16 (2,4,6,8,10) (traduzione in italiano); 11.17 (2,4,6,8,10) (traduzione in italiano).
    Ulteriori esercizi: tradurre le rimanenti frasi.
  • Parte 2
    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.
• 16 maggio - Laboratorio 9
  • 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.24, 13.25, 13.26, 13.27.
  • Costruire una derivazione in Fitch delle seguenti argomentazioni; è possibile usare TautCon per giustificare i passaggi che richiedono solo regole proposizionali.
    Esercizi 13.28, 13.29 (provare che assumendo ¬∃x Cube(x), si dimostra ⊥), 13.30, 13.31.
  • Costruire una derivazione in Fitch delle seguenti argomentazioni; è possibile usare TautCon e, dove strettamente necessario, AnaCon (solo per introdurre conclusioni atomiche o ⊥, avendo come premesse formule atomiche).
    Esercizi 13.34, 13.35.
  • Costruire una derivazione in Fitch delle seguenti argomentazioni; è possibile usare TautCon per giustificare i passaggi che richiedono solo regole proposizionali.
    Esercizi 13.43 (provare che, assumendo ¬∃x¬ Cube(x), si dimostra ⊥), 13.44, 13.45, 13.46, 13.49.
• 23 maggio - Laboratorio 10
  • Derivazioni in Fitch con principio di induzione (regola Peano Induction).
    Esercizi 16.29, 16.30, 16.31, 16.33 (vedere il suggerimento nel testo dell'esercizio).
  • Traduzioni con quantificazioni numeriche: esercizio 14.3 (traduzione in italiano e commenti).
  • Derivazioni in Fitch, è possibile usare TautCon per passaggi proposizional1.
    Esercizi 14.10, 14.11.
• 30 maggio - Laboratorio 11
  • Derivazioni in Fitch (senza induzione).
    Esercizi 13.47, 13.48, 13.50.
  • Derivazioni in Fitch che richiedono l'induzione (regola Peano Induction).
    Esercizi 16.34 (induzione su z), 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, usando induzione e usando come lemma l'esercizio 16.29, in cui si dimostra che ∀ x (0 + x = x) (e la dimostrazione richiede l'uso dell'induzione).
    Per usare una formula F come lemma è possibile seguire uno dei seguenti modi:
    1. si introduce F nella dimostrazione usando la regola Add Lemma... (dal menu Rule? che si usa quando si applica una regola, selezionare Lemma e poi Add Lemma...). È richiesto di includere un file .prf che contenga la derivazione della formula F. In questo modo il sistema verifica che la formula F possa essere correttamente usata come lemma (ossia, le assunzioni usate per dimostrare il lemma sono implicate dalle assunzioni del ragionamento che si sta considerando).
    2. (Consigliato). Più semplicemente, si aggiunge F alle premesse della argomentazione (eventualmente inserendo come commento che si tratta di un lemma già dimostrato). Usare il comando Add Premise del menu Proof; va prima attivata l'opzione Author mode del menu Edit. Notare che in questo modo il sistema non può controllare che il lemma sia usato in modo coerente.
    Esercizio 16.44, senza induzione; usare come lemma la formula ∀x ∀y (x + s(y) = s(x) +y) (esercizio 16.33).
    Esercizio 16.45, senza induzione; usare come lemma la formula ∀x ∀y ∀z( x+z = y+z → x = y) (esercizio 16.35) e la formula ∀x ∀y ( x+y = y+x) (esercizio 16.36).