AndreUT писал(а):
В разных книгах про теорему пишут по-разному: в одних, что существует непротиворечивое и недоказуемое утверждение, а в других, что истинных недоказуемых утверждений несчетное (неперечислимое - насколько я понимаю, это одно и то же) число. Как связаны эти две формулировки? Недоказуемые и непротиворечивые и являются этими истинными недоказуемыми?
Тут Вы много разного понаписывали. Отвечаю по пунктам.
Истинность вообще связана с доказуемостью лишь косвенно, поскольку, как правило, для формальных систем говорят о выводимости теорем (утверждений) из аксиом, и, вроде, обычно, так же в них понимают и доказуемость. Истинность же утверждения это уже выполнимость его в
модели формальной системы.
Вопрос о несчетности числа истинных недоказуемых утверждений тоже несколько уводит в сторону от сути Теоремы Гёделя. Дело в том, что счетные множества это либо конечные, либо равномощные множеству натуральных чисел, и, обычно, множеству вообще всех утверждений, допустимых в формальной системе (с конечным алфавитом). Поэтому, видимо, построив в формальной системе одно недоказуемое и неопровержимое утверждение, его можно добавить как аксиому, затем в этой новой формальной системе построить еще одно недоказуемое и неопровержимое утверждение, добавить его как аксиому, и т.д. Таким образом, получая в результате бесконечное (но счетное) количество утверждений, недоказуемых и неопровержимых в исходной формальной системе.
Далее, я, как и nikvic, думаю, что перечислимость обычно вообще является не числом, а свойством множества, и разговор о ней опять уведет нас в сторону оффтопика о рекурсивных функциях, алгоритмах, программах для машины Тьюринга и т.д.
И, наконец, у теоремы Гёделя много аналогов.
AndreUT писал(а):
Насколько я понял, первая теорема Геделя говорит о том, что в любой формальной системе существует утверждение, которое является непротиворечивым и недоказуемым одновременно.
Не в любой, а в достаточно сильной. Например, для каждого непротиворечивого рекурсивно аксиоматизируемого расширения формальной арифметики
существует предложение, неразрешимое в нем (т.е. замкнутая формула, невыводимая и неопровержимая) (см. Следствие 3.34 из книги Мендельсона). Но, например, вроде исчисление предикатов первого порядка полно, т.е. в нем любое утверждение или доказуемо, или опровержимо (т.е. из аксиом выводимо либо оно, либо его отрицание).
AndreUT писал(а):
аксиомы - это как раз те вещи, которые мы принимаем без доказательств
Это как посмотреть. Вроде, любое недоказуемое в формальной системе утверждение можно принять в ней как новую аксиому, что не повлияет на непротиворечивость этой системы. Проблемы могут возникать, если сделать наоборот – не принимать новое утверждениеа попробовать доказать, выведя из уже имеющихся в этой системе аксиом. Кроме того, принятие утверждений без доказательств из-за их «самоочевидности» касается уже не только формальных систем, а и их (семантических) интерпретаций. И, кстати
«Геометрия Евклида, по-видимому, была предложена как космологическая теория (см. Popper, 1952, стр. 147—148). И ее «постулаты» и «аксиомы» (или «общие понятия») были предложены как смелые, вызывающие предложения, направленные против Парменида и Зенона, учения которых влекли за собой не только ложность, но даже логическую ложность, непредставимость этих «постулатов». Только позже «постулаты» были приняты как несомненно истинные, и смелые антипарменидовские «аксиомы» (вроде «целое больше части») были сочтены настолько тривиальными, что были опущены в позднейших анализах доказательства и превращены в «скрытые леммы». Этот процесс начался с Аристотеля; он заклеймил Зенона как любящего спорить чудака, и его аргументы как «софистику». Эта история была недавно рассказана с интересными подробностями Арпадом Сабо (1960, стр. 65—84). Сa6o показал, что в эпоху Евклида слово «аксиома», как и «постулат», обозначало предположение в критическом диалоге (диалектическом), выставленное для того, чтобы проверить следствия, причем партнер по дискуссии не обязан был принимать его как истину. По иронии истории его значение оказалось перевернутым. Вершина авторитета Евклида была достигнута в век просвещения. Клеро побуждал своих товарищей не «затемнять доказательств и раздражать читателей», выставляя очевидные истины: Евклид делал это лишь для того, чтобы убедить «упорствующих софистов» (1741, стр. X и XI)».
Имре Лакатос «Доказательства и опровержения. Как доказываются теоремы». arseniiv писал(а):
Разумеется, аксиомы вообще к теореме Гёделя не имеют отношения, и Stan Slapenarski написал ерунду. Она говорит о формуле, не выводимой вместе со своим отрицанием, тогда как аксиома данной теории в ней выводима, а отрицание аксиомы выводимо только в противоречивой теории.
Имелась ввиду, конечно, невыводимость Аксиомы параллельных в Абсолютной геометрии, как «самый» яркий и известный геометрический пример.
AndreUT писал(а):
Ну это понятно,
И как показывает история математики, проблема доказательства Аксиомы Параллельных в Абсолютной геометрии и ее решение (заключающее о невозможности данного доказательства) отнюдь не тривиальны (см.
ту же статью из Википедии или
мое краткое резюме).
arseniiv писал(а):
Евклидова геометрия же полна и непротиворечива,
Nemiroff писал(а):
Евклидова геометрия разрешима.
Ух ты.
Т.е. в ней нельзя, например, сформулировать континуум-гипотезу для подмножеств действительной прямой и аналитическая геометрия сильнее евклидовой?
офигенное рассуждение. Ошибку сами сможете найти?
Про Евклидову геометрию, под которой здесь, понимают видимо, какую-нибудь гильбертовскую формальную систему, и говорят о ее непротиворечивости, полноте и разрешимости, Вам, наверное, расскажут другие, а о проблеме полноты формальной арифметики я писал в последнем абзаце 
включает в себя неполную формальную арифметику 