Gli autori di forall x danno questa definizione di validità (pagina 8):
Un argomento è valido se e solo se è impossibile che tutte le premesse siano vere e la conclusione falsa.
Lo chiamano anche “validità in virtù della forma” (pagina 21):
La validità degli argomenti appena considerati non ha molto a che fare con i significati di espressioni inglesi come “Jenny è infelice”, “Dipan è un avido lettore di Tolstoj”, o “Jim ha recitato in molte commedie”. Se ha a che fare con i significati, è con i significati di frasi come ‘e’, ‘o’, ‘non,’ e ‘se…, allora…’.
Tale validità può essere automaticamente convalidata usando proof checker. Supponendo che il proof checker non sia mal costruito, se l’argomento che inseriamo nel proof checker passa, allora è valido in virtù della forma.
Consideriamo la frase: “Sta piovendo”. La negazione di questa frase potrebbe essere scritta come “Non è il caso che piova”. Simboleggiamo “Sta piovendo” con “P”. Allora la sua negazione sarebbe “¬P”. Una frase autocontraddittoria costruita da questi due sarebbe “P ∧ ¬P”, cioè sia “P” che “¬P”.
Utilizzando questo come premessa possiamo costruire un argomento valido in virtù della forma? Sì, possiamo. Ecco un esempio in cui sto cercando di dimostrare che “P ∧ ¬P” implica “P”.
La prima riga è la premessa. Ottengo la seconda riga usando la regola di eliminazione della congiunzione (∧E) che mi permette di usare entrambi i lati della congiunzione (∧) nel mio argomento. Si scopre che ciò che ho usato, “P”, era ciò che volevo mostrare e così il proof checker ha verificato che ho raggiunto il mio obiettivo.
Può sembrare strano che data una premessa autocontraddittoria, sono stato in grado di costruire un argomento valido mostrando che una delle congiunzioni nella premessa autocontraddittoria ha seguito. Può diventare ancora più strano.
Con un po’ più di lavoro, posso dimostrare che da una premessa autocontraddittoria segue qualsiasi cosa. Sia “Q” la simbolizzazione di qualsiasi cosa. Questo esempio mostra che posso costruire un argomento valido in virtù della forma per “Q”:
La prima riga contiene la premessa autocontraddittoria come nell’esempio precedente.
Nelle righe 2 e 3 ho usato l’eliminazione della congiunzione (∧E) ad entrambi i lati della premessa (riga 1) per metterli su righe separate.
Una volta che le ho su righe separate, posso usare la regola dell’introduzione della contraddizione (⊥I) per notare sulla riga 4 che ho una contraddizione (⊥).
Sulla riga 5, poiché ho una contraddizione, posso scrivere qualsiasi cosa io voglia. Questa si chiama la regola dell’esplosione (X). Poiché il mio obiettivo è “Q” e secondo le regole posso scrivere tutto ciò che voglio, scrivo “Q”. Il proof checker verifica che ho raggiunto il mio obiettivo.
Per maggiori dettagli su queste regole, vedi il capitolo 15 “Regole di base per TFL” in forall x.