Falls eine Formel F gültig ist (sprich: eine Tautologie) so gilt im Sequentialkalkül: "{} |- F" ist ableitbar.
( "|-" steht für den Sequentialpfeil)
Angewendet auf die beiden gegebenen Formeln habe ich folgendes Ergebnis erhalten:
a) nicht gültig (Ableitungsversuch misslingt, man kommt zu Anti-Axiomen)
b) gültig (Ableitung gelingt und endet in lauter Axiomen)