# How to check if compound proposition is contradiction (is always false)?

I know how to check compound proposition if it is tautology with TautologyQ[]. But I have not found any function that can check if the compound proposition is contradiction (is always false). Is there any similar way (like with tautology, without generating truth tables) to check if a compound proposition is a contradiction or not?

For example, how can I check if compound proposition p && !p is a contradiction or not?

So to find out if the proposition is a contradiction we can negate the proposition and after check the result if it is the tautology. If the output is True it means that the proposition is contradiction because as we mentioned above the negation of a contradiction is a tautology. If the output is False, that means that the proposition is not contradiction and it can be tautology or contingency.

For example, if we want to check if p && ! p is a contradiction (which it is) we use code:

TautologyQ[Not[p && ! p], {p}]


Output:

True

• Does this checks "if the proposition is a contradiction" or it checks "if the proposition is not a tautology"? Aug 22, 2018 at 18:05
• It checks that the converse of the propositions is a tautology. In my understanding, that means that the proposition is contradiction. Aug 22, 2018 at 18:07
• I think you are right: proofwiki.org/wiki/Contradiction_is_Negation_of_Tautology Aug 22, 2018 at 18:24
• If f is a boolean-valued function, then f(x1, x2, ..., xn) is true for all possible values of the arguments if and only if ¬f(x1, x2, ..., xn) is false for all possible values of the arguments. Hence, Henrik's approach is valid. Aug 23, 2018 at 6:16
• I edited the answer and added more clarification and information from comments. Is it ok? Aug 23, 2018 at 13:13
Resolve[Exists[p, p && ! p == True]]


(*

False

*)

You can interpret this result as: "There does not exist any p such that the statement p && !p is True.

Background example:

Resolve[Exists[{p, q}, (p && ! p == True || q == True)]]


(*

True

*)

You can interpret this result to say:

It is true that there exists some p and q such that both p and !p are True OR q is True. The key claus here is the OR. Certainly there exists some q for which q is True.

• In your example, I can substitute p, p && ! p for any other compound proposition to check for a contradiction, right? For example, for a||bThere sould be Resolve[Exists[a, b, a && b == True]] ? Aug 22, 2018 at 16:54
• Also if False it means contradiction and if True it means that it is not a contradiction? Aug 22, 2018 at 16:55
• False in my solution example means there does not exist any p such that p and not p is True. Aug 22, 2018 at 17:01

I also found another way:

"In a complete logic, a formula is contradictory if and only if it is unsatisfiable". Source

In that case, we can check if the proposition is satisfiable and after negate the result. If the output is Truethat means that the original statement was unsatisfiable which also means that it was contradiction. If the output was False it means that the result was satisfiable, which means that it was tautology or contingency.

For example, lets check if p && !p is contradiction:

Not[SatisfiableQ[p && ! p, {p}]]


output:

True

It means that p && !p is contradiction.

Lets check if p || ! p is contradiction:

Not[SatisfiableQ[p || ! p, {p}]]


output:

False

It means that p || ! p is not contradiction. The output does not say that but it is tautology.

Lets check if p && q is contradiction:

Not[SatisfiableQ[p && q, {p, q}]]


output:

False

It means that p && q is not contradiction. The output does not say that but it is contingency.

• That makes sense because of: $\neg (\exists p \colon \text{$A(p)$is true})$ is equivalent to $(\forall p \colon \neg (\text{$A(p)$is true}))$. SatisfiableQ is essentially the $\exists$-quantor. Aug 23, 2018 at 13:57
• @HenrikSchumacher Thank you. Aug 23, 2018 at 13:58