18 lines
440 B
Plaintext
18 lines
440 B
Plaintext
|
Semantics of FOL
|
||
|
|
-- graph theory
|
||
|
|
-- \Sigma \entails \alpha
|
||
|
|
-- Lemma : two assignments agree on FV(\alpha) in a structure L,
|
||
|
|
then M \entails \alpha under s_1
|
||
|
|
iff
|
||
|
|
M \entails \alpha under s_1
|
||
|
|
-- Proof of lemma : terms, atomic formuals.
|
||
|
|
-- Examples :
|
||
|
|
-- L =(R(,))
|
||
|
|
M1=(\nat, <)
|
||
|
|
M2=(\nat, divides)
|
||
|
|
M3=(pow(nat), \subset)
|
||
|
|
formulas : R(x,y)
|
||
|
|
: \exists x \forall y (R(x,y)).
|
||
|
|
|
||
|
|
|