If i have a propositional formula consisting of conjunctions, disjunctions and implications and no negations of three literals $A, B, C$, is it possible to get a CNF from that formula which include this clause:
$(\neg A \lor \neg B \lor \neg C)$
How could i prove that? Is it possible to get an example which would prove that its possible? If yes, what is the algorithm to get that example (and example itself)?
If we have $\bot$, then it's possible, simply consider $(A\land B\land C)\to\bot\equiv(\lnot A\lor\lnot B\lor\lnot C)$. Otherwise it's not possible. Let $v$ be the valuation function. Consider $v(A)=v(B)=v(C)=\text{T}$. Let $P_i\in\{A,B,C\}$ and $*\in\{\lor,\land,\to\}$, have $v(P_1*P_2)=\text{T}$. Furthermore for any formula that can be expressed in this setting $v(P_1*\dots*P_n)=\text{T}$. However $v(\lnot A\lor \lnot B\lor\lnot C)=\text{F}$, now suppose CNF of $P_1*\dots*P_n$ say $Cl_1\land\dots\land Cl_m$ include $Cl_m:\equiv\lnot A\lor \lnot B\lor\lnot C$, then $$\text{T}=v(P_1*\dots*P_n)= v(Cl_1\land\dots\land Cl_{m-1}\land(\lnot A\lor \lnot B\lor\lnot C))=\text{F}$$ for some clauses $Cl_1\dots Cl_{m-1}$, this gives a contradiction.