Cosa fare e come consegnare

Scaricate il file exercise-settheory.ma (usando il pulsante destro sul link e selezionando Save link as' o qualcosa di simile). Poi aprite il file salvato lanciando un terminale e lanciando il comando ~sacerdot/matita_gtk3/helm/matita/matita/matita.opt exercise-set_theory.ma dalla directory in cui l'avete salvato.

Per prima cosa all'inizio del file riempite i campi con i vostri nomi, cognomi e numero di matricole.

Durante la prova ricordatevi di salvare costantemente per non perdere il lavoro in caso di crash. Matita fa dei salvataggi automatici, ma non fidatevi.

Alla fine dell'esercitazione o del tempo consegnate il file con il comando `~sacerdot/logica1920/ConsegnaLogica exercise-set_theory.ma'.

Come scrivere i simboli

Per inserire i simboli matematici è necessario digitare il loro nome e poi premere ALT-L. In generale i nomi dei simboli sono della forma \nome, ad esempio \equiv. Alcuni simboli molto frequenti hanno dei sinonimi più comodi da digitare, per esemio ha sia il nome \Rightarrow sia =>.

Segue un elenco dei simboli più comuni e i loro nomi separati da virgola, Se sono necessari dei simboli non riportati di seguito si può visualizzare l'intera lista dal menù a tendina View ▹ TeX/UTF8 table.

La sintassi ∀x.P significa "per tutti gli x vale P".

La sintassi F → G dove F e G sono proposizioni nel metalinguaggio significa "F implica G". Attenzione, il simbolo (usato a lezione) non ha lo stesso significato in Matita.

La sintassi ℕ → ℕ è il tipo delle funzioni che preso un numero naturale restituiscono un numero naturale.

Tutti gli operatori sono associativi a sinistra, tranne `→'.

Il linguaggio di dimostrazione di Matita

Gli esercizi di questa lezione richiedono di scrivere una dimostrazione. Tale dimostrazionedeve essere scritta utilizzando il linguaggio di dimostrazione di Matita. Tale linguaggio è composto dai seguenti comandi:

Teoremi e assiomi

Per concludere le dimostrazioni potete utilizzare i seguenti assiomi e teoremi

Assiomi:

Teoremi dimostrati nel laboratorio 1:

Teoremi dimostrati (o da dimostrare) nel corso di questo laboratorio: