Appunti di Informatica

APPUNTI DI INFORMATICA

UNIVERSITÀ DI TRENTO

PROF. ROBERTO ZUNINO

CORSO DI LAUREA IN MATEMATICA

RICCARDO TOSI

NOTAZIONE LOGICA

• ∨ o / or: p ∨ q - p oppure q
• ∧ / and: p ∧ q - p and q
• →: p → q: se p allora q
• ⊥: falso
• ¬: non

Una formula dimostrabile è detta TEOREMA.

Durante una dimostrazione:

• l’insieme delle formule dette ipotesi (già conosciute come valide)
• la formula è detta TESI
• Regola BASE: la tesi dimostrata finita (T vera per ipotesi)

Regole logiche di:

• Introduzione: dimostrazione di un connettivo nella tesi
• Eliminazione: sfruttare un connettivo bo

AND INTRODUZIONE

p ∧ q nella tesi, si riduce la dimostrazione in due:

AND ELIMINAZIONE

p ∧ q nell'ipotesi, si aggiungono due ipotesi, p e q:

Esempio:

Regola base: 1,P5 " P2

RT

APPUNTI DI INFORMATICA

UNIVERSITÀ DI TRENTOPROF. ROBERTO ZUNINO

CORSO DI LAUREA IN MATEMATICA

RICCARDO TOSI

NOTAZIONE LOGICA

• ∨ : or
• ∧: and
• ¬ : not
• → : implica

Una formula dimostrabile è detta TEOREMA

Durante una dimostrazione:

• Ipotesi : formule dette ipotesi (già conosciute come valide)
• Tesi : formula detta TESI
• Regola base : E^F dimostrazione finita (Γ vera per ipotesi)

Regole logiche di:

1. Introduzione: dimostrazione di un connettivo nella tesi
2. Eliminazione: sfruttare un connettivo

AND - INTRODUZIONE

p∧q nella tesi; si rande la dimostrazione in due:

• Γ⊢p →Γ⊢q →Γ⊢p∧q

AND - ELIMINAZIONE

p∧q nell’ipotesi; si aggiungono due ipotesi p e q

• Γ⊢p∧q ⊢p; ⊢q ⊢Γ⊢t

Esempio:

• IP1: p∧(q∧r) tesi: x⊢∧p

1. Eliminazione
   • IP2: p
   • IP3: q∧r
   • IP4: ∧r (q∧r)
2. Eliminazione
   • IP4: q
   • IP5: r
3. Introduzione
   • IP5: x

∧&Lambda:_p^x

π: Regel Base. IP5 ∨ IP2

RT:

OR - INTRODUZIONE

- Si sceglie arbitrariamente una proposizione

IP1: p∨q

• oppure
• ten: p∨q

Se p non si dimostra si prova con q

OR - ELIMINAZIONE

Vi si aggiusta la dimostrazione aggiungendo come ipotesi, p, l'altra, q. Se entrambe i rami sono corretti allora la dimostrazione è vera.

Esempio:

IP1: p∨q

• Introducendo la tes. p∨q
• ten: q

IP2: IP1

• Eliminando l'HP:
• IP3: IP1
• ten: p

IP2: q

• ten: IP1: q∨p
• ten: q
• ten: IP2: IP1
• ten: q
• IP2: q
• ten: q
• IP3: q
• ver

Ciò dimostra che l'OR è COMMUTATIVO

IMPLICA - INTRODUZIONE

p→q

• Si assume p per vera e la q assume tra le ipotesi
• IP:
• IP2: q
• ten: q

IMPLICA - ELIMINAZIONE

p→q Primma si dimostra p, poi si assume l'ipotese q

IP2: q

Esempio:

IP:

• IP1: q
• IP2: q
• ten: q
• IP:
• IP1: q

SE E SOLO SE

p ↔ q (p→q) ∧ (q→p)

• Se e solo se è una doppia implicazione (equivalenza)
• Un circolo di implicazioni in un verso implica l'implicazione nel verso opposto per transitività dell'implicazione

VERO - INTRODUZIONE

──────────

• Fine della dimostrazione

ten: vero

VERO - ELIMINAZIONE

Non esiste un'ipotesi che dice vero è inutile

Esempio:

(p→vero) → (p→q)

• IP:
• ten: q
• p→vero
• p→
• p→vero
• ten: p→vero

• IP1: p
• IP: p→vero
• IP1: p
• vero
• ten: vero

Ciò dimostra che "vero" è l'elemento neutro di ⊺

Falso - Introduzione

Non esiste (bisogna ricavare il falso dalle ipotesi)

Falso - Eliminazione

Un ipotesi falsa permette di ricavare qualunque cosa, pertanto la dimostrazione finisce.

Falso ⊢ trovare che ⊥ → falso

Esempio:

1P.1: P

P→(F→Falso)

⟹ P∨Falso

1P.