Изменения

Естественный язык, как минимум, содержит в себе логику и математику, которые должны были бы быть включены в подобное формализуемое подмножество просто потому, что и логика и математика непосредственно применяются людьми в [[Социальная деятельность|социальной]], в том числе в [[Хозяйственная деятельность|хозяйственной деятельности]].

Естественный язык, как минимум, содержит в себе логику и математику, которые должны были бы быть включены в подобное формализуемое подмножество просто потому, что и логика и математика непосредственно применяются людьми в [[Социальная деятельность|социальной]], в том числе в [[Хозяйственная деятельность|хозяйственной деятельности]].

[[Логицизм]], то есть научная программа о сведе́нии математики к логике высказывалась [[Лейбниц, Готфрид, Вильгельм|Лейбницем]] в конце 17 в. Практическое осуществление логицистического тезиса было предпринято в конце 19 — начале 20 вв. в работах [[Фреге, Фридрих Людвиг Готлоб|Фреге]], и в «[[Principia mathematica]]» за авторством [[Уайтхед, Альфред Норт|Уайтхеда]] и [[Рассел, Бертран Артур Уильям|Рассела]]<ref name="fdict">{{статья|заглавие=Логицизм|издание=Философия: Энциклопедический словарь|издательство=М.: Гардарики. Под редакцией А. А. Ивина.|год=2004}}</ref>. В 1931 году [[Гёдель, Курт|Гёдель]] показал, что никакая формализованная система логики не может быть адекватной [[Основания математики|базой математики]]<ref name="fdict" />. Дальнейшее развития этого направления науки привели к появлению [[Теория типов|теории типов]], первоначальной основанной на упомянутой работе Уайтхеда и  Рассела и дальнейшего многообразия формальных теорий, вплоть до новомодной [[HoTT]]. Ни одна из них не может считаться убедительной основной для [[Юриспруденция|юриспруденции]], '''''даже если бы''''' они были пригодны для описания естественных жизненных ситуаций. Просто потому, что трансляция любого описания, данного на языке подобных теорий в понятные для обывателя термины является задачей нереализуемой сложности. Любые претензии к современному законодательству о его двусмысленности и непрозрачности при переходе на [[Формализм|формализмы]] подобного уровня сложности следовало бы отвергнуть - так как получилось бы, что строгое законодательное описание требований закона, созданное при помощи подобного формального подмножества языка может оказать потенциально непонятным для обывателя, либо содержать в себе логически дыры и прорехи, доступные только избранным специалистам. В этом месте мы приходим к тому, что предложение о смене неформального, естественного языка написания законов на формализованный специализированный его диалект равнозначно смене одного корпуса специалистов по трактовке этих законов (юристов) на другой (программистов-математиков). Аргумент о том, что после такой смены можно будет хотя бы выверять [[Юридическая позиция|юридические позиции]] сторон в спорах при помощи специально написанной программы, как мы видим, не выдерживает никакой критики - с активным применением той же теории типов сейчас построены многие языки программирования. Но никто не слышал о том, чтобы программисты программировали без ошибок. После этого можно было бы сделать вывод, что предложение выгнать юристов, которые 'мутят' сводится к замене их программистами, которые 'мутят' ничуть не меньше.

[[Логицизм]], то есть научная программа о сведе́нии математики к логике был выдвинут [[Лейбниц, Готфрид, Вильгельм|Лейбницем]] в конце 17 в.  

 

Практическое осуществление логицистического тезиса было предпринято в конце 19 — начале 20 вв. в работах [[Фреге, Фридрих Людвиг Готлоб|Фреге]], и в «[[Principia mathematica]]» за авторством [[Уайтхед, Альфред Норт|Уайтхеда]] и [[Рассел, Бертран Артур Уильям|Рассела]]<ref name="fdict">{{статья|заглавие=Логицизм|издание=Философия: Энциклопедический словарь|издательство=М.: Гардарики. Под редакцией А. А. Ивина.|год=2004}}</ref>.  

 

В 1931 году [[Гёдель, Курт|Гёдель]] показал, что никакая формализованная система логики не может быть адекватной [[Основания математики|базой математики]]<ref name="fdict" />.  

 

Дальнейшее развития этого направления науки привели к появлению [[Теория типов|теории типов]], первоначальной основанной на упомянутой работе Уайтхеда и  Рассела и дальнейшего многообразия формальных теорий, вплоть до новомодной [[HoTT]]. Ни одна из них не может считаться убедительной основной для [[Юриспруденция|юриспруденции]], '''''даже если бы''''' они были пригодны для описания естественных жизненных ситуаций. Просто потому, что трансляция любого описания, данного на языке подобных теорий в понятные для обывателя термины является задачей нереализуемой сложности.  

 

Любые претензии к современному законодательству о его двусмысленности и непрозрачности при переходе на [[Формализм|формализмы]] подобного уровня сложности следовало бы отвергнуть - так как получилось бы, что строгое законодательное описание требований закона, созданное при помощи подобного формального подмножества языка может оказать потенциально непонятным для обывателя, либо содержать в себе логически дыры и прорехи, доступные только избранным специалистам.  

 

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

 

Аргумент о том, что после такой смены можно будет хотя бы выверять [[Юридическая позиция|юридические позиции]] сторон в спорах при помощи специально написанной программы, как мы видим, не выдерживает никакой критики - с активным применением той же теории типов сейчас построены многие [[Язык программирования|языки программирования]]. Но никто не слышал о том, чтобы программисты программировали без ошибок. После этого можно было бы сделать вывод, что предложение выгнать юристов, которые 'мутят' сводится к замене их программистами, которые 'мутят' ничуть не меньше.

=== Формализация истины ===

=== Формализация истины ===