Lezione 15, martedì 7 novembre 2017 // Quantificatori, negazione delle proposizioni quantificate, dimostrazione e uso delle proposizioni quantificate,

I temi di questa lezione:

1. qual è la negazione di una proposizione quantificata universalmente e qual è la negazione di una proposizione quantificata esistenzialmente: la negazione di "per  ogni x di tipo T, vale A[x]" è "per qualche x di tipo T, vale la negazione di  A[x]", e la negazione di "per qualche x di tipo T, vale A[x]" è "per ogni x di tipo T, vale la negazione di A[x]", 
2. le regole per dimostrare e per usare le proposizioni quantificate. 

Le regole più interessanti (e non banali) sono quelle per dimostrare una proposizione quantificata universalmente e per usare una proposizione quantificata esistenzialmente:

- dimostrare una proposizione universale "per  ogni x di tipo T, vale A[x]" è dimostrare la proposizione A[a] dove a è un oggetto di tipo T e nella dimostrazione è trattato come un oggetto “generico” (ossia nella dimostrazione si usa dell’oggetto a solo le proprietà che gli spettano in quanto oggetto di tipo T);

-  dall'ipotesi (dall'informazione) che "per qualche x di tipo T, vale A[x]" si può passare a dire che vale A[a] per uno specifico oggetto a di tipo T sul quale nel proseguire la dimostrazione non si usa nient'altro che le proprietà che gli spettano in quanto oggetto di tipo T -- ossia per uno specifico oggetto a che svolgerà nel proseguire la dimostrazione il ruolo di oggetto generico di tipo T.