Formeel systeem: verschil tussen versies

Verwijderde inhoud Toegevoegde inhoud
Japiobot (overleg | bijdragen)
linkfix's, Replaced: stellingstelling (2), met AWB
Regel 1:
Een '''formeel systeem''' is een combinatie van een [[formele taal]] en een [[verzameling (wiskunde)|verzameling]] [[afleidingsregel|afleidings-]] of transformatieregels of [[axioma]]'s die [[zin (taalkunde)|zin]]nen 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 [[uitdrukking (wiskunde)|uitdrukking]]en 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 [[stelling (logica)|stelling]]en.
 
Voorbeelden van formele systemen zijn de [[propositielogica|propositie-]], [[predicatenlogica|predicaten-]] en andere [[logica (wetenschap)|logica]]'s.
Regel 22:
{{Hoofdartikel|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 [[symbool|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 ====
Regel 36:
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 (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]]''.
 
==== Interpretatie van formele systemen ====