2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему
 
 Логические пруверы логики 1-го порядка и NBG
Сообщение17.11.2015, 16:01 


08/03/11
273
Здравствуйте !
Возможно ли использовать логические пруверы для первопорядковой логики, именно Vampire, E, Spass
для доказательства теорем в теории множеств NBG ?
Наверное, этого делать нельзя из-за использования в NBG индивидных переменных 2-х сортов.
Верен ли мой такой вывод ? Обязательно ли преобразовывать все аксиомы NBG и гипотезы с использованием индивидных переменных одного сорта ?
C уважением,
Александр А. Дорин

 Профиль  
                  
 
 Re: Логические пруверы логики 1-го порядка и NBG
Сообщение17.11.2015, 18:43 
Заслуженный участник


27/04/09
28128
Странный вопрос.
1. На него должна ответить документация по тем системам.
2. Если всё плохо, то, разумеется, преобразуйте к виду с переменными одного сорта, а лучше просто найдите такое представление — оно уже очень давно где-нибудь должно быть выписано.

Хотя, конечно, на форуме могут оказаться люди, которые лучше вас знают Vampire, E и Spass. :roll:

-- Вт ноя 17, 2015 20:44:11 --

(А что стало с ZFC?)

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

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



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

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


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

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group