Сравнение подходов к управлению свободными и связанными переменными.

Исправления:

я изначально сказал ф ( Икс , ж 1 ⋯ ж н , а ) была замкнутой корректной формулой. Это не. Я хотел сказать, что внутри ф единственные свободные переменные происходят из Икс , ж 1 ⋯ ж н , а , т.е. ФВ ( ф ) ⊂ { Икс , ж 1 ⋯ ж н , а } .

Сравнение подходов к управлению свободными и связанными переменными.

Какие существуют подходы к управлению свободными и связанными переменными в корректных формулах? Есть ли какие-либо ссылки, которые явно сравнивают несколько способов сделать это и говорят об их преимуществах и недостатках?

Например, вот схема спецификации аксиомы Z(F)(C) , представленная Википедией, но со всеми переменными в нижнем регистре и некоторыми незначительными изменениями в обозначениях.

∀ ж 1 ⋯ ж н . ⁡ ∀ а . ⁡ ∃ б . ⁡ ∀ Икс . ⁡ ( Икс е б ) ↔ ( Икс е а ∧ ф ( Икс 1 , ж 1 ⋯ ж н , а ) )

Обратите внимание, что все переменные символы связаны.

В условном обозначении, использованном в статье, ф является правильно построенной формулой. ф ( Икс 1 , ж 1 ⋯ ж н , а ) является правильно сформированной формулой и тем фактом, что б не появляется в ( Икс 1 , ж 1 ⋯ ж н , а ) имеет большое значение. Дело в том, что б не происходит означает, что б не встречается бесплатно в ф . Я не уверен, как определить ф ( в → ) для произвольного в → в этой нотации ... Я обычно думаю об этом как о способе объявления зависимостей в некотором смысле, когда точная интерпретация зависит от контекста.

Я думаю, что есть некоторые технические преимущества при определении синтаксиса для разделения символов связанных и свободных переменных. Я не придумал разделять свободные и связанные переменные, но не помню, где я это видел.

Пусть строчная латинская буква является связанным переменным символом, а прописная латинская буква — свободным переменным символом. Позволять ψ [ М "=" х ] быть подстановкой, избегающей захвата, заменяющей М с х в правильно построенной формуле ψ .

Используя это соглашение, приведенную выше формулу можно записать следующим образом.

∃ б . ⁡ ∀ Икс . ⁡ ( Икс е б ) ↔ ( Икс е А ∧ ф [ Икс "=" Икс ] )

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

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

вы можете найти индексы де Брейна актуальными! может быть литература, сравнивающая индексы де Брейна с другими методами связывания, что могло бы послужить отправной точкой.
Вы уверены, что хотите сказать, что ф закрытая формула ? «Закрытая формула» обычно означает то же, что и «предложение»: нет свободных переменных. Но Икс , ж 1 , … , ж н , а может все произойти бесплатно в ф .
Я хотел сказать, что аргументы ф захватите все зависимости, которые ф имеет (и поэтому отсутствие б имеет смысл). Закрыта — это определенно не то слово, но я не знаю, что это такое.
Обозначение ф ( в 1 , … , в н ) обычно используется для обозначения свободных переменных формулы ф среди в 1 , … , в н . То есть каждая свободная переменная в ф один из в я , но не все в я должны происходить бесплатно в ф . Это очень полезная запись, потому что тогда мы можем написать ф ( а 1 , … , а н ) для операции замены а я за каждый бесплатный экземпляр в я . И это дает понять, что ф естественно определяет подмножество А н / ан н -арное отношение на А , для любой структуры А .
Обычно нет необходимости аналогичным образом указывать связанные переменные в формуле ф , потому что после связывания их личности не имеют значения. То есть вы можете обменять связанную переменную (в ее квантификаторе и в каждом случае в пределах области действия этого квантификатора) на другую переменную без изменения значения формулы.
Спасибо. То, что меня всегда смущало ф ( в → ) в том, что оно использовалось как для того, чтобы сказать ФВ ( ф ) ⊂ в → и сказать ф [ Икс 1 "=" в → 1 ⋯ Икс н "=" в → н ] где Икс я это я й свободной переменной ... поэтому мне всегда было интересно, что важнее: «имя» параметра или его позиция в списке аргументов. // Индексы Де Брюйна — еще одна хорошая альтернатива. Я видел их раньше в обсуждениях лямбда-исчисления, хотя замена нетривиальна и требует добавления.
Генцен (отец ND и Sequent Calc) использовал подход к разделению переменных: Икс , у используется только привязка, из параметров : а , б используется только бесплатно. Пример с ∀ -Вступительное правило: ф ∀ Икс ф [ Икс / а ]
Я думаю, что некоторые связанные (но не исчерпывающие) материалы могут быть разбросаны по документации Metamath Proof Explorer, например ZFC Axioms Without Distinct Variable Conditions .

Ответы (1)

«Я думаю, что есть некоторые технические преимущества при определении синтаксиса для разделения символов связанных и свободных переменных. Я не придумал идею разделения свободных и связанных переменных, но я не помню, где я это видел». Прием использования разных букв для связанных переменных [т. е. переменных, которые служат для привязки префиксов кванторов к местам в простых или сложных предикатах] и для свободных переменных [выражений, основное использование которых в качестве параметров / фиктивных имен / «произвольных» имен, как вы предпочитаете чтобы выразить это] есть в оригинальных исследованиях естественной дедукции Генцена 1930-х годов, а затем снова в классической книге Правица 1965 года. Он рассматривается в некоторых более поздних влиятельных учебниках по логике, начиная с учебников Леммона и Томасона.

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

Сравнение подходов к управлению свободными и связанными переменными.
СпросиСетьПолитика конфиденциальности1y, 0v