Cosa fare e come consegnare

Scaricate il file exercise-set-theory.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.

• ∨ : \or
• ∧ : \and
• ¬ : \lnot
• → : \to, ->
• ⇔ : \iff
• ∀ : \forall
• ∈ : \in
• ∪ : \cup
• ∩ : \cap
• ∅ : \empty
• ⊆ : \sube

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:

• assume nome : tipo

  Quando si deve dimostrare un tesi come ∀F : Formula.P, il comando assume F : Formula fissa una generica Formula F e la tesi diventa P dove F è fissata.

• suppose P (nome)

  Quando si deve dimostrare una tesi come P → Q, il comando suppose P (Ipotesi1) da il nome Ipotesi1 a P e cambia la tesi Q, che ora può essere dimostrata facendo riferimento all'assunzione P tramite il nome Ipotesi1.

• we procede by cases on x to prove Q

  Si usa quando si vuole usare una disgiunzione per dimostrare una proposizione Q. x deve essere il nome di una disgiunzione nelle ipotesi del goal corrente.

• case name

  Nelle prove per induzione o per casi, ogni caso deve iniziare con il comando case nome, ad esempio se si procede per casi su una disgiunzione si dovrà analizzare prima il caso in cui sia vera la sottoformula sinistra e poi il caso in cui sia vera la formula di destra; in entrambi i casi la sottodimostrazione comincierà con case nome. dove nome serve come chiarimento all'utente.

• by name1,name2,... we proved P (name)

  Permette di ottenere una nuova ipotesi P chiamandola name utilizzando le ipotesi name1,name2... bisogna prestare attenzione a elencare tutte le ipotesi necessarie (assiomi, ipotesi, regole dei connettivi, eventuali teoremi).

• by name1,name2,... done

  Termina un caso della dimostrazione se quello che dobbiamo dimostrare è una banale conseguenza delle ipotesi name1,name2,...

• by name we have F1 (name1) and F2 (name2)

  Quando name è una ipotesi del tipo F1 ∧ F2, si ottengono due nuove ipotesi chiamate name1 e name2 di tipo rispettivamente F1 e F2.

• we need to prove F (name)

  Inizia una sotto-dimostrazione di F. Una volta conclusa, si riprende la dimostrazione precedente con in più l'ipotesi name che F valga.

• using (ABSURDUM name) done

  Conclude la dimostrazione quando name è l'ipotesi che False valga

Teoremi e assiomi

Per concludere le dimostrazioni potete utilizzare i seguenti assiomi e teoremi

Assiomi:

• conj: ∀A, B. A → B → A ∧ B
• conj: ∀A, B. (A → B) → (B → A) → A ⇔ B
• or_introl: ∀A, B. A → A ∨ B
• or_intror: ∀A, B. B → A ∨ B
• ax_extensionality: ∀A, B. (∀Z. Z ∈ A ⇔ Z ∈ B) → A = B
• ax_inclusion1: ∀A, B. A ⊆ B → (∀Z. Z ∈ A → Z ∈ B)
• ax_inclusion2: ∀A, B. (∀Z. Z ∈ A → Z ∈ B) → A ⊆ B
• ax_empty: ∀X. ¬(X ∈ ∅)
• ax_intersect1: ∀A,B. ∀Z. (Z ∈ A ∩ B → Z ∈ A ∧ Z ∈ B)
• ax_intersect2: ∀A,B. ∀Z. (Z ∈ A ∧ Z ∈ B → Z ∈ A ∩ B)
• ax_union1: ∀A,B. ∀Z. (Z ∈ A ∪ B → Z ∈ A ∨ Z ∈ B)
• ax_union2: ∀A,B. ∀Z. (Z ∈ A ∨ Z ∈ B → Z ∈ A ∪ B)
• ax_powerset1: ∀A. ∀Z. (Z ∈ powerset A → Z ⊆ A)
• ax_powerset2: ∀A. ∀Z. (Z ⊆ A → Z ∈ powerset A)

Teoremi dimostrati nel laboratorio 1:

• union_inclusion: ∀A, B. A ⊆ A ∪ B
• union_idempotent: ∀A. A ∪ A = A
• intersection_idempotent: ∀A. A ∩ A = A
• empty_absurd: ∀X, A. X ∈ ∅ → X ∈ A
• intersect_empty: ∀A. A ∩ ∅ = ∅
• union_empty: ∀A. A ∪ ∅ = A
• intersect_commutative: ∀A,B. A ∩ B = B ∩ A
• union_commutative: ∀A,B. A ∪ B = B ∪ A
• distributivity1: ∀A,B,C. A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)
• distributivity2: ∀A,B,C. A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)

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

• antisymmetry_inclusion: ∀A,B. A ⊆ B → B ⊆ A → A = B
• reflexivity_inclusion: ∀A. A ⊆ A
• transitivity_inclusion: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C
• powerset_emptyset: ∀A. A ∈ powerset ∅ → A = ∅
• union_powerset: ∀A, B. (powerset A) ∪ (powerset B) ⊆ powerset (A ∪ B)
• intersection_powerset: ∀A, B. (powerset A) ∩ (powerset B) = powerset (A ∩ B)