title: Formeel bewijs
text: Formeel bewijs in de formele wetenschap is 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.
  
  Bij interactieve bewijsvoering wordt formeel bewijs geleverd en gecontroleerd met behulp van computers. Het eerste wordt ook wel het automatisch bewijzen van stellingen genoemd en is vanzelfsprekend moeilijker dan het laatste.
  
  Achtergrond
  
  Formele taal 
  
  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 
  
  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 
  
  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 
  
  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.
  
  Formele wetenschap