Кіріспе

Тілдің символдары мен сөздерін құруға немесе өзгертуге арналған ережелер. Логикада синтаксис – оларға берілген түсіндіру немесе мағынаға қарамастан, формалды тілдерге немесе формалды жүйелерге қатысты кез келген нәрсе. Синтаксис тілдің мағынасын зерттейтін семантикасымен салыстырғанда, тілдің символдары мен сөздерін құру немесе өзгерту үшін қолданылатын ережелермен айналысады. Формалды тілдерде қолданылатын символдар, формулалар, жүйелер, теоремалар және дәлелдер – синтаксистік бірліктер болып табылады, олардың қасиеттерін оларға берілген кез келген мағынаға қарамастан зерттеуге болады, тіпті оларға ешқандай мағына берілмеуі де мүмкін. Синтаксис әдетте формалды тілдегі мәтіндердің құрамын анықтайтын ережелермен (немесе грамматикамен) байланысты, олар формалды жүйенің дұрыс құрылған формулаларын құрайды. Компьютер ғылымында синтаксис термині бағдарламалау тіліндегі дұрыс құрылған өрнектердің құрамын анықтайтын ережелерді білдіреді. Математикалық логикадағыдай, ол семантикадан және интерпретациядан тәуелсіз.

Таңбалар

Символ – идея, абстракция немесе ұғым, оның белгілері белгілер немесе белгілі бір үлгі құрайтын белгілердің метатілі болуы мүмкін. Формалды тілдің символдары міндетті түрде ешбір нәрсенің символы болмауы керек. Мысалы, ешқандай идеяға сілтеме жасай бермейтін, бірақ тілдегі пунктуацияның бір түрі ретінде қызмет ететін логикалық тұрақтылар бар (мысалы, жақшалар). Егер формула тілдің құрастыру ережелеріне сәйкес келсе, символ немесе символдар тізбегі дұрыс құрылған формуланы құрауы мүмкін. Формалды тілдің символдары олардың интерпретациясына сілтеме жасамай анықтала алуы керек.

Ресми тіл

Ресми тіл – бұл символдардың шекті тізбектерінен тұратын синтаксистік құрылым, олар оның сөздері (көбінесе жақсы қалыптасқан формулалар деп аталады). Символдар тізбегінің қайсысы сөз болып саналатынын тілді жасаушы анықтайды, әдетте қалыптасу ережелері жиынтығын белгілеп. Мұндай тіл оның кез келген өрнегінің мағынасын ескермей анықталуы мүмкін; ол оған қандай да бір түсіндірме берілгенге дейін, яғни мағынаға ие болмас бұрын өмірге келуі мүмкін.

Құрастыру ережесі

Құрылыс ережелері – формальды тілдің дұрыс құрылған формулаларын құрайтын символдар тізбегін нақты сипаттайды. Бұл, формальды тіл әліпбиімен құрылған дұрыс құрылған формулалар жиынтығымен теңдес. Дегенмен, ол олардың семантикасын (яғни, нені білдіретінін) сипаттамайды.

Ұсыныстар

Пропозиция – шындық немесе жалғандықты білдіретін сөйлем. Пропозиция онтологиялық тұрғыдан идея, түсінік немесе абстракция ретінде қарастырылады, оның нақты көріністері – символдардың, белгілердің, дыбыстардың немесе сөздердің тізбектері болып табылады. Пропозициялар синтаксистік бірліктер және сонымен қатар шындықты білдірушілер саналады.

Формалды теориялар

Формалды теория — формалды тілдегі сөйлемдер жиынтығы.

Ресми жүйелер

Формалды жүйе (логикалық есептеу немесе логикалық жүйе деп те аталады) формалды тіл мен дедуктивті аппараттан (дедуктивті жүйе деп те аталады) тұрады. Дедуктивті аппарат трансформация ережелерінің (тұжырым ережелері деп те аталады) жиынтығынан, аксиомалар жиынтығынан немесе олардың екеуінен де құралуы мүмкін. Формалды жүйе бір немесе бірнеше өрнектерден басқа бір өрнекті шығару үшін қолданылады. Формалды жүйелер, басқа синтаксистік құрылымдар сияқты, ешқандай түсіндірмесіз анықталуы мүмкін (мысалы, арифметика жүйесі ретінде).

Формальды жүйедегі синтаксистік салдары

A формуласы Г формулалар жиынының белгілі бір формальды жүйеде синтаксистік салдары болып есептеледі, егер Г жиынынан A формуласы осы формальды жүйеде дәлелденсе.

Синтаксистік салдар формальды жүйенің ешқандай интерпретациясына тәуелді емес.

Формалды жүйенің синтаксистік толықтығы

Формалды жүйе синтаксистік жағынан толық (сондай-ақ дедуктивтік толықтық, максималды толықтық, жоққа шығару толықтығы немесе жай ғана толықтық) – егер жүйе тілінің кез келген формуласы А үшін, А немесе ¬А теорема болса. Басқаша айтқанда, формалды жүйе синтаксистік жағынан толық болады, егер оған дәлелдемесі жоқ аксиоманы аксиома ретінде қосса, қанағаттандырылмаушылық тудырмаса. Шындық функциялық мәлімдемелік логика және бірінші реттік предикаттық логика семантикалық жағынан толық, бірақ синтаксистік жағынан толық емес (мысалы, "а" бір өрнектен тұратын мәлімдемелік логикалық тұжырым теорема емес, оның жоғы да емес, бірақ бұл таутологиялар емес). Гёдельдің толық еместік туралы теоремасы, Пиано аксиомалары сияқты, жеткілікті күшті рекурсивті жүйелердің бірізді де толық бола алмайтынын көрсетеді.

Түсіндірме

Ресми жүйені түсіндіру – жүйенің символдарына мағыналар мен жүйенің өзінің сөйлемдеріне шындық мәндерін тағайындау. Түсіндірілімдерді зерттеу формальды семантика деп аталады. Түсіндіру беру модель құрумен мағыналас. Түсіндіру метатілде беріледі, ол өзі формальды тіл болуы мүмкін, демек, өзі синтаксистік құрылым болып табылады.