assignment 2 uploaded
This commit is contained in:
parent
a3968c50a3
commit
a2c5bc1017
Binary file not shown.
|
@ -0,0 +1,17 @@
|
||||||
|
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)).
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,17 @@
|
||||||
|
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)).
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue