Смысл некоторых формул логики второго порядка

[epros]

Как известно, язык логики второго порядка позволяет говорить о "любых свойствах объектов" (имея в виду в том числе и невыразимые формулами свойства). Я тут задумался над тем, каков мог бы быть смысл подобных формулировок, и первый же подвернувшийся пример показался мне несколько странным. Вот скажите, как можно трактовать формулу:

$\forall Z ~ Z(x) \to Z(y)$?

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

[Sonic86]

$x=y$? (бредово)

[epros]

Sonic86 в сообщении #1157140 писал(а):

$x=y$? (бредово)

Бинго! Я тоже так прочитал и тоже удивляюсь, что звучит бредово.

[Sonic86]

Я не спец, но, если в формуле перейти к множествам $P(t)\to t \in P$ в какой-нибудь теории множеств со страшными множествами (нерегулярными?), то м.б. может оказаться, что предикат все-таки получается несимметричным: $x=y$ или $x=\text{страшному множеству}$. Но я такие теории так и не выучил

Ерунду пишу:
надо просто взять $Z(t)=

[alex_dorin]

$ \forall x \forall y (P(x,y) \equiv \forall Z Z(x) \to Z(y)) $
Это аксиома для предиката $P(x,y)$ для Вашего предложения, со свободными индивидными переменными.

[epros]

alex_dorin в сообщении #1157149 писал(а):

$\forall x \forall y (P(x,y) \equiv \forall Z Z(x) \to Z(y))$
Это аксиома для предиката $P(x,y)$ для Вашего предложения, со свободными индивидными переменными.

1) Я правильно понял, что $\equiv$ - это $\leftrightarrow$?
2) Что Вы хотели сказать этим $P(x,y)$?

Sonic86 в сообщении #1157148 писал(а):

надо просто взять $Z(t)=

Я рассуждал так:
Предикатную переменную под квантором всеобщности можно заменить любым выражением, соответствующим предикату. Заменим $Z$ на $\neg Z$:
$\forall Z ~ \neg Z(x) \to \neg Z(y)$.
Преобразуем по правилам логики высказываний:
$\forall Z ~ Z(y) \to Z(x)$.

Итак, получили, что формула представляет симметричное отношение. Рефлексивность очевидна. Транзитивность доказывается тоже легко. Стало быть, формула представляет отношение эквивалентности. Чтобы его можно было трактовать как равенство с точки зрения логики первого порядка нужно ещё одно - чтобы для любого предиката $\varphi$ из того, что $x$ и $y$ удовлетворяют формуле, следовало $\varphi(x) \leftrightarrow \varphi(y)$. Но это, собственно, очевидно из того, что выполняются $\forall Z ~ Z(x) \to Z(y)$ и $\forall Z ~ Z(y) \to Z(x)$.

[alex_dorin]

[/quote]

epros в сообщении #1157168 писал(а):

1) Я правильно понял, что $\equiv$ - это $\leftrightarrow$?

да, это знак эквивалентности.

epros в сообщении #1157168 писал(а):

2) Что Вы хотели сказать этим $P(x,y)$?

$P(x,y)$ - это двухместный предикат для Вашего предложения , содержащего свободные переменные $x, y$.
О его доказуемости говорить нельзя.

[epros]

alex_dorin в сообщении #1157173 писал(а):

$P(x,y)$ - это двухместный предикат для Вашего предложения , содержащего свободные переменные $x, y$.
О его доказуемости говорить нельзя.

Разумеется, формула была с двумя свободными предметными переменными, стало быть, она выражает бинарное отношение между объектами. Мы здесь, вроде, говорили не о её "доказуемости", а о том, что это отношение странным образом вдруг оказалось отношением равенства.

[Sonic86]

А вообще в этой логике нетривиальные предикаты есть?

[Nemiroff]

https://en.wikipedia.org/wiki/Identity_ ... scernibles

[arseniiv]

Sonic86 в сообщении #1157182 писал(а):

А вообще в этой логике нетривиальные предикаты есть?

Имеется в виду, какие из них определимы в чистой логике второго порядка?

-- Вт окт 04, 2016 20:40:26 --

Тут всё просто. Модель чистой логики второго порядка, очевидно, определяется одним множеством. Изоморфизмы множеств — это биекции, так что определимые отношения или операции должны быть инвариантными относительно биекций носителя. Так что для бинарного отношения $R$, например, $y\ne z\to (xRy\leftrightarrow xRz)$ и, скажем, $x=y\to(xRx\leftrightarrow yRy)$. Оно определяется только значениями, которые оно принимает на одинаковых и на разных элементах — не более четырёх определимых в каждой модели бинарных отношений: тождественные ложь и истина, равенство и неравенство. Так же можно обойтись и с остальными определимыми отношениями и операциями.

[Sonic86]

arseniiv в сообщении #1157256 писал(а):

Sonic86 в сообщении #1157182 писал(а):

А вообще в этой логике нетривиальные предикаты есть?

Имеется в виду, какие из них определимы в чистой логике второго порядка?

Да. Точнее - насколько сложные предикаты могут быть выражены формулами, замкнутыми по переменным типа "свойство"

arseniiv в сообщении #1157256 писал(а):

Тут всё просто. Модель чистой логики второго порядка, очевидно, определяется одним множеством. Изоморфизмы множеств — это биекции, так что определимые отношения или операции должны быть инвариантными относительно биекций носителя. Так что для бинарного отношения $R$, например, $y\ne z\to (xRy\leftrightarrow xRz)$ и, скажем, $x=y\to(xRx\leftrightarrow yRy)$. Оно определяется только значениями, которые оно принимает на одинаковых и на разных элементах — не более четырёх определимых в каждой модели бинарных отношений: тождественные ложь и истина, равенство и неравенство. Так же можно обойтись и с остальными определимыми отношениями и операциями.

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

[warlock66613]

(Оффтоп)

Кто о чём, а epros о логике второго порядка (я как раз недавно читал вашу предыдущую тему на эту тему).

[arseniiv]

Sonic86
Если я нигде не нафейлил, то равенство, да. Правда, надо всё-таки доказать отдельно, что больше-чем-бинарные отношения будут раскладываться по таким бинарным. Ещё тут есть место для комбинаторики: неизоморфных $n$-арных будет столько же, сколько функций из непомеченных разбиений $n$-элементного множества в $\{0,1\}$.

А вот с функциями скучнее. Выразима тождественная функция и вообще функции, равные одному из своих аргументов, и больше не должно быть никаких. Так что нульарных функций вообще не выразима ни одна, несмотря на то, что в модели с областью из одного элемента мы могли бы выбрать её однозначно. Только чтобы это сделать, надо ограничить модели одноэлементными дополнительной аксиомой $x=y$, и это будет уже не чистая логика второго порядка.

[Sonic86]

arseniiv в сообщении #1157322 писал(а):

А вот с функциями скучнее.

Я не понял, откуда Вы берете функции. Берете кванторы по функциям?

arseniiv в сообщении #1157322 писал(а):

Если я нигде не нафейлил, то равенство, да.

Я, честно говоря, не вижу доказательства

А вообще в чем пафос этой логики второго порядка, если там кроме равенств нет ничего?