Формальна семантика

Формальна семантика- дисципліна, що вивчає семантику (інтерпретації) формальних та природних мов шляхом їх формального опису в математичних термінах.

Формальна мова може бути задана без будь-якої інтерпретації. Це досягається завданням безлічі символів (також званого алфавітом) та безлічі правил виведення (також званого формальною граматикою), які визначають, які рядки символів є правильно побудованими формулами. При додаванні правил перетворення та прийнятті деяких пропозицій за аксіоми (що разом називається дедуктивною системою), формується логічна система. Інтерпретація — завдання сенсу її символам і значень істинності її пропозиціям.

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

До становлення сучасної логіки, в «Органоні» Аристотеля, а саме у роботі «Про тлумачення» було задано основи розуміння та значення логіки. Введення кванторів мало вирішити проблему спільності множин, не вирішувану рамках суб'єктно-предикатного аналізу Аристотеля, хоча у логіці термів з'являється новий інтерес, саме спроби побудувати обчислення на кшталт силогістики Аристотеля, але використовуючи властивості спільності кванторів із сучасної логіки.

Основними сучасними підходами до семантики для формальних мов є:

Теоретико-модельна семантика, архетип семантики теорії істинності Альфреда Тарського, що ґрунтується на його Т-схемі, є однією з ключових концепцій модельної теорії. Це один із найпоширеніших підходів. Основна його ідея в тому, що зміст різних частин твердження задаються всілякими способами рекурсивного завдання групи функцій інтерпретації, що відображають пропозиції на деякі задані математичні множини. Так, інтерпретація логіки предикатів першого порядку задається відображенням термів в універсум, і відображення предикатів значення істинності «істина» і «брехня». На модельно-теоретичній семантиці заснований підхід у теорії сенсу під назвою семантика умовної Істини, який вперше був запропонований Дональдом Девідсоном. Семантика Крипке, по суті, вносить деякі доповнення до семантики Тарського.
Теоретико-доказова семантика [en] пов'язує сенс тверджень із ролями, які вони грають у міркуванні. Герхард Генцен, Даг Правіц (швед.Dag Prawitz) та Майкл Даммет вважаються засновниками цього підходу. Нею сильно вплинула пізня філософія Людвіга Вітгенштейна, особливо його афоризм «сенс — це застосування».
Семантика значень істинності [en] (також відома якпідстановна квантифікація) була запропонована Рут Маркус (англ.Ruth Barcan Marcus) для модальних логік на початку 1960-х і потім розвинена в працях Дана (Michael Dunn), Белнапа (англ.Nuel Belnap) і Леблана (Hugues Leblanc) як стандартна логіка першого порядку. Джеймс Гарсон (англ.James Garson) отримав деякі результати в областях адекватності інтенсіональних логік, забезпечених такою семантикою. Умови істинності квантифікованих формул задаються виключно у термінах істинності, безвикористання множин (звідси і назва).
Теоретико-ігрова семантика[en] нещодавно була відроджена Яакко Хінтіккой для логік (кінцевої) частково покритої квантифікації, які спочатку досліджувалися Леоном Хенкіним.
Імовірнісна семантика - узагальнення семантики значень істинності, створене Філдом (Hartry Field).

Лінгвісти рідко застосовували формальні семантики доти, доки Річард Монтегю не показав як можна сприймати англійську (або будь-яку іншу природну мову) як формальну мову. Його внесок у лінгвістичну семантику, відомий як граматика Монтегю, є основою для того, що лінгвісти називаютьформальною семантикою.