Table of contents
- 1. Definities
- 1.1. Geldig vervolg
- 1.1.1. Abstracte formule
- 1.1.2. Tegenvoorbeeld
- 1.2. Sequent
- 1.3. Semantisch tableau
- 1.3.1. Gesloten tak
- 1.3.2. Open tak
- 1.3.3. Reductieregels
- 1.3.4. Tegenvoorbeeld
- 1.3.5. Consistent
- 1.3.6. Tautologie
- 1.4. Desda
- 1.5. Semantisch consistent
- 1.6. Adequaatheidsstelling
- 1.1. Geldig vervolg
Definities
Geldig vervolg
Notatie: Als ψ een geldig gevolg is van ∑ ↔ ∑ ⊨ ψ ↔ ∑ / ψ
Als ψ geen geldig gevolg is van ∑ ↔ ∑ ⊭ ψ
Een
formule
De formules van de propositielogica worden als volgt gedefinieerd: Dit is inductief bewijs. Notatie: Vervang kleine letters door Griekse letters. Wordt aangegeven met kleine griekse letters in plaats van normale letters. Een ingevulde abstracte formule heet een instantie. Als elke waardering van een formule φ ook meteen een model is van φ. bv.: ( φ ∨ ¬ φ ).
φ heet een geldig vervolg van een verzameling formules ∑ als elk model van ∑ ook model is van ψ.
Abstracte formule
Synoniemen: formuleschema
Als ∑ = ∅ dan ⊨ ψ. ψ is dan waar onder elke waardering en automatisch een
tautologie
.
Ofwel als voor elke waardering V geldt: V(φ) = 1.
Tegenvoorbeeld
Een
model
Notatie: verzameling modellen van een formule: MOD(φ) = { V | V(φ) = 1 } De waardering V heet een model van een formule φ als geldt: V(φ) = 1. Model van een formuleverzameling Een waardering V heet een model van een formuleverzameling ∑ als zij model is van elke φ ∈ ∑.
van ∑ dat geen model van ψ is. Dit is een tegenvoorbeeld van de gevolgtrekking ∑ / ψ.
Sequent
Een rij in de vorm: φ1, ... , φn o ψ1, ... , ψn
Tegenvoorbeeld van een sequent
Een
waardering
Synoniemen: situatie, valuation. De functie van alle propositie letters naar een waardering.
V die geeft V(ψ1) = ... = V(ψn) = 1 en V(φ1) = ... = V(φm) = 0.
Notatie: V( )
Semantisch tableau
Notatie: Slechts aangeven wat er verandert.
Een schema waarin op systematische wijze het mogelijk bestaan van tegenvoorbeelden van een gegeven sequent gereduceerd wordt tot een of meerdere overzichtelijke sequenten. Zodra deze boom niet verder gereduceerd kan worden, spreken we van een semantisch tableau.
Gesloten tableau: Alle takken sluiten.
Open tableau: Minstens een tak open.
Gesloten tak
Er treedt eenzelfde formule links en rechts op in de sequent.
Open tak
Er treedt geen formule zowel links als rechts op, terwijl ook geen regel meer toepasbaar is.
Reductieregels
Tegenvoorbeeld
Als het semantisch tableau van het sequent φ1, ... , φn o ψ1, ... , ψn minstens een open tak heeft.
Het tegenvoorbeeld kan dan worden afgelezen door de atomen links van o waar te maken, en recht onwaar.
Consistent
Als het semantisch tableau van het sequent φ1, ... , φn o minstens een open tak heeft.
Tautologie
Als het semantisch tableau van het sequent o ψ gesloten is en dus geen tegenvoorbeeld heeft.
Desda
Synoniemen: ↔
Dan en slechts als dan.
Semantisch consistent
Een formuleverzameling ∑ is (semantisch) consistent als ∑ een model heeft. We zeggen ook dat ∑ vervulbaar is.
Een formuleverzameling die niet consistent is, heet inconsistent.
Adequaatheidsstelling
φ1, ... , φn ⊨ ψ ↔ er bestaat een gesloten tableau voor φ1, ... , φn o ψ
Comments