Autorzy forall x podają taką definicję ważności (strona 8):
An argument is valid if and only if it is impossible for all of the premises to be true and the conclusion false.
Odnoszą się do tego również jako do „ważności ze względu na formę” (strona 21):
Ważność rozważanych właśnie argumentów nie ma wiele wspólnego ze znaczeniami angielskich wyrażeń takich jak 'Jenny is miserable’, 'Dipan is an avid reader of Tolstoy’, czy 'Jim acted in lots of plays’. Jeśli w ogóle ma to związek ze znaczeniami, to ze znaczeniami wyrażeń takich jak 'and’, 'or’, 'not’ i 'if…, then…’.
Taką poprawność można automatycznie zweryfikować za pomocą proof checkerów. Zakładając, że proof checker nie jest źle skonstruowany, jeśli argument, który wprowadzamy do proof checkera przechodzi, to jest on ważny na mocy formy.
Rozważmy zdanie: „Pada deszcz”. Zaprzeczenie tego zdania można zapisać jako „Nie jest tak, że pada deszcz”. Symbolizujmy zdanie „Pada deszcz” przez „P”. Wtedy jego negacją będzie „¬P”. Zdanie wewnętrznie sprzeczne zbudowane z tych dwóch zdań miałoby postać „P ∧ ¬P”, czyli zarówno „P”, jak i „¬P”.
Czy używając tego jako przesłanki możemy skonstruować ważny argument na mocy formy? Tak, możemy. Oto przykład, w którym próbuję pokazać, że „P ∧ ¬P” implikuje „P”.
Pierwsza linia jest przesłanką. Drugi wiersz otrzymuję, stosując regułę eliminacji koniunkcji (∧E), która pozwala mi użyć dowolnej strony koniunkcji (∧) w moim argumencie. Okazuje się, że to, czego użyłem, „P”, było tym, co chciałem pokazać, a więc sprawdzacz dowodów zweryfikował, że osiągnąłem swój cel.
Może się wydawać dziwne, że biorąc pod uwagę samozaprzeczalną przesłankę, byłem w stanie skonstruować poprawny argument pokazujący, że jeden ze spójników w samozaprzeczalnej przesłance wynikał z niej. To może stać się jeszcze dziwniejsze.
Przy odrobinie więcej pracy, mogę pokazać, że cokolwiek wynika z samozaprzeczalnej przesłanki. Niech „Q” będzie symbolizacją czegokolwiek. Ten przykład pokazuje, że mogę skonstruować ważny na mocy formy argument dla „Q”:
Pierwszy wiersz zawierał samozaprzeczalną przesłankę jak w poprzednim przykładzie.
W liniach 2 i 3 użyłem eliminacji koniunkcji (∧E) po obu stronach przesłanki (linia 1), aby umieścić je w osobnych liniach.
Gdy już mam je w osobnych liniach, mogę użyć reguły wprowadzania sprzeczności (⊥I), aby zauważyć w linii 4, że mam sprzeczność (⊥).
W linii 5, ponieważ mam sprzeczność, mogę napisać cokolwiek chcę. To się nazywa reguła eksplozji (X). Ponieważ moim celem jest „Q”, a zgodnie z regułami mogę napisać wszystko, co chcę, piszę „Q”. Dowód sprawdza, czy osiągnąłem swój cel.
Więcej szczegółów na temat tych reguł znajdziesz w rozdziale 15 „Podstawowe reguły TFL” w forall x.
.