Formeel bewijs

Een formeel bewijs is een logisch bewijs formeel uitgedrukt in een axiomatisch systeem. Hierbij wordt begonnen met axioma's. Dan worden de daaruit afgeleide theorema's geponeerd (die natuurlijk afleidbaar zijn uit de axioma's maar om papier en tijd te sparen worden ze niet afgeleid - dat is al eerder gebeurd door iemand). Vervolgens wordt de propositie bewezen.

Dat de theorema's gebruikt mogen worden kan ook bewezen worden:

• De axioma's impliceren de theorema's, A|-T.
• Stel propositie p is een logisch gevolg is van de axioma's en theorema's, (A&T)|-p.
• Dan geldt ook dat de axioma's de propositie impliceren, A|-p (bewijs volgt).

Als A|-T, dan is A→T een tautologie. En zo is ook (A&T)→p een tautologie. Wat we van deze tautologische proposities afleiden zijn ook tautologieën. Zo komen we tot de volgende redenering:

A→p is een tautologie, dus A|-p. We kunnen dus theorema's als het ware toevoegen aan de axioma's om een formeel bewijs te construeren.

Een voorbeeld van een concreet formeel bewijs: 1x2 is 2.

Bewijsstructuren

 1.     A1         )
 ..     ..         ) Axioma's
 n.     An         )
 n+1.   T1         ]]
 ..     ..         ]] Theorema's
 n+m.   Tm         ]]
 ..     ..
 r.     P

 1.     A1         )
 ..     ..         ) Axioma's
 n.     An         )
 n+1.   T1         ]]
 ..     ..         ]] Theorema's
 n+m.   Tm         ]]
 n+m+1. P          (AD)
 ..     ..
 s.     Q
 s+1.   P→Q       ((n+m+1)-s, AD)

 1.     A1         )
 ..     ..         ) Axioma's
 n.     An         )
 n+1.   T1         ]]
 ..     ..         ]] Theorema's
 n+m.   Tm         ]]
 ..     ..
 r.     Pa         } a arbitrair
 r+1.   ∀x(Px)     (r,UG)

 1.     A1         )
 ..     ..         ) Axioma's
 n.     An         )
 n+1.   T1         ]]
 ..     ..         ]] Theorema's
 n+m.   Tm         ]]
 n+m+1. Pa         (AD)
 ..     ..
 s.     Qa
 s+1.   P→Q       ((n+m+1)-s, AD)
 s+2.   ∀x(Px→Qx) (s+1; UG)