В логике синтаксис — это все , что связано с формальными языками или формальными системами, безотносительно к какой-либо интерпретации или значению, придаваемому им. Синтаксис касается правил, используемых для построения или преобразования символов и слов языка, в отличие от семантики языка, которая касается его значения.
Символы , формулы , системы , теоремы и доказательства, выраженные на формальных языках, являются синтаксическими сущностями , свойства которых могут изучаться независимо от того, какое значение им может быть придано, и, по сути, не нуждаются в каком-либо придании.
Синтаксис обычно ассоциируется с правилами (или грамматикой), управляющими составлением текстов на формальном языке, которые представляют собой правильно построенные формулы формальной системы.
В информатике термин синтаксис относится к правилам, управляющим композицией правильно сформированных выражений в языке программирования . Как и в математической логике, он не зависит от семантики и интерпретации.
Символ — это идея , абстракция или концепция , маркерами которой могут быть знаки или метаязык знаков, которые образуют определенный шаблон. Символы формального языка не обязательно должны быть символами чего-либо. Например, существуют логические константы , которые не ссылаются на какую-либо идею, а скорее служат формой пунктуации в языке (например, скобки). Символ или строка символов могут включать в себя правильно сформированную формулу, если формулировка согласуется с правилами формирования языка. Символы формального языка должны быть способны быть определены без какой-либо ссылки на какую-либо их интерпретацию.
Формальный язык — это синтаксическая сущность, состоящая из набора конечных строк символов , которые являются его словами (обычно называемыми его правильно сформированными формулами ). Какие строки символов являются словами, определяется создателем языка, обычно путем указания набора правил формирования . Такой язык может быть определен без ссылки на какие-либо значения любого из его выражений; он может существовать до того, как ему будет назначена какая-либо интерпретация — то есть до того, как он обретет какое-либо значение.
Правила формирования — это точное описание того, какие строки символов являются правильно сформированными формулами формального языка. Это синоним набора строк в алфавите формального языка, которые составляют правильно сформированные формулы. Однако это не описывает их семантику (т. е . что они означают).
Предложение — это предложение , выражающее что-то истинное или ложное . Предложение онтологически определяется как идея , концепция или абстракция , чьими лексемами являются шаблоны символов , знаков, звуков или строк слов. [2] Предложения считаются синтаксическими сущностями, а также носителями истины .
Формальная теория — это набор предложений на формальном языке .
Формальная система (также называемая логическим исчислением или логической системой ) состоит из формального языка вместе с дедуктивным аппаратом (также называемым дедуктивной системой ). Дедуктивный аппарат может состоять из набора правил преобразования (также называемых правилами вывода ) или набора аксиом , или иметь и то, и другое. Формальная система используется для вывода одного выражения из одного или нескольких других выражений. Формальные системы, как и другие синтаксические сущности, могут быть определены без какой-либо интерпретации , данной им (например, как система арифметики).
Формула А является синтаксическим следствием [3] [4] [5] [6] в рамках некоторой формальной системы множества Г формул, если в формальной системе существует вывод А из множества Г.
Синтаксическая последовательность не зависит от какой-либо интерпретации формальной системы. [7]
Формальная система синтаксически полна [ 8] [9] [10] [11] (также дедуктивно полна , максимально полна , отрицательно полна или просто полна ) тогда и только тогда, когда для каждой формулы A языка системы либо A, либо ¬A является теоремой . В другом смысле формальная система синтаксически полна тогда и только тогда, когда никакая недоказуемая аксиома не может быть добавлена к ней в качестве аксиомы без внесения несоответствия . Истинностно-функциональная пропозициональная логика и логика предикатов первого порядка семантически полны, но не синтаксически полны (например, пропозициональное логическое утверждение, состоящее из одной переменной «a», не является теоремой, как и ее отрицание, но они не являются тавтологиями ). Теорема Гёделя о неполноте показывает, что никакая достаточно мощная рекурсивная система, такая как аксиомы Пеано , не может быть одновременно последовательной и полной.
Интерпретация формальной системы — это присвоение значений символам и истинностных значений предложениям формальной системы. Изучение интерпретаций называется формальной семантикой . Предоставление интерпретации синонимично построению модели . Интерпретация выражается на метаязыке , который сам по себе может быть формальным языком и, как таковой, является синтаксической сущностью .