11.2: Багатосортована логіка

Last updated
Save as PDF

Page ID: 52775

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

Template:MathJaxZach

У логіці першого порядку змінні та квантори варіюються в межах однієї області. Але часто корисно мати кілька (нез'єднаних) доменів: наприклад, ви можете захотіти мати область чисел, область геометричних об'єктів, область функцій від чисел до чисел, область абелевих груп і так далі.

Багато відсортована логіка забезпечує такий вид фреймворку. Один починається зі списку «sorts» —« sort» об'єкта вказує на «домен», який він повинен населяти. Потім один має змінні та квантори для кожного сортування та (зазвичай) присудок ідентичності для кожного сорту. Функції та відносини також «набираються» видами об'єктів, які вони можуть приймати як аргументи. В іншому випадку дотримуються звичайних правил логіки першого порядку, при цьому версії кількісних правил повторюються для кожного сорту.

Наприклад, для вивчення міжнародних відносин ми можемо вибрати мову з двома видами об'єктів: громадяни Франції та громадяни Німеччини. У нас може бути унарне відношення, «п'є вино», для об'єктів першого сорту; інше унарне відношення, «їсть вурст», для об'єктів другого сорту; і двійкове відношення, «утворює багатонаціональну подружню пару», яка приймає два аргументи, де перший аргумент має перший сорт, а другий аргумент - другого сорту. Якщо ми використовуємо змінні\(a\)\(b\),\(c\) для діапазону над французькими громадянами і\(x\)\(y\),\(z\) щоб діапазон над німецькими громадянами, то\[\lforall{a}{\lforall{}{} x}[(\Atom{\Obj{MarriedTo}}{a,x} \lif (\Atom{\Obj{DrinksWine}}{a} \lor \lnot \Atom{\Obj{EatsWurst}}{x})]]\nonumber\] стверджує, що якщо будь-яка французька особа одружена з німець, або французька людина п'є вино або німець не їсть вурст.

Багато відсортована логіка може бути вбудована в логіку першого порядку природним чином, шляхом об'єднання всіх об'єктів багатьох відсортованих доменів разом в один домен першого порядку, використовуючи унарні символи предикатів для відстеження сортів, і релятивізації кількісних показників. Наприклад, мова першого порядку, що відповідає наведеному вище прикладу, матиме унарні присудкові символи «\(\Obj{German}\)» та «\(\Obj{French}\),» на додаток до інших описаних відносин, зі стиранням вимог до сортування. Сортований квантор\(\lforall{x}{A}\), де\(x\) є змінною німецького сорту, перекладається на\[\lforall{x}{(\Atom{\Obj{German}}{x} \lif A)}.\nonumber\] Ми повинні додати аксіоми, які гарантують, що сорти є окремими - наприклад,\(\lforall{x}{\lnot (\Atom{\Obj{German}}{x} \land \Atom{\Obj{French}}{x})}\) - а також аксіоми, які гарантують, що «п'є вино» тільки утримує об'єкти\(\Atom{\Obj{French}}{x}\), що задовольняють присудок і т.д. з цими умовностями і аксіомами неважко показати, що багатосортовані речення переводяться на пропозиції першого порядку, а багатосортовані похідні переводяться на похідні першого порядку. Крім того, багатосортовані структури «переводяться» на відповідні структури першого порядку і навпаки, тому ми також маємо теорему про повноту для багатосортованої логіки.