Per definizione sappiamo che R' e' derivabile se
{b}|--D baa
cioe' si esiste una dimostrazione (una sequenza di assiomi, ipotesi, se ce ne sono,
e fbf ottenute a partire da fbf precedenti utilizzando le regole di inferenza)
che abbia come conclusione baa.
Ma baa non e' un'assioma, ne' un'ipotesi (infatti l'unica ipotesi e' b),
ne' puo' essere la conclusione dell'unica regola di inferenza che abbiamo,
poiche' l'unica premessa dovrebbe essere b, cosa impossibile poiche' la premessa
dell'unica regola utilizzabile deve esssere per forza una stringa di a concatenate.
Quindi non puo' esistere una dimostrazione per {b}|--D baa.
Possiamo quindi affermare che nel sistema formale D, R' non e' drivabile.
R' e' invece ammissibile. Per var vedere cio', dobbiamo mostrare, per definizione di
ammissibilita' che
se |--D+R' α allora |--D α
cioe' che se esiste una dimostrazione di un teorema in D+R', di tale teorema
esiste anche una dimostrazione in D.
Nel nostro caso questo e' banalmente vero,
poiche' una dimostrazione di un teorema in D+R' la regola R' non si puo' mai utilizzare
(se fosse utilizzata, vorrebbe dire che la regola e' utilizzata con premessa b,
il che e' impossibile, come abbiamo visto prima).
Questo significa che una dimostrazione di |--D+R' e' automaticamente
anche una dimostrazione di |--D α