2014 dxdy logo

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

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




 
 Логические пруверы логики 1-го порядка и NBG
Сообщение17.11.2015, 16:01 
Здравствуйте !
Возможно ли использовать логические пруверы для первопорядковой логики, именно Vampire, E, Spass
для доказательства теорем в теории множеств NBG ?
Наверное, этого делать нельзя из-за использования в NBG индивидных переменных 2-х сортов.
Верен ли мой такой вывод ? Обязательно ли преобразовывать все аксиомы NBG и гипотезы с использованием индивидных переменных одного сорта ?
C уважением,
Александр А. Дорин

 
 
 
 Re: Логические пруверы логики 1-го порядка и NBG
Сообщение17.11.2015, 18:43 
Странный вопрос.
1. На него должна ответить документация по тем системам.
2. Если всё плохо, то, разумеется, преобразуйте к виду с переменными одного сорта, а лучше просто найдите такое представление — оно уже очень давно где-нибудь должно быть выписано.

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

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

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

 
 
 [ Сообщений: 2 ] 


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group