FilosofieWiki

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:

Als A|-T, dan is AT 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:

1.(A&T) p(P)
2.AT(P)
3.A (A&T)(2, Abs)
4.Ap(1,3, HS)

Ap 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

Bewijs PBewijs PQ
 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.   PQ       ((n+m+1)-s, AD)
Bewijs x(Px)Bewijs x(PxQx)
 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.   PQ       ((n+m+1)-s, AD)
 s+2.   x(PxQx) (s+1; UG)


Bladeren
Hoofdpagina
Huishoudelijk
Argument
Connectieven
Links