Formeel systeem: verschil tussen versies

Een reeks is [[recursieve reeks|recursief]] als met behulp van [[algoritme]]n bepaalde eigenschappen van te vorentevoren kunnen worden voorspeld.

In zowel de [[computerwetenschap]] als de [[linguïstiek]] is een "formele grammatica" een grammatica die een nauwkeurige beschrijving van een formele of [[natuurlijke taal|natuurlijke]] taal geeft. Dit gebeurt in het geval van formele talen aan de hand van [[String (informatica)|strings]]. Formele grammatica's kunnen verder worden onderverdeeld in twee categorieën. [[Generatieve grammatica]]'s specificeren nader hoe strings of vergelijkbare reeksen in een formele taal kunnen worden voortgebracht (bijvoorbeeld door ze op te schrijven), terwijl [[analytische grammatica]]'s aangeven hoe een string als zodanig kan worden geanalyseerd en herkend om uit te maken of een string werkelijk tot de taal behoort.

Aan de hand van een formeel systeem kan een reeks stellingen worden opgesteld, die binnen het formele systeem zelf bewezen kunnen worden. Een dergelijke reeks bestaat uit alle strings waarvoor formeel bewijs bestaat. Alle strings hebben met andere woorden in dit verband tegelijkertijd de functie van [[stelling (logica)|stelling]] en van axioma. Er is echter geen sprake van een [[beslisbaarheid (logica)|beslisprocedure]] met behulp waarvan bepaald kan worden of een string wel of geen stelling is, zoals in formele grammatica het geval is. Het begrip stelling dient verder in dit verband te worden onderscheiden van ''[[metastelling]]''.

Een ''geïnterpreteerd formeel systeem'' is een formele taal waarvoor zowel [[deductief systeem|deductieve]] als semantische regels met betrekking tot de logische interpretatie gelden. Een dergelijk systeem kan worden geschreven als een [[quadrupel]]: <math><\alpha,\mathcal{I},\mathcal{D} d,\mathcal{D}></math>. In geval van [[extensie (predicaatlogica)|extensionele]] metataal geeft <math>\mathcal{D}</math> de [[valuatie (logica)|valuatie]] voor de zinnen van de taal weer, in het geval van [[intensie|intensionele]] metataal staat de relatie tussen uitdrukking en intensie centraal. <math>\mathcal{D} d</math> is de relatie van het rechtstreekse formele bewijs, waarbij de primitieve zinnen van het formele systeem worden beschouwd als rechtstreeks afleidbaar. Gewoonlijk wordt <math>\mathcal{D} d</math> beschouwd als [[waarheidsconservatief]], wat wil zeggen dat elke zin die rechtstreeks van een zin die waar is wordt kan worden afgeleid zelf ook waar is. In een dergelijk systeem kunnen echter ook andere [[modale logica|modaliteiten]] worden behouden.