В книге предлагается  увлекательное введение в символическую логику.  Дана унифицированная трактовка трех «возможных миров»: эпистемического мира человеческих убеждений в истинности высказываний; мира машин, способных воспроизводить истинные высказывания (печатать предложения, выражающие эти высказывания), и мира математических систем, в которых можно доказывать высказывания. Предложено    нестандартное изложение знаменитых теорем Гёделя о неполноте формальных систем и теоремы Лёба и  увлекательный анализ взаимоотношения между понятиями «непротиворечивость», «доказуемость» и «разрешимость».