# Model checking for logical consequence in propositional logic

Let us consider the following algorithm concerning propositional logic and entailment, taken from the book Artificial Intelligence A modern approach.

A truth-table enumeration algorithm for deciding propositional entailment. TT stands for truth table. PL-TRUE? returns true if a sentence holds within a model. The variable model represents a partial model- assignment to only some of the variables. The function call EXTEND(P, true, model) returns a new partial model in which P has the value true.

function  TT-ENTAILS? (KB,α) returns  true  or  false
inputs: KB, the knowledge base, a sentence in propositional logic
α, the query, a sentence in propositional logic

symbols <--- a list of the propositional symbols in KB and α
return TT-CHECK-ALL(KB,α,symbols,[])
function TT-CHECK-ALL(KB,α,symbols,model ) returns true or false
if EMPTY?(symbols) then
if PL-TRUE?(KB, model) then return PL-TRUE?(α,model)
else return true
else do
P <---FIRST(symbols); rest <--- REST(symbols)
return TT-CHECK-ALL(KB,α,rest,EXTEND(P,true,model) and
TT-CHECK-ALL(KB, α, rest, EXTEND(P,false,model)


I realized that the algorithm returns TRUE when the KB is false, regardless the truth value of α.

Is this correct because anything is logical consequence of FALSE? If this is not the case, how can I justify the behavior of this algorithm?

By definition of logical consequence, a statement ($\alpha$ in this case) follows from a bunch of other statements ($KB$ in this case) if and only if it is impossible for $\alpha$ to be false while all of the statements in $KB$ are true.
So, if $KB = FALSE$, then it is impossible for all statements in $KB$ to be all true, and hence it is also impossible for $\alpha$ to be false while all of the statements in $KB$ are true.
And so yes, whatever $\alpha$ is, it will be a consequence.