Метатеорема про дедукцію

Вперше ця теорема була сформульована у 1930 р. Ер- браном. Тому іноді її називають теоремою Ербрана. Але як загальний методологічний принцип, що характеризує аксіоматично-дедуктивні системи, вона з’явилася у А.

Вивідність формули на підставі метатеореми про дедукцію визначається трьома особливостями, які ви­ражаються у вигляді таких правил:

а) із довільних формул А1,... А_п вивідна кожна із цих формул:

б) із довільних формул А1,... А_п вивідна кожна форму­ла, яка є вивідною в S² :

в) якщо із довільних формул А1,... А_п вивідна формула виду МР, то із них також вивідний і консеквент цього модусу.

Ці особливості вивідності (дедукції) на підставі метатео­реми про дедукцію стають очевидними на основі таких се­мантичних міркувань:

1) Особливість а) виражає властивість рефлексивності слідування:

2) Особливість б) виражає властивість істинних (вивід­

них) формул. «Кожна істинна формула розглядається як консеквент(логічно істинної імплікації) з до­

вільним антецедентом».

3) Особливість в) фіксується таким способом:

Перейдемо до доведення метатеореми про дедукцію:

Розглянуті варіанти доведення метатеореми про де­дукцію показують, що вона описує одну із фундаментали­зм а. Є. Конверський. Логіка

них властивостей числень, суть якої полягає у тому, що доведена формула із множини засновків, з’єднуючись че­рез імплікацію з будь-яким із цих засновків чи їх комбі­нацією, теж буде доведеною.

3.