Промежуточная логика

В математической логике, суперинтуиционистская логика - это логика высказываний, расширяющая интуиционистскую логику. Классическая логика - сильнейшая последовательная суперинтуиционистская логика; таким образом, непротиворечивые суперинтуиционистские логики называются промежуточными логиками (логики занимают промежуточное положение между интуиционистской логикой и классической логикой).

• 1 Определение
• 2 Свойства и примеры
• 3 Семантика
• 4 Связь с модальной логикой
• 5 См. Также
• 6 Ссылки

Суперинтуиционистская логика - это набор L пропозициональных формул в счетном наборе переменных p i, удовлетворяющие следующим свойствам:

1. все аксиомы интуиционистской логики принадлежат L;

2. если F и G - формулы такие, что F и F → ​​G принадлежат L, то G также принадлежит L (замыкание согласно modus ponens );

3. если F (p 1, p 2,..., p n) является формулой L, а G 1, G 2,..., G n - любые формулы, тогда F (G 1, G 2,..., G n) принадлежит L ( закрытие при подстановке).

Такая логика является промежуточной, если, кроме того,

4. L не является набором всех формул.

Существует континуум различных промежуточных логик. Конкретные промежуточные логики часто конструируются путем добавления одной или нескольких аксиом к интуиционистской логике или семантического описания. Примеры промежуточных логик включают:

• интуиционистскую логику (IPC, Int, IL, H)
• классическая логика (CPC, Cl, CL): IPC + p ∨ ¬p = IPC + ¬¬p → p = IPC + ((p → q) → p) → p
• логика слабого исключенного среднего (KC, логика, логика Де Моргана ): МПК + ¬¬ p ∨ ¬p
• логика Гёделя - Даммета (LC, G): IPC + (p → q) ∨ (q → p)
• Kreisel - Логика Патнэма (КП ): IPC + (¬p → (q ∨ r)) → ((¬p → q) ∨ (¬ p → r))
• логика конечных проблем (LM, ML): определяется семантически как логика всех фреймов формы $⟨P\; (X)\; \setminus \; \{\; X\},\; \subseteq ⟩\; \{\backslash \; displaystyle\; \backslash \; langle\; \{\backslash \; mathcal\; \{P\}\}\; (X)\; \backslash \; setminus\; \backslash \; \{X\; \backslash \},\; \backslash \; substeq\; \backslash \; rangle\}$для конечных множеств X ( «Булевы гиперкубы без вершины»), по состоянию на 2015 год не известно, что они рекурсивно аксиоматизируемые
• реализуемость логика
• Логика Скотта (SL ): IPC + ((¬¬p → p) → (p ∨ ¬p)) → (¬¬p ∨ ¬p)
• Логика Сметанича (SmL ): IPC + (¬q → p) → (((p → q) → p) → p)
• логики ограниченной мощности (BCn):
• логика ограниченной ширины, также известная как логика ограниченных антицепей (BWn, BAn): $IPC\; +\; \bigvee \; i\; =\; 0\; n\; (\bigwedge \; j\; \ne \; ipj\; \to \; pi)\; \{\backslash \; displaystyle\; \backslash \; textstyle\; \backslash \; mathbf\; \{IPC\}\; +\; \backslash \; bigvee\; \_\; \{i\; =\; 0\}\; ^\; \{n\}\; \{\backslash \; bigl\; (\; \}\; \backslash \; bigwedge\; \_\; \{j\; \backslash \; neq\; i\}\; p\_\; \{j\}\; \backslash \; to\; p\_\; \{i\}\; \{\backslash \; bigr)\}\}$
• логики ограниченной глубины (BDn): IPC + p n ∨ (p n → (p n − 1 ∨ (p n − 1 →... → (p 2 ∨ (p 2 → (p 1 ∨ ¬p 1)))...)))
• логика ограниченная ширина верха (BTW n):
• логика ограниченного ветвления (Tn, BBn): $IPC\; +\; \bigwedge \; i\; =\; 0\; n\; (\; (пи\; \to \; \bigvee \; j\; \ne \; ipj)\; \to \; \bigvee \; j\; \ne \; ipj)\; \to \; \bigvee \; я\; =\; 0\; npi\; \{\backslash \; displaystyle\; \backslash \; textstyle\; \backslash \; mathbf\; \{IPC\}\; +\; \backslash \; bigwedge\; \_\; \{i\; =\; 0\}\; ^\; \{n\}\; \{\backslash \; bigl\; (\}\; \{\backslash \; bigl\; (\}\; p\_\; \{i\}\; \backslash \; to\; \backslash \; bigvee\; \_\; \{j\; \backslash \; neq\; i\}\; p\_\; \{j\}\; \{\backslash \; bigr)\}\; \backslash \; to\; \backslash \; bigvee\; \_\; \{j\; \backslash \; neq\; i\}\; p\_\; \{j\}\; \{\backslash \; bigr)\}\; \backslash \; to\; \backslash \; bigvee\; \_\; \{i\; =\; 0\}\; ^\; \{n\}\; p\_\; \{i\}\}$
• n-значная логика Гёделя (Gn): LC+ BCn − 1 = LC+ BDn − 1

Форма суперинтуиционистской или промежуточной логики полная решетка с интуиционистской логикой в ​​качестве дна и противоречивой логикой (в случае суперинтуиционистской логики) или классической логикой (в случае промежуточных логик) в качестве вершины. Классическая логика - единственный коатом в решетке суперинтуиционистской логики; решетка промежуточных логик также имеет уникальный коатом, а именно SmL .

Инструменты для изучения промежуточных логик аналогичны инструментам, используемым для интуиционистской логики, таким как семантика Крипке. Например, логика Гёделя – Даммета имеет простую семантическую характеристику в терминах общих порядков.

Учитывая алгебру Гейтинга H, набор пропозициональных формул, которые действительны в H, - это промежуточная логика. И наоборот, исходя из промежуточной логики, можно построить ее алгебру Линденбаума, которая является алгеброй Гейтинга.

Интуиционистский фрейм Крипке F - это частично упорядоченный набор, а модель Крипке M - фрейм Крипке с такой оценкой, что $\{x\; \mid \; M,\; x\; ⊩\; p\}\; \{\backslash \; displaystyle\; \backslash \; \{x\; \backslash \; mid\; M,\; x\; \backslash \; Vdash\; p\; \backslash \}\}$является верхним подмножеством F. Набор пропозициональных формул, которые действительны в F это промежуточная логика. Учитывая промежуточную логику L, можно построить модель Крипке M так, чтобы логика M была L (эта конструкция называется канонической моделью). Фрейм Крипке с этим свойством может не существовать, но общий фрейм существует всегда.

Пусть A - пропозициональная формула. Перевод A по Гёделю – Тарскому определяется рекурсивно следующим образом:

• $T\; (pn)\; =\; ◻\; pn\; \{\backslash \; displaystyle\; T\; (p\_\; \{n\})\; =\; \backslash \; Box\; p\_\; \{n\}\}$
• $T\; (\neg \; A)\; =\; ◻\; \neg \; T\; (A)\; \{\backslash \; displaystyle\; T\; (\backslash \; neg\; A)\; =\; \backslash \; Box\; \backslash \; neg\; T\; (A)\}$
• $T\; (A\; \wedge \; B)\; =\; T\; (A)\; \wedge \; T\; (B)\; \{\backslash \; displaystyle\; T\; (A\; \backslash \; земля\; B)\; знак\; равно\; T\; (A)\; \backslash \; земля\; T\; (B)\}$
• $T\; (A\; \vee \; B)\; =\; T\; (A)\; \vee \; T\; (B)\; \{\backslash \; displaystyle\; T\; (A\; \backslash \; vee\; B)\; =\; T\; (A)\; \backslash \; vee\; T\; (B)\}$
• $T\; (A\; \to \; B)\; =\; ◻\; (T\; (A)\; \to \; T\; (B))\; \{\backslash \; displaystyle\; T\; (A\; \backslash \; to\; B)\; =\; \backslash \; Box\; (T\; (A)\; \backslash \; to\; T\; (B))\}$

Если M является модальной логикой, расширяющей S4, то ρM = {A | T (A) ∈ M} - суперинтуиционистская логика, а M называется модальным компаньоном ρM. В частности:

• IPC = ρ S4
• KC= ρ S4.2
• LC= ρ S4.3
• CPC = ρ S5

для любой промежуточной логики L существует много модальных логик M таких, что L = ρM.

• Список логических систем

1. ^«Промежуточная логика». Энциклопедия математики. Проверено 19 августа 2017 года.
2. ^Constructive Logic and the Medvedev Lattice, Sebastiaan A. Terwijn, Notre Dame J. Formal Logic, Volume 47, Number 1 (2006), 73-82.

• Тосио Умедзава. О логике, промежуточной между интуиционистской и классической логикой предикатов. Journal of Symbolic Logic, 24 (2): 141–153, июнь 1959 г.
• Александр Чагров, Михаил Захарящев. Модальная логика. Oxford University Press, 1997.