Nel caso della logica proposizionale, il metododelle tabelle di verità, costituisce un procedimento di decisione. Data una qualunque peoposizione, si può stabilire, con un numero finito di passaggi, se essa assume sempre e solo il valore vero, oppure se in qualche caso assume il valore falso. Nel primo caso diciamo che si tratta di una tautologia o legge logica.Siamo quindi in grado di verificare se, una certa espressione è una legge logica o no,ma non possiamo, cosa molto più interessante, generare l'insieme delle leggi logiche, cioè generare un procedimento che ci permetta di dedurre tali leggi da altre assunte come vere. Al fine di risolvere il problema precedente, cioèdi dedurre in una teoria scientifica, in modo corretto, le proposizioni sempre vere, si utilizzano i sistemi formali di deduzione in cui si può dimostrare la validità di un'affermazione senza ricorrere alle tabelle di verità. In un sistema formale di deduzione, partendo da determinate premesse, si deducono certe conclusioni, senza considerae il significato dei termini che in esse compaiono. Vediamo come si procede per costruire in un sistema formale di deduzione:
1. Si introduce un linguaggio preciso e rigoroso.
2. Si scelgono, tra le frasi del linguaggio, alcune proposizioni da porre alla base della teoria, delle quali si accetta la verità per convenzione, senza alcuna dimostrazione. Tali frasi vengono dette assiomi.
3. Si formulano alcune regole dette regole di deduzione o inferenza, in virtù delle quali si deducono le altre proposizioni.
Il numero delle regole dev'essere minimo ed il loro contenuto semplice.
In un primo momento si applicano le regole di deduzione agli assiomi ottenendo nuove proposizioni, dette teoremi, quindi si applicano le solite regole al nuovo insiemedi proposizioni così ottenute e si ottengono altre proposizioni.
Il gioco delle stelle e delle barre.
Consideriamo un gioco che usa quattro simboli: le lettere A e B, le stelle e le barre.
A B ★ /
Questi simboli possono essere combinati in diversi modi, utilizzando un numero arbitrrio di copie di ciascun simbolo. Ad esempio:
A★BA //★★A /A★B/
Sono tutte stringhe costruite con questi simboli. Stabiliamo che alcune delle stringhe possibili siano vincenti e le altre perdenti. Ovviamente, come in qualsiasi gioco devono esserci delle regole, nel nostro caso servono regole che specifichino quali stringhe siano vincenti e quali perdenti. Adotteremo le tre seguenti regole:
1. Il simbolo A da solo è stringa vincente
2. Il simbolo B da solo è stringa vincente
3. Se S1 e S2 sono striscie vincenti allora anche /S1★S2/ è striscia vincente
E' sottointeso che nessun altra stringa, al di fuori di quelle ottenute mediante queste tre regole, è vincente. Per chiarire il significato di queste regole, iniziamo a giocare. In base alle prime due regole la stringa A e la stringa B sono vincenti. Ora che abbiamo due srtinghe vincenti, possiamo applicare la regola tre, assumendo S1="A" e S2="B", otteniamo /A★B/. Applichiamo di nuovo la regola 3, assumendo stavolta S1="B" e S2="A" otteniamo cosi la striscia vincente /B★A/. Abbiamo ora a disposizione quattro stringhe vincenti ed è chiaro che possiamo ottenerne molte altre, continuando ad applicare la regola 3. Ad esempio posto S1="A" e S2="/B★A/", otteniamo la stringa vincente /A★/B★A//. La striga /A★/B★A/ è invece perdente poichè non può essere ottenuta mediante le tre regole viste.
Il gioco delle stelle e delle barre evidenzia le componenti fondamentali del tipo più semplice di sistema formale. Un sistema formale è costituito da tre elementi caratteristici:
1. Un insieme di simboli con cui formare stringhe ed un insieme di regole che specificano che cos'è una stringa ben formata. Nel nostro gioco i simboli sono A B ★ / ogni stringa si considera ben formata, purchè sia costruita da questi simboli.
2. Un elenco di stringhe vincenti, detto insieme degli assiomi. Nel nostro gioco gli assiomi sono definiti da 1. e 2.
3. Un insieme di metodi per costruire nuove stringhe vincenti, detto insieme delle regole di inferenza. Il nostro gioco ha una sola regola di questo tipo: la 3.
Una stringa vincente è una particolare stringa ben formata, costituita da un esemplare di assioma oppure costruita apartire da stringhe vincenti già note, mediante applicazioni delle regole di inferenza. In logica e in matematica le stringhe vincenti sono dette teoremi. Nel nostro gioco /A★B/ è un teorema, è infatti una stringa vincente, in virtù delle regole 1. e 2. e di un'applicazione della regola 3.