Vedem (vezi Tabelul 1.4), dacă luăm interpretarea lui j. pentru care j (x) = 0, j (y) = 1 (adică luăm al treilea rând al tabelului), atunci j (F1) = j (F2) = j (F3) = 0. În consecință, formula G nu este o consecință logică a formulelor F1, F2, F3.
Conceptul unei consecințe logice este strâns legat de conceptul de satisfacebilitate.
Definiția. Se consideră că setul de formule 1, F2, ..., Fl> este fezabil. dacă există o interpretare j astfel încât j (F1) = j (F2) = ... = j (Fl) = 1.
Valabilitatea setului de formule 1, F2, ..., Fl> poate fi verificată prin construirea unei tabele de adevăr comun pentru aceste formule. Dacă există cel puțin o linie în care F1 se află în coloanele formulelor F1, F2, ..., Fl, atunci acest set de formule este fezabil. Dacă nu există o astfel de linie, atunci multe formule sunt impracticabile. Astfel, setul de formule 1, F2, F3, G> din exemplul anterior este fezabil, deoarece în tabelul 1.4 de pe prima linie există coloane în coloanele acestor formule.
În subiectul 4 avem nevoie de următoarea declarație.
Teorema 1.2 Formula G este o consecință logică a formulelor F1, F2, ..., Fk dacă și numai dacă setul de formule
Dovada. Fie formula G o consecință a setului de formule F1, ..., Fk. Să presupunem, prin contradicție, că mulțimea L este satisfăcătoare. Aceasta înseamnă că există o interpretare a lui y astfel încât y (F1) = ... = y (Fk) = y (Ø G) = 1. Dar dacă y (F1) = ... = y (Fk) = 1, atunci y (G) = 1, deoarece G este o consecință logică a formulelor F1, ..., Fk. Rezultatul contradicției y (t G) = 1 și y (G) = 1 demonstrează că setul de formule 1, ..., Fk. Ø G> nu este fezabil.
Acum, setul de formule L este imposibil de realizat. Luați în considerare o interpretare j astfel încât j (F1) = ... = j (Fk) = 1. Deoarece L nu este fezabil, atunci j (Ø G) = 0. Dacă j (Ø G) = 0, atunci j (G) = 1. Prin urmare, egalitatea j (G) = 1 rezultă din egalitatea j (F1) = ... = j (Fk) = 1. Aceasta înseamnă că G este o consecință logică a setului de formule F1, ..., Fk.
Articole similare
Trimiteți-le prietenilor: