Теорема Геделя утверждает неполноту теорий определенного класса. Не всех теорий. ЛПП, например, условиям Геделя не удовлетворяет, соответственно, является полной теорией (в частности, в ЛПП выводима формула о непротиворечивости ЛПП).

Точно!!! Как же я сразу не додумался!!!. Собственно, это и есть неполнота, во всей своей красе, вероятно. И, наверное, там 2 аксиома не нужна, достаточно третьей:)

Но у нас в Set нету никаких «_|_, T, => и т.п.».

А кто говорит про Set? Ну и там есть {}, {*}, hom и т.п. оно топос — в учебнике Голдблата всё есть, например.

что значит «противоречива в качестве логики»?

Доказуем абсурд (_|_) или «A и не A».

Что вообще такое «рассматривать теорию в качестве логической системы»?

То что ты цитируешь. Например, FOL это логика, или STLC. С другой стороны, читаем у Барендрегта

Так как теория лямбда-исчисления свободна от логики, непротиворечивость нужно понимать следующим образом.

...

(ii) Пусть T — формальная теория, формулами которой являются равенствами. Тогда говорят, что T непротиворечива (и пишут Con(T)), если в T доказуемо не любое замкнутое равенство. В противном случае говорят, что T противоречива.

/

Как это вообще можно сделать, если «утверждения - это типы», а типов в ULC нет?

Я говорю термы переводить — как это пытались делать изначально. А типов нет, или один, поэтому функторной интерпретации просто нет.

Так как теория лямбда-исчисления свободна от логики, непротиворечивость нужно понимать следующим образом.

И все же эта фраза отдает каким-то душком. Как может быть теория свободна от логики, если любая теория — есть ни то иное, как логические построения. Если от этого абстрагироваться, любой бред можно назвать теорией.

А кто говорит про Set? Ну и там есть {}, {*}, hom и т.п. оно топос

Ну интерпретация же определяется как функтор в Set, в классическом понимании, по крайней мере.

Доказуем абсурд (_|_) или «A и не A».

Я знаю, что значит «противоречива». Что значит «противоречива в качестве логики»? Что вообще значит «в качестве логики»?

То что ты цитируешь.

Что я цитирую?

Например, FOL это логика, или STLC.

Что значит «FOL - это логика»? Или «STLC - это логика»?

Я говорю термы переводить — как это пытались делать изначально.

Никто не пытался их переводить так, как ты говоришь (в «логические утверждения»).

А типов нет, или один, поэтому функторной интерпретации просто нет.

Почему же нет? Есть.

Теория может быть непротиворечива, полна и разрешима (то есть есть алгоритм который за конечное время выяснит является ли любое утверждение теоремой или нет). Это можно доказать внешними средствами теории моделей.

Теория может доказать свою же непротиворечивость (так как Con(T) может быть утверждением, в отличии от полноты и правильности, которые являются модельными характеристиками).

Как-то я не понимаю что тебя удивляет :)

полноты и правильности, которые являются модельными характеристиками

Да ладно?

Что значит «противоречива в качестве логики»? Что вообще значит «в качестве логики»?

То что ты цитируешь :) А теперь сравни с определением противоречивости и непротиворечивости для лямбда-исчисления которое я процитировал из Барендрегта.

Что я цитирую?

Что значит «FOL - это логика»? Или «STLC - это логика»?

Ты цитировал в сообщение на которое я отвечал:

Считаем теорию «логикой» если она годится для построения логических рассуждений, то есть там есть типичные ингредиенты _|_, T, => и т.п. и они взаимопереводимы с этими же утверждениями какой-нибудь тестовой «логики» (по желанию).

В FOL есть формулы _|_, T, => и т.п., в STLC(++) — типы.

Никто не пытался их переводить так, как ты говоришь (в «логические утверждения»).

http://en.wikipedia.org/wiki/Curry's_paradox#Lambda_calculus

Почему же нет?

Если взять категорию ULC на одном (!) рефлексивном объекте и категорию какого-нибудь STLC с {T, F, * -> *, * x *, * | *}, то нужной функторной эквивалентности явно нет.

Теория может быть непротиворечива, полна и разрешима

Чем является утверждение «Если а = b и b = c то b = c»? Это, на мой взгляд посылка, которая не может быть доказана. На ее основе, мы можем построить некую теорию. Но тот факт, что аксиома недоказуема, в рамках теории, которая на нее опирается, она неполна.

Если же мы в рамках теории попытаемся доказать нашу посылку, то очевидно, что теория впадет в противоречие, поскольку она обосновывает собственное основание. Т.е. на момент, когда она пытается обосновать свою посылку, она отрицает собственное существование, поскольку, если посылка не доказана «из-вне», не может существовать и самой теории. В этом и заключается основная проблема, аналогичная парадоксу лжеца.

Поэтому, я действительно удивляюсь, когда слышу, что теория может быть полной и одновременно непротиворечивой. Это взаимоисключающие понятия.

Да ладно?

Допустим, правильность это метатеоретическое свойство которое не формализируется в T.

я не понял что подразумевается под правильности, речь шла о полноте.

То что ты цитируешь :) А теперь сравни с определением противоречивости и непротиворечивости для лямбда-исчисления которое я процитировал из Барендрегта.

Да вопрос не в противоречивости, а в том, что понимать под «в качестве логики». Мне это неясно. То есть определение «можно вывести (А и не-А)» в рамках ULC вообще не имеет смысла, т.к. нету ни понятия выводимости (или какого-либо его эквивалентна, через modus ponens как в типизированных исчислениях), ни отрицания.

В FOL есть формулы _|_, T, => и т.п., в STLC(++) — типы.

Я хотел увидеть формальное определение. Или мы гвоорим «это логика» - просто как некоторое неформальное, интуитивное утвержедние?

http://en.wikipedia.org/wiki/Curry's_paradox#Lambda_calculus

Но в ULC нету true и false. В смысле, мы можем выбрать два терма, которые будут буд-то true и false - но есть ведь еще куча термов.

Если взять категорию ULC на одном (!) рефлексивном объекте и категорию какого-нибудь STLC с {T, F, * -> *, * x *, * | *}, то нужной функторной эквивалентности явно нет.

А с чего бы у ULC и STLC была эквивалентность?

Как же это согласуется с теоремой Геделя о неполноте?

Там есть оборот «sufficiently strong», а если не sufficiently strong, то эта теорема не факт что распространяется на теорию в вопросе.

Как может быть теория свободна от логики, если любая теория — есть ни то иное, как логические построения.

Теория T языка L это произвольное множество формул (при определённости термов и формул) называемых аксиомами T.

Если от этого абстрагироваться, любой бред можно назвать теорией.

This. Ну так принято в математике.

Чем является утверждение «Если а = b и b = c то b = c»? Это, на мой взгляд посылка, которая не может быть доказана.

В смысле транзитивность? Запросто может.

Конкретизируй — что за теория, что за посылки.

Поэтому, я действительно удивляюсь, когда слышу, что теория может быть полной и одновременно непротиворечивой.

http://en.wikipedia.org/wiki/Presburger_arithmetic#Properties

Но это доказывается внешними средствами.

Доказательство непротиворечивости внутренними средствами я видел — ссылку привёл (можно ли доказать ещё полноту/правильность в подобном случае внешними средствами — не знаю).

Но тот факт, что аксиома недоказуема, в рамках теории, которая на нее опирается, она неполна.

В любой теории есть правила вывода. Ну, самое известное, например - modus ponens: если выводимы высказывания «X» и «X => Y», то выводимо высказывание «Y». В общем правило вывода имеет левую часть (посылки) и правую (вывод), левая часть есть некое множество высказываний, оно может быть пустым, такие правила вывода являются аксиомами. Требовать «доказательство аксиом» то же самое, что требовать доказательства правил вывода - это вещи метатеоретические, внешние по отношению к теории.

Под полнотой теории подразумевается, что если у нас есть некое высказывание А (А может быть сформулировано в языке данной теории), то в этой теории выводимо либо А, либо не-А. То есть полнота требует, чтобы _какое-нибудь_ из двух было выводимо. При этом если выводимы оба, то теория называется противоречивой (в обратном случае - непротиворечивой). Понятно, что если теория противоречива, то она полна. Но если теория полна - то это не значит, что она непротиворечива.

Доказательство непротиворечивости внутренними средствами я видел — ссылку привёл (можно ли доказать ещё полноту/правильность в подобном случае внешними средствами — не знаю).

Доказательства Геделя для непротиворечивости и полноты ЛПП как раз «внутренние», емнип.

я не понял что подразумевается под правильности, речь шла о полноте.

Soundness подразумевается. Чем completeness отличается и как формализуется внутри T?

Soundness подразумевается.

а у Soundness вообще есть формальное определение? Я всегда думал, что это нечто «интуитивное».

Чем completeness отличается и как формализуется внутри T?

А чем непротиворечивость отличается от полноты в этом плане?

Конкретизируй — что за теория, что за посылки.

Да нет, это не конкретная теория, это мое собственное обобщение, как мне казалось, справедливое для любой теории.

Или мы гвоорим «это логика» - просто как некоторое неформальное, интуитивное утвержедние?

Неформально, да. Просто исторически же были попытки использовать ULC в качестве логики, отсюда все эти ранние утверждения о её противоречивости и парадоксы. Помимо типизированных вариантов были попытки починить этот момент, они даже частично удались (у Карри, ЕМНИП), просто получившаяся «логика» оказалась бедной.

А формально — ну как угодно, любая интерпретация позволяющая смотреть на вещи как на формулы/доказательства/выводы и наоборот.

А с чего бы у ULC и STLC была эквивалентность?

Вот я и говорю — такой функторной интерпретации нет, то есть вообще :)

Просто исторически же были попытки использовать ULC в качестве логики

Да ну? Каким образом? ULC это же обычный группоид, и теория у него - теория обычного группоида, как отсюда получить логику?

Anoimous. Возраждение.

А я же писал, что мы с коллегами работаем над его излечением, и постить он временно не сможет. Никто не поверил и меня забанили. А сами проверьте:

www.linux.org.ru/show-comments.jsp?nick=anonimous

Последний коммент 2 числа. А сейчас он на лечении и идет на поправку.

А вот ТС'ом предстоит заняться

Soundness: T ⊢ f ⇒ T ⊨ f

Completeness: T ⊨ f ⇒ T ⊢ f

Inconsistency: T ⊢ f ∧ ¬f

Consistency: T ⊬ f ∧ ¬f

Заметьте, что пациент в оп ведет диалог с собой же. Как мило!

Какие закорючечки! Глянул на тред, да тут одни кандидаты в доктора! Моё почтение

Каким образом?

Я не знаю, но есть работы Чёрча 32/33 годов и Карри 30/58/72-ых.

Soundness: T ⊢ f ⇒ T ⊨ f
Completeness: T ⊨ f ⇒ T ⊢ f

⊢ - выводимость, с-но ⊨ - общезначимость? тогда ты тут местами перепутал (по крайней мере для полноты) :)

Consistency: T ⊬ f ∧ ¬f

Ну так и у полноты есть немодельное определение (то, что выводимость тождественна общезначимости вообще только Гедель доказал):

(T ⊢ f) или (T ⊢ ¬f)

В твоих словах, однако, читается зависть к сабжу. Он хоть и некомпетентен в програмировании и математике, но мозгов и харизмы в нем куда больше, чем, например, в тебе. Ты завидуешь, так, потому что тебе на лоре не уделют столько же внимаания, сколько ему, да малыш? Или у вас что-то личное?

но мозгов и харизмы в нем куда больше, чем, например, в тебе

Залогинься!

Пока вы одного дебила лечили, два новых появилось

Не, ну я другого объяснения твоего поведения просто не вижу. Ты же постоянно пытаешься поднять тему, отслеживаешь его комменты, читаешь треды. Ну ладно, будем считать, что это случайность. Продолжаем наблюдения:)

Ну вот, и ты сам с собой заговорил. Начинааешь копировать поведение? Это уже посерьезней будет.

Я тебе сразу скажу: когда в социуме появляется такой вот эксцентрик (причём пофигу одаренный ли он или наоборот дурачок как анонiмус) начинается травля со стороны «людей как все». Ну и я, среднестатистический человек (таки быдло, если тебе угодно), ясное дело, не мог пройти мимо. И если ты повнимательнее почитаешь, не я закидывал его говном больше всего и не пытался что-то объяснять. Потому что объяснять ему нет смысла. А вот назвать больным - самое то!

Удовлетворил я твоё любопытство?

Стоп! Сколько вас всего анонимусов в этом треде?

Не знаю, реальные дурачки мне не интересны, я просто прохожу мимо. Каждому свое, видимо.

Э, не! Это человеческая психология, товарищ. И вообще, а что ты тогда делаешь на ЛОРе?

http://en.wikipedia.org/wiki/Completeness#Logical_completeness

http://en.wikipedia.org/wiki/Soundness#Soundness

http://en.wikipedia.org/wiki/Soundness#Relation_to_completeness

http://u.math.biu.ac.il/~dahari/download/Mathematical Logic/Elad 22.pdf

Да вроде не перепутал — теорема => тавтология (soundness), тавтология => теорема (semantically complete).

(T ⊢ f) или (T ⊢ ¬f)

По первой ссылке это называется syntactically complete, то что фигурирует в теореме о неполноте.

Также там утверждается

Truth-functional propositional logic and first-order predicate logic are semantically complete, but not syntactically complete

http://en.wikipedia.org/wiki/First-order_predicate_logic#Completeness_and_und...

http://en.wikipedia.org/wiki/Gödel's_completeness_theorem#Preliminaries

http://en.wikipedia.org/wiki/Gödel's_completeness_theorem#Relationship_to_the...

The name for the incompleteness theorem refers to another meaning of complete

Т.е., например, полнота FOL это модельная полнота, а синтаксической полноты и нет вовсе.

Да вроде не перепутал — теорема => тавтология (soundness), тавтология => теорема (semantically complete).

Действительно, это я в значках запутался.

Т.е., например, полнота FOL это модельная полнота, а синтаксической полноты и нет вовсе.

А можно пример такой формулы, которая невыводима в ЛПП вместе с отрицанием? Пример по ссылке не подходит, т.к. пропозиционные переменные не являются формулами ЛПП.

В продолжение темы о функциональной чистоте ФП.

Дабы избежать спекуляций фп-фанбоев, которые имеют склонность уходить от вопросов в дебри схоластики уровня дворовой гопоты и алгебры 5-го класса, привожу простейший пример, ибо его достаточно, для прояснения вопроса.

https://github.com/haskell/bytestring/blob/master/Data/ByteString/Internal.hs

Я рассматриваю данный код исключительно с практической точки зрения, абстрагируясь от пространных рассуждениях о чистоте и математических абстракциях. Тем более, данные абстракции протухли уже лет 80 как.

Небольшой пример для Ъ

-- | This \"function\" has a superficial similarity to 'unsafePerformIO' but
-- it is in fact a malevolent agent of chaos. It unpicks the seams of reality
-- (and the 'IO' monad) so that the normal rules no longer apply. It lulls you
-- into thinking it is reasonable, but when you are not looking it stabs you
-- in the back and aliases all of your mutable buffers. The carcass of many a
-- seasoned Haskell programmer lie strewn at its feet.
--
-- Witness the trail of destruction:
--
-- * <https://github.com/haskell/bytestring/commit/71c4b438c675aa360c79d79acc9a491e7bbc26e7>
--
-- * <https://github.com/haskell/bytestring/commit/210c656390ae617d9ee3b8bcff5c88dd17cef8da>
--
-- * <https://ghc.haskell.org/trac/ghc/ticket/3486>
--
-- * <https://ghc.haskell.org/trac/ghc/ticket/3487>
--
-- * <https://ghc.haskell.org/trac/ghc/ticket/7270>
--
-- Do not talk about \"safe\"! You do not know what is safe!
--
-- Yield not to its blasphemous call! Flee traveller! Flee or you will be
-- corrupted and devoured!
--
{-# INLINE accursedUnutterablePerformIO #-}
accursedUnutterablePerformIO :: IO a -> a
#if defined(__GLASGOW_HASKELL__)
accursedUnutterablePerformIO (IO m) = case m realWorld# of (# _, r #) -> r
#else
accursedUnutterablePerformIO = unsafePerformIO
#endif

С превеликой скорбью приходится констатировать, что ФП-критикуны, не написали ни одной строчки когда, делающей хоть что-то полезное (многочисленные факториалы, с хелловордами не в счет). И это очень печально, я щитаю. Очень печально...

Для повышения квалификации, предлагаю почитать статьи Вадлера по теме: http://homepages.inf.ed.ac.uk/wadler/topics/history.html Начать можно с его Propositions as Types, разделы 1-3.

По ссылке обычная борьба с Си-говном в попытках получить юзабельное АПИ. Что сказать-то хотел?

По ссылке обычная борьба с Си-говном

Ровно такая же «борьба с Си-говном» присутствует и в array, только происходит на хаскельной куче, и запрятана поглубже.

И не ради «юзабельного АПИ», а ради хоть сколько-нибудь приличной скорости работы. Да, и всё общесистемное окружение — сплошное Си-говно. И либо, ты учишься с ним «договариваться», либо... Либо налицо очередная академическая поделка.

Нет никакой разницы, что именно: либо многочисленные костыли и квирки рантайма, либо брутальный подход с использованием FFI.

Короче говоря, если «чистое ФП» и не миф, то к хаскелю оно не имеет ровным счетом никакого отношения.

Ещё небольшой пример:

foreign import ccall unsafe "hashk_128"
  __hashk_128 :: CString -> CString -> IO ()

hashk :: ByteString -> ByteString
hashk str_ = unsafePerformIO $ do
  let res_ = B.replicate 128 0
  B.useAsCString str_ $ \str -> unsafeUseAsCString res_ $ \res -> __hashk_128 str res
  return res_

__hashk_128 мутирует буфер от ByteString — нормально или могут быть проблемы? Пока вроде брат жив :)

Начать можно с его Propositions as Types, разделы 1-3.

Он там про unsafePerformIO и протухшем ФП пишет (дожили, у хаскелистов уже чистое ФП и математические абстракции протухли)?

у хаскелистов уже чистое ФП и математические абстракции протухли

Не цепляйся к словам. Я имел ввиду нетипизированное лямбда-исчисление.

B.useAsCString все-равно сделает копию байтстринга, хоть и на сишной куче, так что брат не умрет в любом случае.

А вот с unsafeUseAsCString нужно обращаться поучтивее, т.к. байтстринги не \0-терминированы.

Ну да, если приходится пользоваться unsafePerformIO, а им приходится пользоваться, потому что вся ось написана на C, то есть вероятность, что твои функции окажутся не функциями. Это типа какой-то секрет?

Да, можно и в Хаскеле забить на чистоту, если ты реально идиот, только как это становится аргументом против Хаскеля не особо понятно.

Против чистоты Хаскеля, естественно.

А когда ты откроешь для себя unsafeCoerce, то, видимо, придется читать твои посты про то какой Хаскель типонебезопасный?

B.useAsCString все-равно сделает копию байтстринга

А вот с unsafeUseAsCString нужно обращаться поучтивее, т.к. байтстринги не \0-терминированы.

Да, у меня там

void hashk_128(const char* /* <- null-terminated */, char[128] /* <- array */);

Хотя можно было и

void hashk_128(const char* /* <- buffer */, size_t /* <- its size */, char[128] /* <- array */);

с

unsafeUseAsCString str_ $ \str -> unsafeUseAsCString res_ $ \res -> __hashk_128 str (length str_) res

Мне больше интересно принято ли вот так локально ломать прозрачность с помощью unsafeUseAsCString и левого сишного кода с последующим вытаскиванием из под IO с тем обоснованием, что для одинаковых str hashk_128 заполняет одинаковые хеши в res.

А можно пример такой формулы, которая невыводима в ЛПП вместе с отрицанием?

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

Мне больше интересно принято ли вот так локально ломать прозрачность

Как я понял — все-таки да. В противном случае, просядет производительность, да и фрагментацию сишной кучи разводить совсем не стоит.

Сами по себе байтстринги это вообще ForeignPtr, со всеми вытекающими. Т.е. по факту, никакой ссылочной прозрачности не ломается. Байтстринги не являются АТД. Ни что нам не мешает юзать ForeignPtr, включая принудительное выполнение его финалайзера.

Еще хуже, что байтстринги никогда не копируются, и операции типа take и drop не обладают ссылочной прозрачностью, т.к. хоть и возвращают «новый» байтстринг, но указатель остается прежним. Но делать ставку на это категорически нельзя, т.к. при неправильно заданных параметрах они возвращают empty.

Право слово, лучше бы все это работало бы через ST.

Короче говоря самая настоящая Темная Сторона. И требует соответствующего уважения.

Насчет вытаскивания из-под IO — не знаю. Я из-под IO вытаскиваю только в очень-очень редких случаях.

Я разобрался. Суть в том, что ЛПП - не теория, по-этому она не может быть полной, понятие полноты для нее не определено. Чтобы получить теорию, нам надо выбрать для ЛПП некую сигнатуру - тогда мы уже получим теорию первого порядка. Если сигнатура, например, пустая, полученная теория очевидно синтаксически полна - т.к. просто у нас не будет формул :)

Когда же говорится о семантической полноте ЛПП, то имеется ввиду полнота для теории ЛПП с любой сигнатурой (таковых теорий много). Ну и еще даже более сильно - семантически полны вообще все расширения ЛПП (они же - теории первого порядка).

А вот для сигнатуры арифметики (при этом аксиомы арифметики, допустим, добавлять не будем) синтаксической полноты, очевидно, не будет.

Видимо это должна быть формула истинная не во всех моделях,

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