catpad

Category:

Baba is Gödel

gromozeka порекомендовал отличную игрушку — «Baba Is You».
Это такие головоломки, где надо ходить, толкать разные штуки и дотрагиваться до чего-то, чтобы победить — вроде бы уже сто раз виденное. Но тут есть одно интереснейшее отличие: правила игры можно менять по ходу дела, а главное — сами эти правила являются элементами игры!
Например, если на экране написано «Flag Is Win», то выиграть можно, дотронувшись до флага. Но саму надпись Flag можно вытолкнуть и вместо неё поставить, например, Crab — и теперь уже выиграть можно, дотронувшись до краба. Ещё интересней: в начале каждого уровня «Baba Is You», то есть игра идёт от лица этой самой Baba. Но если вытолкнуть бабу из надписи и подставить Lake, то играть после этого можно будет целым озером (оно всё целиком будет двигаться вместо Baba). При этом, если вовремя не подставить что-то на место Бабы, то уровень сразу проигран, потому что главное действующее лицо исчезает.
Постепенно появляются всякие новые операторы вроде And, Has и т.п. Невероятно классно придумано!

Поиграл я немного в Бабу и тут до меня дошло: это же прямое воплощение доказательства теоремы Гёделя!
Как известно, доказательство Гёделя построено на том, что язык мета-математики (т.е. высказывания о формулах формальной арифметики) переведён на язык самой арифметики. Таким образом, рассужать о формальной системе можно не со стороны (то есть, не на мета-языке), а прямо внутри самой системы, то есть на языке математики.
Здесь происходит ровно то же самое: правила игры (то есть, мета-высказывания об игре) сами становятся частью игры (системы). Ими можно манипулировать не выходя за пределы игры, то есть без того, чтобы «исправлять книгу правил».
Можно продолжить аналогию ещё немного. Гёдель в конце концов подставляет в теорему, которая говорит о своей недоказуемости, её собственный гёделевский номер. В терминах Бабы, это, наверное, можно было бы сделать с помощью подстановки в правило выигрыша «...Is Win» самого героя игры, т.е. «Baba Is Win» с немедленным выигрышем. Но сделать это невозможно, потому что как только Baba будет вытолкнуто из правила «Baba is You», «Baba Is Win» перестаёт быть условием победы, так как игрок больше не называется Бабой. (С другой стороны «Baba is You and Win» должно стработать, но это надо будет попробовать).


Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.