すまんが、教えてくれ。

ψ→(a∨b∨c)が恒真式であり、ψが充足可能であるようなψは、
ホーン式ではない。

上記命題は恒真命題でしょうか？

自明に思えますし、可算の範囲で変数の追加によって、
ホーン式にならない事は証明できそうに思いますが、
変数の追加によってホーン式にならないことが
ホーン式ではないことにはならない。

逆数学や形式的検証に関わる分野で、上記は
よく知られていたりしますか?

それとも、物凄く恥ずかしいことを聞いていますか?