Преподавание математики как языка

Написано по просьбе babybitch_

В середине 1930-х годов Черчем и Тьюрингом было высказано фундаментальное утверждение. Неформально говоря, согласно этому утверждению, все строго описываемые функции являются рекурсивными. Это означает, что любая функция, которую можно точно вычислять или для которой можно изготовить устройство, которое будет ее вычислять, может быть всегда описана внутри любого языка, который обладает так называемой Тьюринг-полнотой. Таковыми являются многие языки программирования, а также бестиповое экстенсиональное лямбда-исчисление, которое, в принципе, тоже может рассматриваться как язык программирования.

С другой стороны, в 1930 году была доказана теорема Геделя о неполноте любой непротиворечивой теории, которая включает арифметику, то есть такая теория всегда содержит некоторое утверждение, которое нельзя доказать внутри нее. Иначе говоря, если теория полна, то она неизбежно противоречива, и в ней можно доказать любое утверждение, включая заведомо неверные. В связи с этим, уместен вопрос о максимальной непротиворечивой теории, которая бы позволяла записывать логические утверждения, содержащие общность, существования, переменные, функции и их свойства. Более формально, такия система называется логикой первого порядка, или, что то же самое, логикой предикатов.

Оказывается, максимальным непротиворечивым теориям соответствуют полные по Гильберту-Посту теории, утверждениями которых являются равенства. Такие теории называются эквациональными (от английского "равенство") и сами по себе свободны от логики, но с их помощью, тем не менее, можно описывать утверждения логики первого порядка. Полнота по Гильберту-Посту, в свою очередь, говорит о том, что любое верное утверждение доказуемо, а любое неверное утверждение делает систему противоречивой. Это свойство, естественно, слабее полноты теории в общем смысле, о котором идет речь в упомянутой теореме Геделя: ложность неверных утверждений в общем случае невозможно доказать.

Таким образом, чтобы найти наиболее мощную непротиворечивую теорию, в рамках которой можно было бы описывать любые строго определяемые математические конструкции, требуется удовлетворить одновременно полноте по Тьюрингу и полноте по Гильберту-Посту. Оба свойства есть у упомянутого в самом начале бестипового экстенсионального лямбда-исчисления. Это по сути простой язык, в котором есть три элементарных сущности: переменная, абстракция и аппликация, - два правила упрощения выражений, а также опреденный порядок выбора частей выражения для достижения наиболее простой формы.

Известно, что когда дети учатся говорить, они строят в своей голове заново учебник, описывая грамматику языка. Это означает, что люди генетически приспособлены к изучению грамматики. При преподавании математики в школе, однако, эта способность мало используется: часто имеют место неформальные определения и "объяснение на пальцах". В противоположность такому подходу, для некоторых детей, изучающих математику, возможно, было бы более естественно изучить сначала новый язык описания, и уже на этом языке увидеть определяемые математические конструкции. Ввиду простоты, на роль такого языка годится бестиповое экстенсиональное лямбда-исчисление.