Формален Систем

Формалниот систем се користи за изведување на израз од еден или повеќе други изрази претходно наведени во системот. Овие изрази се нарекуваат аксиоми (кај оние кои однапред се земаат за вистинити), или пак теореми (кај оние кои се изведени). Еден формален систем може да се формулира и изучува заради неговите сопствени својства, или пак за опишување (т.е. моделирање) на надворешни појави.

Секој формален систем има формален јазик, кој е составен од примитивни симболи (знаци). Овие симболи дејствуваат врз основа на извесни правила на создавање и се развиваат по инференција (заклучок) од множество аксиоми. Затоа системот се состои од ред формули изградени по пат на конечни комбинации на примитивните симбол—комбинации кои пак се формирани од аксиомите врз основа на наведените правила.

Формалните системи во математиката се состојат од следниве елементи:

1. Конечно множество симболи (т.е. азбука), кои се користат за составување на формули (т.е. конечни низи на симболи).
2. Граматика, која ни кажува како добро-образуваните формули се составени од симболите од азбуката.

За да се реши дали формулата е добро-образувана или не треба да се има извесна процедура за решавање.

1. Множество аксиоми или аксиоматски шеми:

секој аксиом мора да претставува добро-образувана формула.

1. Множество правило на инференција.

За еден формален систем се вели дека е рекурзивен (т.е. делотворен) ако множеството аксиоми и множеството правила на инференција претставуваат нерешителни множества или полурешителни множества, според контекстот.

Теоретичарите го користат поимот формализам како приближен синоним за формален систем но овој поим се користи и за конкретен стил на нотација (запишување).

Формален јазик

Формален јазик е множество (конечни) низи А од утврдена азбука α.

Формална граматика

Во информатиката и лингвистиката, формална граматика е прецизниот опис на еден формален јазик: множество низи. Двете главни категории на формална граматика се генеративните граматики, кои се множество правила за генерирање на јазичните низи, и аналитичките граматики, што претставуваат множество правила за анализирање на низите со цел да се одреди дали низата му припаѓа на јазикот. Накратко, аналитичката граматика нè учи како да распознаеме кои низи му припаѓаат на множеството, додека генеративната граматика нè учи како да ги пишуваме само тие низи во множеството.

Формални докази

Формалниот доказ е ред од низи. За низата да се смета за дел од доказот, таа може да биде аксиома или пак производ на примената на правилото на инференција врз претходни низи во редот на докази. Последната низа од редот се нарекува теорема.

Гледиштето дека математиката не е ништо повеќе од генерирање на формални докази се нарекува формализам. Давид Хилберт ја основал метаматематиката како дисциплина која има за цел да ги обработува формалните системи. Секој јазик кој се користи за разгледување на еден формален систем се нарекува метајазик. Метајазикот може да биде само обичен природен јазик, или самиот може да биде делумно формализиран, но во секој случај тој не е толку формализиран колку формалниот јазик на формалниот систем кој се разгледува, кој пак тогаш се нарекува објектен јазик, т.е. „објектот“ на дадената расправа (разгледување).

Откога ќе се постави формален систем, тогаш можеме да дефинираме множество теореми кои можат да се докажат во рамките на формалниот систем. Ова множество се состои од сите низи кои можат да се докажат. Така, сите аксиоми се сметаат за теореми. За разлика од граматиката за низи, не постои гаранција дека ќе има процедура за решавање дали една низа е теорема или не. Поимот теорема сам по себе не значи исто што и теореми за формалниот систем, кои пак, за да не дојде до забуна, обично се нарекуваат метатеореми.

Формални толкувања

Формалното толкување (интерпретација) на еден формален систем е давање (назначување) на значења на симболите, и вистинитосни вредности на речениците на тој формален систем. Изучувањето на формалните толкувања се нарекува формална семантика. Давање на толкување е синонимно со составување на модел.

Толкуван формален систем е формален јазик за кој се дадени и синтаксичките правила на дедукција и и семантичките правила на толкување. Толкуваниот формален систем може да се изрази како наредениот четворократник <α,${\displaystyle {\mathcal {I}}}$ ,${\displaystyle {\mathcal {D}}}$ d,${\displaystyle {\mathcal {D}}}$ >. Додека, во случај на екстензивните метајазици, ${\displaystyle {\mathcal {D}}}$  е односот помеѓу припишаната вредност на речениците во јазикот, во случај на интензивни метајазици, ова е однос помеѓу дознаките, т.е., односот помеѓу еден израз и неговата интензија (намера); и каде ${\displaystyle {\mathcal {D}}}$ d е односот на директната изведливост. Во сеопфатна смисла, овој однос се смета за таков што примитивните реченици на формалниот систем се сметаат за диреткно изведливи од празното множество реченици. Тука се наведуваат аксиомите, некои слични на оние наведени за формалниот систем, а други пак како оние за толкуван формален јазик. Обично сакаме ${\displaystyle {\mathcal {D}}}$ d да ја зачувува вистинитосната вредност (т.е. секоја реченица директно изведлива од вистинита реченица е самата вистинита), меѓутоа во ваков систем може да се зачуваат и други модалитети. За ови цели можеме да формулираме аксиома употребувајќи го поимот „вистина“. За секое ${\displaystyle {\mathcal {I}}}$ _i1,...,${\displaystyle {\mathcal {I}}}$ _in, ${\displaystyle {\mathcal {I}}}$ _j, p₁,...,p_n,q ако ${\displaystyle {\mathcal {D}}}$ d(${\displaystyle {\mathcal {I}}}$ _j,{${\displaystyle {\mathcal {I}}}$ _i1,...,${\displaystyle {\mathcal {I}}}$ _in}), ${\displaystyle {\mathcal {D}}}$ (${\displaystyle {\mathcal {I}}}$ _i1,p₁) и ... и ${\displaystyle {\mathcal {D}}}$ (${\displaystyle {\mathcal {I}}}$ _in,p_n) и p₁ и ... и p_n, q.

За толкуваните формални системи постои и алтернатива, што се поексплицитни дефиниции во кои се работи со знаци d, или пак и знаци d и знаци D, аналогни на оние дадени за толкуваните формални јазици.

• Raymond M. Smullyan, Theory of Formal Systems: Annals of Mathematics Studies, Princeton University Press (1 април 1961) 156 стр. ISBN 0-691-08047-X
• S. C. Kleene, 1967. Mathematical Logic Препечатено од Dover, 2002. ISBN 0-486-42533-9

• Encyclopædia Britannica, Формален систем дефиниција на Енциклопедија Британика 2007.
• Кристер Бломквист, Вовед во формалните системи Архивирано на 16 февруари 2008 г., 1997.
• Што е тоа формален систем?: цитати од `Artificial Intelligence: The Very Idea' од Џон Хејџленд (1985), стр. 48-64.
• Хајнрих Хере, Формален јазик и системи Архивирано на 19 јули 2011 г., 1997.
• Питер Сабер, Формални системи и машини: Изоморфизам Архивирано на 24 мај 2011 г., 1997.