1. Perché le logiche modali normali hanno bisogno di essere chiuse per Sostituzione Uniforme? Se non c’è questa proprietà, l’insieme di formule è lo stesso? Vedi appunti
  2. Perché in calcolo assiomatico una derivazione è una sequenza mentre in G3 è un albero? Per ragioni storiche
  3. Qual è la differenza tra G3 e G3C? G3 famiglia di calcoli, G3C per la logica classica
  4. Profondità e altezza di una derivazione sono la stessa cosa? Sì
  5. La nostra interpretazione della proprietà 3 di G3 è corretta? Sì
  6. Cosa vuol dire che G3K è un calcolo cut-free per $K$? G3C non è già cut-free? G3C è cut-free per la logica proposizionale classica e G3K per la logica K
  7. Dato che $L\square$ e $R\Diamond$ possono essere applicate infinite volte, l’interpretazione semantica per cui quando siam bloccati abbiamo un controesempio, salta? Ovvero, come facciamo a capire quando ci siamo bloccati?
  8. Nel linguaggio etichettato che abbiamo definito, vale la regola $LR\square$? $LR\square$ vale nel calcolo di Gentzen (esteso con quella regola). Gentzen + $LR\square$ è un calcolo cut-free per la logica modale ma non è invertibile
  9. Qual è il metodo per trasformare una formula del tipo $\forall \vec{x} \left ( (P_1 \land P_2 \dots ) \supset \exists \vec{y} ( Q_1 \lor Q_2 \dots ) \right )$ in una regola? Vedi appunti su carta
  10. Perché la regola di Euclide ha bisogno della forma contratta? Perché se v e u sono la stessa etichetta e le due formule principali sono identiche, se applichi dall’alto al basso Euclid puoi dover fare ulteriormente Euclid, ma hai solo due copie e quindi non potresti applicarlo in alcuni casi. Quindi aggiungi anche la forma contratta.
  11. Qual è la regola corrispondente alla confluenza?
  12. Chiarimento dimostrazione pp-invertibilità. In particolare, nei casi induttivi in cui la formula è principale non usiamo l’IH? Già
  13. Dimostrazione dei due corollari extra dell’ammissibilità del taglio Vedi aggiunte agli appunti
  14. Che differenza c’è tra peso e lunghezza di una formula? Sono uguali
  15. Devo ricordarmi confluenza etc?

Solo regole a sinistra, solo su formule atomiche, rappresentano un assioma del tipo “congiunzione di atomi ⇒ disgiunzione di atomi”, chiuse sotto contrazioni (aggiungi tutte le versioni contratte che servono). Ciò non è restrittivo, perché ci sono regole per trasformare assiomi del prim’ordine in regole di questo tipo