Дискуссионный математический форумМатематический форум
Математический форум Math Help Planet

Обсуждение и решение задач по математике, физике, химии, экономике

Теоретический раздел
Часовой пояс: UTC + 3 часа [ Летнее время ]
новый онлайн-сервис
число, сумма и дата прописью

Часовой пояс: UTC + 3 часа [ Летнее время ]




Начать новую тему Ответить на тему  [ Сообщений: 4 ] 
Автор Сообщение
 Заголовок сообщения: Ещё одно свойство равенства
СообщениеДобавлено: 05 авг 2022, 23:29 
Не в сети
Light & Truth
Зарегистрирован:
23 авг 2010, 22:28
Сообщений: 4405
Cпасибо сказано: 562
Спасибо получено:
1075 раз в 952 сообщениях
Очков репутации: 313

Добавить очки репутацииУменьшить очки репутации
Задача для любителей формальных доказательств. Пусть есть любое классическое исчисление предикатов первого порядка (гильбертовское, с аксиомами и правилами вывода). Добавим к нему три свойства равенства: рефлексивность ([math]\forall x (x=x)[/math]), симметричность ([math]\forall x,y (x=y \to y=x)[/math]), транзитивность ([math]\forall x,y,z ((x=y \and y=z) \to (x=z))[/math]). Требуется доказать, используя любые производные правила вывода (доказуемые в данном исчислении), что [math]\vdash \exists x \exists y (x=y)[/math].

P.S. Как решать, я знаю. Возможно, кому-то эта задача будет интересна.

Вернуться к началу
 Профиль  
Cпасибо сказано 
 Заголовок сообщения: Re: Ещё одно свойство равенства
СообщениеДобавлено: 06 авг 2022, 02:22 
Не в сети
Последняя инстанция
Зарегистрирован:
06 июн 2013, 16:17
Сообщений: 2423
Cпасибо сказано: 101
Спасибо получено:
718 раз в 674 сообщениях
Очков репутации: 155

Добавить очки репутацииУменьшить очки репутации
Сначала доказываем [math]x=x[/math] из рефлексивности, а затем вводим квантор существования два раза.

Вернуться к началу
 Профиль  
Cпасибо сказано 
За это сообщение пользователю 3D Homer "Спасибо" сказали:
Ellipsoid
 Заголовок сообщения: Re: Ещё одно свойство равенства
СообщениеДобавлено: 06 авг 2022, 12:24 
Не в сети
Light & Truth
Зарегистрирован:
23 авг 2010, 22:28
Сообщений: 4405
Cпасибо сказано: 562
Спасибо получено:
1075 раз в 952 сообщениях
Очков репутации: 313

Добавить очки репутацииУменьшить очки репутации
Есть и другой способ:

1) [math]\forall x (x=x) \to (x=x)[/math] (правило удаления квантора общности);

2) [math](x=x) \to \exists x (x=x)[/math] (правило введения квантора существования);

3) [math]\forall x (x=x) \to \exists x (x=x)[/math] (правило силлогизма: 1 и 2);

4) [math]\forall x (x=x)[/math] (рефлексивность равенства);

5) [math]\exists x (x=x)[/math] (modus ponens: 3 и 4);

6) [math]\exists x (x=x) \to \exists x \exists y (x=y)[/math] (modus ponens: 6 и 5) (правило разделения переменных, связанных квантором общности);

7) [math]\exists x \exists y (x=y)[/math] (modus ponens: 6 и 5).

3D Homer, Ваш подход я понял так:

1) [math]\forall x (x=x) \to (x=x)[/math] (правило удаления квантора общности);

2) [math]\forall x (x=x)[/math] (рефлексивность равенства);

3) [math]x=x[/math] (modus ponens: 1 и 2).

А дальше как?

Вернуться к началу
 Профиль  
Cпасибо сказано 
 Заголовок сообщения: Re: Ещё одно свойство равенства
СообщениеДобавлено: 06 авг 2022, 22:45 
Не в сети
Последняя инстанция
Зарегистрирован:
06 июн 2013, 16:17
Сообщений: 2423
Cпасибо сказано: 101
Спасибо получено:
718 раз в 674 сообщениях
Очков репутации: 155

Добавить очки репутацииУменьшить очки репутации
В книге

Верещагин Н.К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. 4-е изд. М.: МЦНМО, 2012

на с. 134 приводится аксиома [math]\varphi(t\slash x)\to\exists x\,\varphi[/math]. Здесь [math](t\slash x)[/math] есть подстановка терма [math]t[/math] вместо переменной [math]x[/math]. Формулу [math]x=x[/math] можно представить как [math](x=y)(x\slash y)[/math]. Поэтому [math]x=x\to\exists y\,x=y[/math] является аксиомой. Далее, формулу [math]\exists y\,x=y[/math] можно представить как [math](\exists y\,x=y)(x\slash x)[/math]. Поэтому [math](\exists y\,x=y)\to\exists x\exists y\,x=y[/math] также является аксиомой.

Вернуться к началу
 Профиль  
Cпасибо сказано 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему      Страница 1 из 1 [ Сообщений: 4 ]

 Похожие темы   Автор   Ответы   Просмотры   Последнее сообщение 
Одно свойство с.в. соответствующего нулевому с.зн

в форуме Линейная и Абстрактная алгебра

Gargantua

2

164

30 июн 2019, 18:44

Одно непонятное свойство двух действительных чисел

в форуме Размышления по поводу и без

ivashenko

2

287

18 авг 2016, 00:47

Свойство НОД

в форуме Алгебра

dasha math

4

346

22 июл 2014, 15:14

Одно уравнение

в форуме Алгебра

ivashenko

42

1081

03 июн 2020, 09:37

Ещё одно неравенство

в форуме Алгебра

Tantan

14

391

10 апр 2020, 12:08

Свойство логарифмов

в форуме Алгебра

Loren

21

587

27 апр 2018, 22:02

Свойство логарифма

в форуме Алгебра

sfanter

5

282

15 окт 2015, 10:52

Странное свойство

в форуме Задачи со школьных и студенческих олимпиад

Rori

11

1097

14 мар 2014, 21:00

Выполняется ли свойство?

в форуме Линейная и Абстрактная алгебра

rangersdark

0

200

08 ноя 2015, 13:56

Свойство векторов.

в форуме Линейная и Абстрактная алгебра

Aytohandas

7

381

31 май 2014, 07:57


Часовой пояс: UTC + 3 часа [ Летнее время ]



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 14


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Перейти:  

Яндекс.Метрика

Copyright © 2010-2022 MathHelpPlanet.com. All rights reserved