Assurdo in un contesto / logico

• Assurdo logico: nel contesto dei blocchi Tet(a) ∧ Cube(a)
• Per dimostrare che Q segue logicamente P1, P2, ... Pn (in un contesto C) assumo ¬Q e dimostro in C l'assurdo (cioè dimostro ⊥ usando l'assunzione ¬Q, le premesse P1, ... Pn e le proprietà del contesto C)

Assurdo tautologico / proposizionale

• Assurdo proposizionale: è la contraddizione P∧¬P falsa in tutte le interpretazioni booleane
• Per dimostrare che Q segue tautologicamente P1, ... Pn assumo ¬Q e dimostro l'assurdo usando solo regole tautologicamente valide (cioè dimostro ⊥ usando l'assunzione ¬Q e le premesse P1, ... Pn, ovvero senza usare le proprietà del contesto)

¬ Intro

• Per inferire ¬P, si può usare una sottoprova per mostrare che P→⊥. Per introduzione di not si inferisce ¬P selezionando la sottoprova

¬ Elim

• si può inferire P da ¬¬P applicando l'eliminazione del not.