Сделан вывод, что в Теореме Геделя, если формальная система S непротиворечива, то формула A невыводима в S; если система S ω-непротиворечива, то формула ¬A невыводима в S. Таким образом, если система S ω-непротиворечива, то она неполна и A служит примером неразрешимой формулы. В стандартной интерпретации формула A означает "не существует вывода формулы A", то есть утверждает свою собственную невыводимость в S. Следовательно, по теореме Геделя, если только система S непротиворечива, то эта формула и в самом деле невыводима в S и потому истинна в стандартной интерпретации. Таким образом, для натуральных чисел формула A верна, но в S невыводима.

В процессе доказательства теоремы строится такая формула B арифметической формальной системы S, что, если формальная система S непротиворечива, то в ней невыводимы обе формулы B и ¬B; иначе говоря, если система S непротиворечива, то она неполна, и B служит примером неразрешимой формулы. Формулу B иногда называют россеровой неразрешимой формулой. Эта формула немного сложнее геделевой.

В стандартной интерпретации формула B означает "если существует вывод формулы B, то существует вывод формулы ¬B". Согласно же теореме Геделя в форме Россера, если формальная система S непротиворечива, то формула B в ней невыводима; поэтому, если система S непротиворечива, то формула B верна в стандартной интерпретации.