Выводимость можно описать как отношение формальной арифметики, и если формальная система Т может выражать отношения формальной арифметики, то она может выражать и выводимость. Да, отношение «высказывание S выводимо в T» посложнее, чем a+b=c, но принципиальной разницы между ними нет.
Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
Для понимания теоремы Гёделя очень советую прочесть книгу Д. Хофштадтера «Гёдель, Эшер, Бах — эта бесконечная гирлянда», там идея «странной петли», которая используется в доказательстве, пояснена на множестве простых примеров. Очень грубо и упрощенно теорему Гёделя о неполноте можно интерпретировать так: любой язык, достаточно мощный для того, чтобы быть собственным метаязыком (формальная арифметика — это язык именно такой мощности) либо не полон (содержит недоказуемые, т.е. не выводимые за конечное число шагов с помощью конечного числа правил вывода из конечного числа аксиом, истинные утверждения) либо противоречив (содержит доказательство как какой-либо гипотезы А, так и её отрицания not A).
Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
Можно редактировать некоторые настройки AMI Aptio4 UEFI (на нем сейчас почти все современные десктопные платы) с помощью утилиты AMIBCP 4. Жаль только, что далеко не все.
Автору темы респект, отличный проект.
Я тоже сейчас неспеша занимаюсь темой патча UEFI: пишу поддержку новых БИОСов для плат на Z87 в PMPatch (это патчер для снятия защиты от записи с регистра 0xE2, которая не дает загружаться драйверу CPUPM из OS X).
Смотря в каком сегменте.
Если в обыкновенный ПК для дома — все перечисленные вполне конкуренты. Я не помню ни одного производителя плат на Z77, у которого был бы один шлак. Даже у ECS в тот раз получилось сделать что-то приличное.
Если брать оверклокеров, то Gigabyte, Asrock, MSI.
Если брать пользователей компактных систем, то Gigabyte, Asrock, MSI, Zotac.
А так при прочих равных для дома можно смело брать первую попавшуюся плату, разницу именно в надежности сейчас уже трудно заметить.
Регулярно получаю и оправляю посылки при помощи «постомата» Packstation. Покупаешь через интернет марку, заполняя при покупке адрес получателя, таможенные формуляры, если посылка должна проходить таможню, вес и размер посылки. Оплачиваешь марку через PayPal, печатаешь саму марку со штрихкодом и таможенные формы (если нужны), наклеиваешь все это на коробку. Подходишь к автомату, он сканирует штрих-код и предлагает открыть ящик 4 размеров на выбор. Кладешь посылку, закрываешь ящик, получаешь от автомата чек с номером для отслеживания, датой и временем принятия. Всё.
Получение тоже очень простое, тебе приходит СМС с кодом, приходишь к автомату, вводишь код и получаешь свою посылку. Такая система позволяет указать в качестве адреса получателя ближайший к тебе постомат, если паранойя не позволяет указать свой.
Если такую систему введут в России повсеместно — будет отлично, и не нужно ничего выдумывать дополнительно.
Сами ребята из BMW говорят, что технологии вроде Driver Assist или Drive-By-Wire с одной стороны улучшают автомобили и удешевляют их производство, но с другой лишают водителя кайфа от непосредственного управления. Причем люди, готовые за этот кайф платить, и являются основными покупателями дорогих и быстрых машин, поэтому практически все системы помощи водителю в них пока еще можно отключить.
Основным препятствием к производству полностью автоматических автомобилей является не инертность и недовольство водителей, а дороговизна соответствующей инфраструктуры, ведь автомобили должны общаться не только между собой, но и с электроникой внутри дорожного покрытия, станциями слежения за дорожной ситуацией и т.п. А на это все нужны деньги, которых не то, чтобы нет, но тратить их никто особенно не торопится.
Сейчас же основной вектор работ в области автоматизации вождения — стандартизация взаимодействия между разными авто и программными комплексами внутри каждого авто. В том числе и поэтому BMW отказываются от FlexRay в пользу RT Ethernet и от своих собственных наработок в пользу наработок проекта AUTOSAR.
Жаль только, что это все стремительно устаревает.
Некоторые из любителей новых технологий уже избавились от поддержки BIOS и загрузки через MBR полностью, и такой загрузчик у них работать уже не будет. Так что уже сейчас можно считать загрузку через MBR глубоким legacy.
Будущее — за UEFI. А там и загрузчик пишется в разы проще, и на ассемблере программировать уже не нужно, хоть и можно. Кому интересно почитать код и посмотреть на то, как нынче устроена загрузка — документация и исходные коды проекта TianoCore к вашим услугам.
И, судя по некоторым разговорам в кулуарах, в следующем году стендов производителей железа будет еще меньше, а те из них, кто останется, будут присутствовать только в бизнес-части, куда обычному посетителю выставки вход закрыт.
Уже сейчас стенды с китайскими USB-хабами и зарядниками занимают добрую половину павильона, а стендов Asus и Gigabyte нет вообще.
Да и людей, с которыми там хочется встретиться, приезжает все меньше и меньше с каждым годом. На Cebit 2012 было почти 40 оверклокеров и причастных к оверклокингу человек со всего мира, а на этой оверклокерское шоу устраивали только на стенде Asrock, и приехали хорошо если человек десять.
В общем, если так пойдет и дальше, то в следующем году вместо Cebit'а я поеду на Computex.
Смешно еще и то, что слова «сайт» и «онлайн» на кириллических языках для малознакомых с существующим интернетом людей звучат как очередной «абырвалг».
Как уже не раз говорилось, сама идея доменов на национальных языках — порочна. А новые «кириллические» домены со словами английского языка — это вообще ни в какие ворота уже.
Попробую достать на тест вышеупомянутый ZBOX на H61 и поставить на него OS X. Придется, возможно, сменить WLAN-карту, но даже так получится дешевый аналог Mac Mini в полностью собранном виде.
CM Seidon 120M уже удалось достать (спасибо Саше Крону), читайте ее обзор на OCClub.ru в самое ближайшее время.
Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
Автору темы респект, отличный проект.
Я тоже сейчас неспеша занимаюсь темой патча UEFI: пишу поддержку новых БИОСов для плат на Z87 в PMPatch (это патчер для снятия защиты от записи с регистра 0xE2, которая не дает загружаться драйверу CPUPM из OS X).
Если в обыкновенный ПК для дома — все перечисленные вполне конкуренты. Я не помню ни одного производителя плат на Z77, у которого был бы один шлак. Даже у ECS в тот раз получилось сделать что-то приличное.
Если брать оверклокеров, то Gigabyte, Asrock, MSI.
Если брать пользователей компактных систем, то Gigabyte, Asrock, MSI, Zotac.
А так при прочих равных для дома можно смело брать первую попавшуюся плату, разницу именно в надежности сейчас уже трудно заметить.
Спасибо за отчет, Дим.
Только слово «пропиетраных» поправь, уж больно страшное оно.
Получение тоже очень простое, тебе приходит СМС с кодом, приходишь к автомату, вводишь код и получаешь свою посылку. Такая система позволяет указать в качестве адреса получателя ближайший к тебе постомат, если паранойя не позволяет указать свой.
Если такую систему введут в России повсеместно — будет отлично, и не нужно ничего выдумывать дополнительно.
Основным препятствием к производству полностью автоматических автомобилей является не инертность и недовольство водителей, а дороговизна соответствующей инфраструктуры, ведь автомобили должны общаться не только между собой, но и с электроникой внутри дорожного покрытия, станциями слежения за дорожной ситуацией и т.п. А на это все нужны деньги, которых не то, чтобы нет, но тратить их никто особенно не торопится.
Сейчас же основной вектор работ в области автоматизации вождения — стандартизация взаимодействия между разными авто и программными комплексами внутри каждого авто. В том числе и поэтому BMW отказываются от FlexRay в пользу RT Ethernet и от своих собственных наработок в пользу наработок проекта AUTOSAR.
Некоторые из любителей новых технологий уже избавились от поддержки BIOS и загрузки через MBR полностью, и такой загрузчик у них работать уже не будет. Так что уже сейчас можно считать загрузку через MBR глубоким legacy.
Будущее — за UEFI. А там и загрузчик пишется в разы проще, и на ассемблере программировать уже не нужно, хоть и можно. Кому интересно почитать код и посмотреть на то, как нынче устроена загрузка — документация и исходные коды проекта TianoCore к вашим услугам.
Уже сейчас стенды с китайскими USB-хабами и зарядниками занимают добрую половину павильона, а стендов Asus и Gigabyte нет вообще.
Да и людей, с которыми там хочется встретиться, приезжает все меньше и меньше с каждым годом. На Cebit 2012 было почти 40 оверклокеров и причастных к оверклокингу человек со всего мира, а на этой оверклокерское шоу устраивали только на стенде Asrock, и приехали хорошо если человек десять.
В общем, если так пойдет и дальше, то в следующем году вместо Cebit'а я поеду на Computex.
Как уже не раз говорилось, сама идея доменов на национальных языках — порочна. А новые «кириллические» домены со словами английского языка — это вообще ни в какие ворота уже.
CM Seidon 120M уже удалось достать (спасибо Саше Крону), читайте ее обзор на OCClub.ru в самое ближайшее время.