V.8 Satisfiable and valid
Satisfiable and valid [Slide 167]
- A first order ITL formula f is satisfiable if and only if there exists an
interval σ such that M⟦f⟧(σ) = tt.
- A first order ITL formula f is valid if and only if for all intervals σ,
M⟦
f⟧(σ) = tt.
Example 55.
- (0 < 1) is a valid formula.
- Formula skip ∧ A = 0 is satisfiable because M⟦skip ∧ A = 0⟧(σ) = tt
where interval σ is σ0σ1 and σ0(A) = 0 and σ1(A) = 10.