Modus ponens, teorema e implicazione logica

[ilbis]

Ho una grande cofnusione su questi tre argomenti: implicazione logica, teorema visto come implicazione e modus ponens.

Faccio un facile esempio. Mi si mostra che una implicazione logica è tipo P piove Q strada è bagnata:
P=>Q che ha anche valori falsi nella 3a colonna della tabella di verità.

Tuttavia a me sembrerebbe più un teorema perché quando è vero che piove sempre è bagnata la stra, quindi con passaggi logicamente validi (partendo da P con vari assiomi che rendono vera =>) dovrei mostrare la tautologia di P=>Q.

Ma quindi oggi piove => strada è bagnata è una implicazione o una tautologia (e quindi teorema)?

Detto ciò prendiamo il "teorema" P=>Q come sempre vero in 3a colonna della solita tavola di verità.
Il modus ponens come funziona? dice che se P vera e P=>Q vera allora è vera Q. Ovviamente è tatuologia perché potrei avere (P e P=>Q) falsa che quindi mi dà (P e P=>Q)=>Q vera.
Però non capisco il senso del modus ponens, mi sembra mi dica la stessa cosa del teorema, se P è vera (oggi piove) allora la strada è certamente bagnata (Q vera), quindi cosa cambia a livello logico dal teorema: se P è vera assicura che Q è vera. Stessa medesima cosa del teorema P=>Q.

Ho grande confusione in testa. Spero in un aiuto.

[Cannelloni]

Una tautologia è una proposizione vera a livello già sintattico, cioè, una proposizione che comunque venga calata in qualsiasi contesto rimarrà sempre vera. Per esempio: se una cosa è vera allora non è falsa. Non ho bisogno di calarla in un contesto per analizzarla, questa proposizione è una tautologia. Scritta in termini di formula logica dovrebbe essere: $A\rightarrow\neg\neg A$ che equivale a $A\rightarrow A$ che ha una tavola di verità in cui il risultato è sempre vero.

Prendiamo invece le tue proposizioni:
$P=$"piove"
$Q=$"la strada è bagnata"

e guardiamo i seguenti enunciati
1) $P\rightarrow Q$
2) $Q\rightarrow P$
3) $P\leftrightarrow Q$

Hai dimostrato tutti e 3 gli enunciati, ma questo non li rende tautologie perché posso assegnare a $P$ e $Q$ valori che rendono falsi quei 3 enunciati. Per cui no, non sono tautologie.

Il modus ponens non c'entra niente con tutto questo. Ma lo puoi utilizzare per dimostrare che è vera $P$ o $Q$. Per esempio se guardi dalla finestra e vedi che piove, poiché hai dimostrato per conto tuo che $P\rightarrow Q$, per modus ponens concludi che è vera $Q$ senza bisogno di guardare la strada.

Ma il modus ponens è una tautologia? Sì, infatti il modus ponens si formula come segue
$(P\wedge(P\rightarrow Q))\rightarrow Q$
Prova a fare la tabella di questa formula e vedi che da sempre vero. Questo ci turba? No. Dopotutto, tutte le implicazioni dimostrative si basano su tautologie sintattiche. Questo non le rende inutili perché sono trasposte sul piano semantico dove la tabella di verità non è più uno strumento valido.

Per farti capire: hai avuto un'intuizione giusta, le implicazioni dimostrative sono ispirate da tautologie del contesto sintattico (dove tutto è semplice e bello) e trasposte in quello semantico (ok, non è ESATTAMENTE così). Questo è anche il motivo per cui ci sono più correnti di pensiero nella logica moderna. Per esempio gli intuizionisti rifiutano il principio del terzo escluso! Qual è la formula?
$A\vee\neg A$ che è sintatticamente una tautologia, ma, secondo loro, non lo è semanticamente