28. Логіки вищих порядків. Теза Гільберта.

29. Нетрадиційні логіки. Інтуїціоністська логіка. Семантка можливих світів (реляційна семантика).

Нетрадиційні логіки: інтуїціоністські й модальні логіки. Модальні –темпоральні, епістемічні, деонтичні, композиційно-номінативні модальні логіки (транзиційні, темпоральні)

Мова інтуїціоністської логіки

не діє закон виключеного третього й пов'язані з ним закони де Моргана, закон зняття подвійного заперечення. Пропозиційні зв'язки , , &,  тепер незалежні, еквіваленція подається через імплікацію та кон'юнкцію: PQ = (PQ)&(QP). Операції квантифікації x та x теж незалежні.

Задамо мову інтуїціоністської ПЛ.

Алфавiт мови складається iз символiв логiчних зв’язок , , &,  та множини Ps пропозицiйних символів.

Дамо iндуктивне визначення формули мови інтуїціоністської ПЛ:

1) кожний АPs є формулою;

2) якщо  та  – формули, то , , &,  – формули.

Алфавiт мови складається з таких символів:

– предметнi імена (змiннi) x, y, z,...;

 предикатнi символи (ПС) p₀, p₁, p₂,... заданої арностi;

 символи логiчних операцiй , , &,  та x, x.

Множину Ps предикатних символів назвемо сигнатурою мови ІЛП.

Дамо iндуктивне визначення формули мови інтуїціоністської логіки предикатів:

1) кожна атомарна формула є формулою;

2) якщо  та   формули, то , , &,   формули;

3) якщо   формула, x предметне iм’я, то x та x  формули.

Моделлю можливих світів інтуїціоністської логіки, або реляційною інтуїціоністською моделлю назвемо трійку М = (S, , I). Тут S – множина світів,  – бінарне відношення на S, I – відображення інтерпретації. Відношення  є відношенням часткового порядку на S.

відображення інтерпретації I : PsS{T, F}. Якщо   та I(A, ) = T, то I(A, ) = T. Це означає, що при підйомі по світах істинність атомарних формул не може перейти у фальш.

28. Інтуїціоністські числення Гільбертівського та Генценівського типу.

Аксіоматичні системи гільбертівського типу для інтуїціоністської ПЛ називаються інтуїціоністськими пропозиційними численнями (ІПЧ).

Множина правил виведення ІПЧ складається з єдиного правила:

МР) A, AB B – modus ponens.

Множина аксіом ІПЧ визначається такими схемами аксіом:

А1) A(BA) А2) (A(BC))((AB)(AC))

А3) A&BA А4) A&BB

А5) A(BA&B) А6) AAB

А7) BAB А8) (AC)(BC))(ABC)

А9) (AB)((AB)A) АI) A(AB)

Аксіоматичні системи генценівського типу для інтуїціоністської ПЛ називаються інтуїціоністськими секвенційними пропозиційними численнями (ІСПЧ).

Інтуїціоністською специфікацією назвемо слово вигляду  чи , де  – інтуїціоністський префікс, що є іменем світу, у якому специфікована формула має відповідне значення.

Інтуїціоністський префікс – це слово, символами якого є імена натуральних чисел.

Будемо вважати, що замкненість секвенції (суперечність) дає пара специфікованих формул вигляду _ та _. Це відповідає умові, що формула, істинна у світі , зберігає істинність у всіх його наступниках. Крім того, введемо такі додаткові умови замкненості секвенції:

– поява в секвенції пари формул _ та _;

– поява в секвенції пари формул _ та _.

Форми _, _, _&, _& секвенційних числень класичної логіки. Нехай така секвенція-виcновок  має вигляд _ AB, . виконання форми _ зводиться до побудови піддерева  з коренем , листами якого можуть бути довільні секвенції вигляду ₁, ..., _m, , де кожна формула _i має вигляд чи . _

Аксіоматичні системи гільбертівського типу для інтуїціоністської логіки предикатів називаються інтуїціоністськими численнями предикатів. Логічні аксіоми інтуїціоністського числення предикатів задаються схемами аксіом ІПЧ, до яких додаємо кванторні схеми:

АQ1) AxA;

АQ2) xAA.

Множина правил виведення інтуїціоністського числення предикатів складається з трьох правил:

МР) A, AB B – modus ponens;

П) AB  xAB, якщо x не вiльна у B,  правило -введення;

П) AB AxB, якщо x не вiльна в A,  правило -введення.

Аксіоматичні системи генценівського типу для інтуїціоністської логіки першого порядку називаються інтуїціоністськими секвенційними численнями предикатів.

Базовими секвенційними формами таких числень є базові секвенційні форми ІСПЧ, до яких додаються кванторні секвенційні форми:

_ за умови, що вільна змінна у{хA}.

_ .

_ .