forall xの著者は有効性の定義をこのように述べています（8ページ）：
An argument is valid if and only if it is impossible for all of the premises to be true and the conclusion false.
また、これを「形式による妥当性」（21ページ）と呼ぶ：
今考えた議論の妥当性は、「ジェニーは悲惨だ」「ディパンはトルストイの熱心な読者だ」「ジムはたくさんの演劇に出演した」といった英語の表現の意味とはあまり関係ない。 もし意味と関係があるとすれば、それは「and」「or」「not」「if…、then…」といったフレーズの意味である。
こうした妥当性は、証明チェッカーを使って自動的に検証することができる。 証明チェッカーに入力した論証が通れば、証明チェッカーが貧弱でないと仮定すれば、それは形式の徳で妥当である。
“It is raining. “という文を考えてみること。 この文の否定は “It is not the case that it is raining” と書くことができる。 It is raining “を “P “で記号化しよう。 すると、その否定は”¬P “となる。 この二つから作られる自己矛盾文は、「P∧¬P」、つまり「P」と「¬P」の両方となる。
これを前提にして、in virtue of formの有効な論証を構成することができるでしょうか。 はい、できます。 3639>
1行目が前提です。 2行目は、接続詞(∧E)のどちら側を使っても良いという接続詞消去ルール(∧E)を使って論証して得ますね。 私が使ったもの、「P」は私が示したかったものであることが判明したので、プルーフチェッカーは私が目的を達したことを確認しました。
自己矛盾する前提が与えられたとき、自己矛盾する前提の接続詞の1つが続くことを示す有効な議論を構築できたことは奇妙に見えるかもしれません。 さらに奇妙なことがあります。
もう少し頑張れば、自己矛盾の前提からどんなものでも導かれることを示すことができます。 Q “を “何々 “の記号とする。 この例は、私が「Q」に対して有効なin virtue of form argumentを構築できることを示している：
最初の行は、前の例と同様に自己矛盾の前提を含んでいた。
2行目と3行目では、前提（1行目）の両側に接続詞消去（∧E）を使って、これらを別の行に配置しました。
一旦別々の行にしたら、4行目で矛盾導入のルール（⊥I）を使って、矛盾がある（⊥）と記すことができる。
5行目で、矛盾があるので、何でも好きなことを書くことができる。 それを爆発（X）の法則といいます。 私の目標は「Q」であり、規則に従って私は何でも書くことができるので、「Q」と書いています。 証明チェッカーは、私がゴールに到達したことを確認します。
これらのルールの詳細については、第15章「TFLの基本ルール」の forall x.
を参照してください。