Formeel systeem: verschil tussen versies
Verwijderde inhoud Toegevoegde inhoud
Regel 34:
{{Hoofdartikel|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 [[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]]''.
| |||