У ній розрізняють синтаксис і семантику.
На синтаксичному рівні дають визначення й аналіз суто формальних відношень між символами в межах певної системи. До синтаксису належать: алфавіт; правила побудови формул із символів алфавіту; правила виведення одних формул із інших (перетворення одних формул на інші).
1. Алфавіт (від назви перших двох букв грецького алфавіту: альфа та бета; новогрец. - віта) - кінцева сукупність штучно створених символів, за допомогою яких твориться певна формально-логічна система.
2. Правила побудови формул із символів алфавіту - метависловлювання про те, як із символів алфавіту штучної мови створити формулу, і як із простих формул, побудувати нову складну формулу.
3. В межах певної формально-логічної системи розрізняють формальне виведення та формальне доведення, що здійснюють за певними правилами.
Формальне виведення (формальна вивідність) - виведення, яке означає таке відношення логічного слідування, коли із формули виду А виводять формулу виду В, і лише з того випливає: якщо А - істинне, то В - істинна. Таке відношення слідування називається відношенням дедуктивного виведення, формальний вираз якого А - В, де і--символ дедуктивного виведення.
Формальне доведення - доведення, яке має логічну форму виведення формули виду А, яка є теоремою, із формул виду А,, А.,,... А , які є аксіомами за фіксованими правилами виведення. Якщо формулу виду А виводять із формул виду А., А2, ... Ая, то її називають доказовою формулою. Формальне доведення зображають так: (Аґ А2,... Ап) ь А, де А,, А2,... Ап - засновки, А - висновок, а і--символ дедуктивного виведення.
Правила дедуктивного виведення - правила дедуктивного умовиводу, які визначають строге (необхідне) виведення певного висловлювання (висновку) з вихідних висловлювань (засновків) на підставі логічних законів.
Прикладами правил дедуктивного виведення є правила введення й усунення пропозиційних зв'язок (логічних постійних) (див. 4.2.1), правило дедукції - модус поненс тощо. На підставі правил виведення визначають, чи є формула певного виду вивідною чи невивідною, доказовою або недоказовою.
Вивідна формула - формула виду А, яку виводять за допомогою правил виведення зі скінченної послідовності формул виду А1,А2,... Ая, кожна з яких є тавтологією і належить до множинності формул системи 5, відповідно, невивідною є формула, яку не виводять з цих формул.
Символічний запис (А,, А2,Ап) н А засвідчує, що формулу А виводять з аксіом А,, А2.....Ап.
Доказовою називають формулу, яка має формальне доведення за правилами логічного виведення в межах певної системи 5, а недоказовою є формула, яка за правилами логічного виведення не є формально доведеною в межах певної системи 5'.
Семантика - інтерпретація символів певної системи та надання їм істиннісного значення. Для інтерпретації створюють семантичну модель, яка приписує смисл символам, які в сукупності створюють певну формально-логічну систему. Таких інтерпретованих моделей може бути побудовано багато. На семантичному рівні визначають також основні семантичні різновиди формул. Оскільки у побудованих логіками та математиками формально-логічних системах створено багато формул, то їх поділяють на такі види: тотожно-істинні формули, тотожно-хибні формули, нейтральні формули.
Тотожно-істинна формула має значення істинності ("істина") для всіх значень змінних, які входять до структури формули, її ще називають тавтологією (термін Л. Вітгенштайна), загальнозначущою формулою, логічним законом.
Тотожно-хибна формула має значення хибності ("хибність") при всіх значеннях змінних, що входять до структури формули.
Нейтральна формула - формула, яка не є ні тотожно-істинною, ні тотожно-хибною в межах певної формально-логічної системи S.
Установлення того, що деяка формула певного виду тотожно-істивна, тотожно-хибна або нейтральна, здійснюють за допомогою специфічних методів. Одним із таких методів на семантичному рівні є метод побудови таблиць істинності, метод побудови аналітичних таблиць тощо. На синтаксичному рівні для цього використовують метод зведення формул до їх кон'юнктивного або диз'юнктивного виду (про це йтиметься в 4.2.1).
Інтерпретація формально-логічної системи (лат. interpreta-tio- роз'яснення, тлумачення) - 1) роз'яснення значення логічних символів за правилами визначення їхньої істинності та правилами позначення пропозиційних змінних на підставі принципів несуперечності та повноти; 2) побудова семантичної моделі певного типу формально-логічної системи (формалізму) для певної предметної галузі. Розрізняють внутрішню та зовнішню інтерпретацію формально-логічної системи. Внутрішня інтерпретація в контексті мета логічного аналізу формально-логічних систем означає семантичну модель, що будується з метою розкриття значення символів формалізованої мови та надання істиннісного значення висловлюванням у межах певної формально-логічної системи. Інтерпретація має таку послідовність: у межах певної формальної системи S визначають абстрактний об'єкт (предмет, властивість, відношення), який позначають певним символом. Сукупність таких об'єктів називають полем інтерпретації. Кожне висловлювання, що стосується певного об'єкта в системі S, набуває значення істинності ("істина" або "хибність"). Система S, яку вибирають для інтерпретації, називається семантичною моделлю. Для кожної конкретної формально-логічної системи може бути побудована семантична модель, тобто її інтерпретація.
Особливості формально-логічних систем
4.2. Класична символічна логіка
4.2.1. Логіка висловлювань
Рівносильні формули логіки висловлювань
Відношення логічного слідування між формулами
Металогічна оцінка логіки висловлювань
4.2.2. Логіка предикатів
Рівносильні формули логіки предикатів
Заперечення висловлювань з кванторами