КОНСПЕКТ
по математическа логика
за III курс математика
2005/2006 уч. година
- Функции и предикати в дадено множество. Сигнатури и структури. Термове. Еднозначност на прочита им.
- Множество на променливите на терм. Затворени термове. Семантика на термовете. Атомарни формули. Еднозначност на прочита им.
- Множество на променливите на атомарна формула. Затворени атомарни формули. Семантика на атомарните формули. Ербранови структури.
- Формули. Еднозначност на прочита им. Свободни и свързани променливи на формула. Затворени и отворени формули.
- Семантика на формулите. Тъждествена вярност и изпълнимост на формули.
- Еквивалентни формули.
- Модели и изпълнимост на множество от формули. Следване на формула от множество от формули.
- Импликация и еквиваленция. Конюнкции и дизюнкции с произволен ненулев краен брой членове.
- Заместване на променлива с терм в терм.
- Заместване на променлива с терм във формула - дефиниция и синтактични свойства.
- Стойност на резултат от заместване на променлива с терм във формула. Основни съотношения на следване за кванторите. Структури с термално породен носител.
- Преименуване на свързана променлива. Привеждане на формула в пренексен вид.
- Скулемизация. Скулемова нормална форма.
- Затворени частни случаи на формулите. Ербранови модели на множества от отворени формули.
- Дизюнкти. Непосредствена резолвента на два дизюнкта. Метод на резолюцията.
- Теорема за компактност за множества от затворени дизюнкти.
- Пълнота на метода на резолюцията.
- Представяне на безкванторна формула чрез крайно можество от дизюнкти.
- Теорема за компактност за множества от формули.
- Бисимулация.
- Факторизация на структура.
- Предикатно смятане с равенство. Свеждане на семантични въпроси за предикатното снятане с равенство към съответни въпроси за общото предикатно смятане.
- Теорема за компактност в предикатното смятане с равенство. Нестандартни естествени числа.
- Теорема на Льовенхайм-Скулем.
- Свойства на удовлетворяването и на изпълнимостта на множества от формули.
- Секвенции. Формална системa от Генценов тип за предикатното смятане.