Formeel bewijs

In de formele wetenschap is een formeel bewijs een eindige reeks proposities (goedgevormde formules in formele taal) binnen het kader van de beschrijving van formele systemen waarbij elke propositie door middel van afleidingsregels uit voorafgaande proposities of axiomas kan worden afgeleid. De uiteindelijke propositie is een stelling. Het afleiden van een stelling is een logisch gevolg van de voorafgaande formules. Een logische consequentie is het resultaat van het deductieve systeem van een formeel systeem.

Een automatische stellingbewijzer is een programma dat van een gegeven propositie een formeel bewijs probeert te vinden. Dit is echter een moeilijk probleem dat niet in het algemeen beslisbaar is. Bij interactieve bewijsvoering wordt het formele bewijs door de gebruiker geleverd en slechts gecontroleerd met behulp van de computer.

Achtergrond

Formele taal

Zie Formele taal voor het hoofdartikel over dit onderwerp.

Formele taal is een eindige rij van symbolen. Deze symbolen worden over het algemeen ontworpen voordat ze een specifieke interpretatie krijgen, ofwel voordat er een bepaalde referent aan wordt gekoppeld.

Formele grammatica

Zie Formele grammatica en Formatieregel voor de hoofdartikelen over dit onderwerp.

Een formele grammatica is een beschrijving van de regels van een formele taal. Dit is een vrij breed begrip dat bijvoorbeeld op de informatica maar ook op de wiskundige logica betrekking kan hebben. De term "formele grammatica" wordt daarnaast soms ook gebruikt voor de regels van gewone menselijke taal (zie ook theoretische taalkunde). In het laatste geval heeft om spraakverwarring te vermijden de term grammatica echter de voorkeur.

Formeel systeem

Zie Formeel systeem voor het hoofdartikel over dit onderwerp.

Een formeel systeem, ook wel logisch systeem of logische calculus, bestaat uit formele taal in combinatie met een deductief systeem. Het deductieve systeem kan bestaan uit een reeks afleidingsregels, een reeks axioma's of een combinatie hiervan (in het laatste geval is sprake van de axiomatische methode). De bewijstheorie speelt in dit verband eveneens een belangrijke rol, namelijk bij het afleiden van de ene stelling uit de andere. Zie ook wiskundig bewijs.

Interpretaties

Zie Formele semantiek en Interpretatie (logica) voor de hoofdartikelen over dit onderwerp.

De interpretatie van een formeel systeem houdt het toekennen van betekenis aan symbolen in, zowel met betrekking tot natuurlijke als formele talen. In het laatste geval wordt van formele semantiek gesproken, in het eerste geval kortweg van semantiek.