У меня возник новый вопрос к общественности. ИМХО он подходит для элементарного рассмотрения оснований математики. Итак, внимание вопрос.
Почему наша реальная математическая практика непротиворечива?
Я много задумывался над этим вопросом... По-моему тут ключевая идея в том, что, все реальное конструктивно. ...
Скажу свое слово, хотя меня тут не жалуют. Видимо для математиков типично привлекать бесконечность там, где уже ничего другое не помогает. Складывается нехорошее представление, что философы разбираются в математике гораздо больше, чем математики в философии, но это уже другой разговор. На самом деле надо задавать другой вопрос, или ударение ставить не на первом, а на последнем слове. На самом деле математика представляет собой незначительную и сильно отфильтрованную часть знания о реальности. Почему математики оставляют только непротиворечивую и строгую часть? Потому что приучены реагировать только на нее и только ее они ищут в любом знании, отбрасывая все остальное. Да непротиворечивость достичь тяжело, но гораздо интереснее, что разные математики начиная «фильтровать» одно интуитивное знание приходят в результате к разным строгим формулировкам. Это и разные основания математики и некатегоричность у Левельгейма-Сколема. Получается, что одна и та же реальность предстает перед математиками в принципиально разных обличиях, а именно – в зависимости от того, какую в каждом случае неформальную часть они отбрасывают. Этот процесс не получается формализовать (а значит и до конца понять) и приходится иметь дело с набором непротиворечивых и строгих, но совершенно несовместимыми между собой математических описаний. Картина мира расщепляется на множество не связанных друг с другом осколков.
Думаю, пока математики настаивают на строгости, они будут получать непротиворечивые описания реальности, каких бы усилий это не стоило. Но картина мира будет расщепляться всё больше и больше. Это, видимо, как-то связано с неполнотой. Потому только очень недалекий математик может три раза утверждать, что наше знание реальности строго и непротиворечиво. Чтобы быть полным в знание нужно внести противоречие, если противоречия нет, то знание неполно, а раз так, то простой подсчет показывает – формальная система не отражает бесконечно больше, чем способна выразить.
Главной особенностью К-систем является то, что vek88 явно упустил и не желает признавать – это отсутствие явной связи между причиной и следствием. Эта связь оборвана и не рассматривается вообще ни в каком виде. Т.е. следствие не выводится, а просто сосуществуют вместе как-то где-то уже полученные и возникшие. Да такие системы можно рассмотреть формально, но они в принципе не предназначены что-либо выводить. Зато с их помощью можно одинаково хорошо отразить даже противоречивое знание. Что это нам дает? Вернее, что можно выразить такого, чего нельзя выразить противоречивой формальной системой, которая противоречива в строгом смысле? Неформальную противоречивость мы пока не трогаем. Можно как vek88 - пытаться достигнуть полноты, пожертвовав материальной импликацией и молясь на бесконечность, но мы поступим умнее.
Упрощенно строгость можно понимать, как требование пользоваться только тем, что оговорено, т.е. правила не меняются по ходу рассуждений, никакой новой информации, какой нет в исходных предпосылках, не возникает походу ниоткуда ну и т.п. Тогда пользуясь лишь оговоренными правилами и начиная с предпосылок мы, принимая решения о направлении рассуждений, не должны получит разные результаты решая задачу двумя разными путями. Так возникает непротиворечивость как своего рода намеренное ограничение вольности математиков. Если непротиворечивость нет, то математики устойчиво заблуждаются в том, что можно получить вообще любой результат. Это как-то трудно сочетается с наличием многих оснований математики и должно приводить к противоречивому выводу утверждений одних оснований начав с рассуждений в совершенно иной системе оснований? Зафиксируем в К-системе небольшой кусок непротиворечивого рассуждения и под конец добавим противоречие. Это отличается от противоречивой системы, поскольку в ней любые выводы возможны, а в нашей К-системе – нет, в ней вообще ничего не выводится сверх того, что там уже есть. Отличается К-система и от непротиворечивых рассуждений, так как явно присутствует противоречие. Как же так может быть? Остается предположить, что кроме противоречивых и непротиворечивых формальных систем остается еще очень много чего.
Где же оно тогда находиться? Оно за пределами строгости, исходные предпосылки не заданы изначально. А появляются неожиданно во время рассуждений. Правила меняются. По аналогии с квантовой механикой – измерение меняет изучаемый объект, если мы каждый раз будем менять определение X и правила манипулирования им при каждом упоминании Х, то никакие формальные правила в такой ситуации сформулировать изначально нельзя по определению. Существующая строгость оговаривает все возможные вольности с самого начала и разрешает только такие, что не влияют на конечный результат. Если ж мы изначально примем точку зрения что рассуждения могут меняться радикальным образом и непредсказуемо для математика, то мы придем к свершено другой математике. Кстати, все радикальные изменения несмотря на их непредсказуемость ведь может вносить другой математик по каким-то своим строго оговоренным правилам. В квантовой механике есть еще один нюанс – мы должны ждать внешнего события иначе просто не будем знать каким образом изменился исследуемый объект. Не дождавшись события мы в принципе не способны продолжать рассуждения, а это уже намек на предсказание Канта о существовании таких формальных построений, которые не сводимы только к математике полностью оторванной от реальности, т.е. всяких внешних событий, а еще точнее, от вносимых другим математиком изменений в наши конструкции.
Существующие представления о строгости не дают возможность исследовать объекты, свойства которых меняются в процессе рассуждений. И никаким исчислением Поста запретить существование таких объектов не получится.
, что верно 
", то можно просто записать это число в явной форме (замкнутым термом), поэтому для записи соответствующей аксиомы нам квантор существования не потребуется. Но если аксиома записана с квантором существования, то это сразу наводит на подозрения, что в "реальной практике" мы это число в явном виде записать не сможем. 
натуральных чисел, мы сначала даем определение натурального числа. Рациональные числа мы определяем, опираясь на уже данное определение натуральных чисел - и далее говорим о множестве 
рациональных чисел. Опираясь на множества рациональных чисел, мы определяем действительные числа, например, через дедекиндово сечение на множестве рациональных чисел или через фундаментальную последовательность рациональных чисел. И т.д.