Beweren en bewijzen/supplement/De Gevolgmatrix

Wat hebben al die rare symbolen met elkaar te maken?

Op pagina 11 introduceert Van Benthem de schuine streep: a, b, c, ... / B. Hij scheidt aannames van een conclusie, en men mag hem ook schrijven als men nog niet weet of de conclusie uit de aannames volgt. JE kunt de schuine streep lezen als een |= met een vraagteken. Ondertussen hebben we een aantal symbolen leren kennen die allemaal om een soort implicatie of gevolg uitdrukken. Het is bijna hetzelfde, maar net niet. Ook de typepijl -> uit onze taal heeft ermee te maken.

Hier een poging, orde te scheppen.

Voegtekens uit onze taal

Deze worden gedefinieerd in de grammatica en komen voor in teksten die in onze taal geschreven zijn. Helaas zijn deze twee niet te onderscheiden qua uiterlijk.

-> 

Implicatie.

-> 

Functietype.

Metataal

Deze horen niet bij onze taal maar worden gebruikt om te praten over formues uit onze taal.

|= 

Geldig gevolg.

⊢ 

Afleidbaar.

o 

Semantisch tableau.

De Matrix

	-> implicatie	-> functietype	|= geldig	⊢ afleidbaar	o tableau
->		f: Bew(a)->Bew(b) f: Bew(a->b) "Een functie die voor elk gegeven bewijs voor a een bewijs voor b oplevert is een bewijs voor a->b." Zo is Bew gedefinieerd.	a |= b |= a->b Zo is -> gedefinieerd.	a |- b |- a -> b Implicatie-introductie	o a->b | a o b
->			x in a |= expr(x) in b |=(LAMBDA x:a. expr(x)) in a->b Zo is -> gedefinieerd.	x: a ⊢ expr(x): b ⊢(LAMBDA x:a. expr(x)): a->b Typeringsregel voor LAMBDA-expressies.
|=	A |= a A |= a->b A |= b Modus ponens	f in a->b, x in a |= f(x) in b "Als het argument van een functie in haar domain ligt, ligt het beeld in haar range." Zo zijn de begrippen domain en range gedefinieerd.		A |- b A |= b "Wat bewezen is, is ook waar." Zo zijn de deductieregels gedefinieerd. Dit kun je nagaan door ze een voor een te controleren.	o a sluit |= a "Als er geen tegenvoorbeeld bestaat moet het wel waar zijn.
⊢	A |- a A |- a->b A |- b Implicatie-eliminatie	f: a->b, x: a f(x): b Typeringsregel voor functieaanroep.	A |= b en ⊢ is volledig A |- b "Wat waar is kan ook bewezen worden, tenminste als het bewijssysteem volledig is."
o			|= a o a sluit "Een ware bewering heeft geen tegenvoorbeeld."