Formeel systeem

Een formeel systeem is een combinatie van een formele taal en een verzameling afleidings- of transformatieregels of axioma's die zinnen in de formele taal omzetten in nieuwe zinnen. Formele systemen worden gebruikt als formeel bewijs. Vrijwel alle formele systemen maken gebruik van de axiomatische methode om nieuwe uitdrukkingen af te leiden uit oude die eerder in het systeem zijn uitgedrukt. De oude uitdrukkingen die worden verondersteld waar te zijn worden axioma's genoemd, de nieuwe uitdrukkingen heten stellingen.

Voorbeelden van formele systemen zijn de propositie-, predicaten- en andere logica's.

Een formeel systeem kan zelf worden bestudeerd aan de hand van zijn intrinsieke eigenschappen, of worden gebruikt als model om externe verschijnselen mee te beschrijven.

Beschrijving

In de wiskunde, logica en grammatica bestaan formele systemen uit de volgende elementen:

Een eindige reeks symbolen (bijvoorbeeld een alfabet) met behulp waarvan formules worden opgesteld.
Een grammatica die voorschrijft hoe goedgevormde formules worden opgesteld aan de hand van de alfabetische symbolen. Of een formule al dan niet goedgevormd is wordt meestal door middel van een procedure besloten.
Een reeks axioma's of een axioma-schema. waarin elk axioma de vorm heeft van een goedgevormde formule.
Een reeks afleidingsregels.

Een reeks is recursief als met behulp van algoritmen bepaalde eigenschappen van tevoren kunnen worden voorspeld.

Soorten formele systemen

Formele taal

Elk formeel systeem heeft zijn eigen formele taal (niet te verwarren met taal in de traditionele betekenis). Formele taal bestaat uit een eindige reeks primitieve symbolen, die op hun beurt opgesteld volgens formatieregels, die op hun beurt zijn afgeleid van eerdere axioma's. Hierdoor bestaat het formele systeem als geheel uit een eindige reeks primitieve symbolen, die zijn gevormd in overeenstemming met vaste uit eerder bepaalde axioma's. Een "formele taal" kan dus worden gedefinieerd als een eindige aaneenschakeling A van symbolen uit een alfabet α.

Formele grammatica

In zowel de computerwetenschap als de linguïstiek is een "formele grammatica" een grammatica die een nauwkeurige beschrijving van een formele of natuurlijke taal geeft. Dit gebeurt in het geval van formele talen aan de hand van 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.

Formeel bewijs

Met "formeel bewijs" worden aaneenschakelingen van strings e.d. bedoeld. Om als deel van een formeel bewijs te kunnen dienen moet een string een axioma of een stelling zijn (zie boven). In de filosofie van de wiskunde wordt ervan uitgegaan dat de hele wiskunde gebaseerd is op het genereren van formeel bewijs. David Hilbert bedacht in dit verband de metawiskunde om binnen de wiskunde zelf formele wiskundige systemen te beschrijven. Een taal die wordt gebruikt om een formeel systeem te beschrijven heet een metataal. Een metataal kan een gewone natuurlijke taal zijn, of een taal die zelf althans gedeeltelijk formeel is opgesteld, bijvoorbeeld computertaal. De taal die deel uitmaakt van het formele systeem dat onderzocht wordt en bijgevolg zelf het onderwerp van studie is heet in dit verband de objecttaal.

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 en van axioma. Er is echter geen sprake van een 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.

Interpretatie van formele systemen

Een formele interpretatie van een formele taal houdt het toekennen van betekenissen aan de symbolen en waarheidswaarden aan de zinnen van het formele systeem in. Formele semantiek (niet te verwarren met de semantiek als onderdeel van de taalkunde) behelst de studie van formele interpretatie. Het geven van een interpretatie komt ongeveer overeen met het aanbrengen van een structuur in wiskundig-logische zin.

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