В чем разница между суждениями и суждениями?

27

Меня смущает тонкое различие между суждениями и суждениями, когда они подвергаются интуиционистской теории типов. Может ли кто-нибудь объяснить мне, в чем смысл отличать их и что отличает их? Особенно ввиду Карри-Ховарда Изоморфсима.

день
источник
Возможно, вам будет интересно почитать en.wikipedia.org/wiki/…
Энтони

Ответы:

17

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

Суждение - это то, что мы можем знать, то есть объект познания. Суждение очевидно, если мы действительно знаем это.

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

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

говорит Нордстрем и соавт. С другой стороны, в классической логике и в целом пропозиции - это объекты, выраженные на языке, который может быть «истинным» или «ложным».

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

Я предлагаю «Конструктивную логику» Фрэнка Пфеннинга , «Доказательства и типы» Жана-Ива Жирара и «Программирование в теории типов Мартина-Лёфа» Бенгта Нордстрома и др. Все три свободно доступны в Интернете. Последний, вероятно, наиболее близок к тому, что вы хотите, так как он ориентирован на программирование и подробно рассказывает о значении этих терминов и многом другом.

Энтони
источник
2
Первая цитата - Фрэнк Пфеннинг, а не Жирар.
Ноам Цайлбергер
Один вопрос: правильно ли утверждать, что (под высказыванием как парадигмой типа) высказывания являются типами, а суждения являются следствием / выражением (логической структуры) теории типов?
Джорджио Мосса,
1
Откуда мы знаем, что знаем что-то? (Относительно «Суд очевиден, если мы на самом деле знаем его»?)
CMCDragonkai
16

Возможно, я могу попытаться дать менее метафизический ответ.

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

Существует метаязык, который также является логическим языком, в котором мы пытаемся объяснить, какие вещи в базовом языке являются истинными или ложными. Заявления, которые мы делаем на этом мета-языке, называются «суждения».

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

Удай Редди
источник
14

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

Андрей Бауэр
источник
1
Мне обычно нравятся ваши ответы, Андрей, но в этом случае я не следую. Почему среда заявления имеет значение? Или это разница в глаголах «говорить» и «провозглашать». В таком случае, откуда мы знаем, что текст не провозглашается, а миссис Марпл не говорит? Единственное другое отличие, которое я вижу, состоит в том, что текст пассивен, а миссис Марпл активна; но кто-то написал текст, верно?
Энтони
6
Тот факт, что мы можем сформулировать предложение «Дворецкий сделал это», ничего не значит. Тот факт, что он существует на листе бумаги, ничего не значит. Но когда миссис Марпл выносит суждение «Дворецкий сделал это» перед всеми, собравшимися в милом викторианском читальном зале, это совершенно другое. Возможно, я был слишком загадочным.
Андрей Бауэр
@ Андрей Бауэр: Я должен извиниться за то, что проголосовал за вас раньше, теперь я вижу смысл. Большое спасибо.
день
12

В теориях типа Мартина-Лёфа суждения являются частью речевых актов . Есть четыре (или пять согласно Википедии) суждения:

  • A TYпеA
  • s:AsA
  • sзнак равноT:AsTA
  • Aзнак равноВAВ
  • Γ СоNTеИксTΓ

AATAT:ATAT:A

Я бы добавил «Основы конструктивной математики» Майкла Бисона к предложениям в ответе Энтони. Мартин-Лёф дал несколько выступлений, которые очень хорошо объясняют его теорию, но, к сожалению, большинство из них не превратились в опубликованную им форму (но посмотрите этот сайт ).

Кава
источник
Спасибо за перечисление. Но мой вопрос сейчас заключается в том, не являются ли эти суждения тривиально превращаться в суждения? Например, «A - это тип» - это просто предикат, когда A создается, например, посредством Nat, это становится предложением, не так ли?
день
ΓT:A
1
T:A(Γ)
2
@plmday, может быть полезно следующее, почему это не может произойти с математической точки зрения: «вы не можете иметь вселенную, относитесь к« p доказывает A »как к предложению и имеете разрешимый предикат доказательства». [Beeson 1980, p. 409]. (Но для Мартина-Лёфа главная проблема заключается в том, что они концептуально отличаются, и их запутывание приведет к неоправданным основаниям, которые могут привести к парадоксальным результатам.)
Каве,
2
Я хотел бы добавить, что это кажется мне слишком специфичным, поскольку существует множество других версий ITT с другими решениями (например, Пропорция CoC). Я думаю, что более важная концепция здесь содержится во втором комментарии Каве: попытка превратить некоторые суждения в суждения может внести в теорию тонкие и опасные проблемы. Это не означает, что теория типов не может быть описана в теории типов, но только то, что между метатеорией, теорией и выражениями в этой теории существуют четкие линии.
Энтони,
4

Суждения - это композиция двух вещей:

  1. п
  2. A

A[п]

[п][п][T]ЧАС1,...,ЧАСNA1,...,ANгде некоторые логики имеют такие суждения, которые нетривиально эквивалентны любому предложению языка логики. Таким образом, различные виды пропозициональных представляются в довольно элементарной классической логике.

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

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

Чарльз Стюарт
источник
-3

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

Сэмюэл Дюкло
источник
1
Вы ошибаетесь, говоря, что решение было проверено. Проверенное (доказанное) суждение называется теоремой.
Андрей Бауэр