Wiem, że po tej deklaracji nie mam wyjścia i muszę wytłumaczyć, o co chodzi.

Zajmuję się logiką. Logika dla matematyków to trochę jak gramatyka historyczna dla polonistów: nauka o języku, którym się posługują. Język ten jest złożony z formuł, będących napisami, które z kolei wyrażają własności struktur matematycznych, na przykład podzbiorów prostej (których jest nieskończenie wiele) albo algebry wartości logicznych prawda i fałsz, która jest skończona.

Jednym z najważniejszych w logice jest twierdzenie o pełności dla logiki pierwszego rzędu, które udowodnił jako pierwszy Kurt Gödel.

Orzeka ono, że każdą własność struktur matematycznych, którą da się wyrazić w logice pierwszego rzędu i która przysługuje wszystkim bez wyjątku strukturom, można także udowodnić, posługując się formalnym systemem dowodowym. Własności przysługujące wszystkim strukturom nazywa się tautologiami i można o nich myśleć jako o fundamentalnych prawach matematycznego świata, sformułowanych za pomocą sztywnego, skodyfikowanego języka logiki. Z kolei system dowodowy opiera się na ściśle określonych manipulacjach na napisach, którymi są formuły logiki, w oderwaniu od wszelkich intuicji czy odwołań do świata struktur. Formułę, dla której znajdzie się dowód w tym systemie, nazywa się twierdzeniem.

Twierdzenie o pełności mówi, że zbiory tautologii i twierdzeń są identyczne: jak coś jest prawdziwe w każdej strukturze, to ma także formalny dowód, a jak ma dowód, to jest prawdziwe we wszystkich strukturach.

Nieformalnie, matematyk ścisły formalista (tak sobie wyobrażam użytkowników systemu dowodowego) i matematyk odwołujący się do rozumienia i znaczenia formuł (powiedzmy o nim, że to matematyk platonista) tworzą i badają tę samą matematykę.

Kluczowe dla twierdzenia o pełności jest to, że dopuszczone są w nim także struktury nieskończone jako obiekty, których własności wyraża logika. Z twierdzenia Trachtenbrota wynika, że dla zbioru formuł prawdziwych we wszystkich strukturach skończonych (ale niekoniecznie prawdziwych w strukturach nieskończonych) nie dałoby się stworzyć stosownego systemu dowodowego. W świecie bez struktur nieskończonych drogi matematyka-formalisty i matematyka-platonisty by się rozeszły.