« first day (2 days earlier)    last day (14 days later) » 

xavierm02
xavierm02
14:38
Ok. I think I have a good argument to say that you can't characterise finiteness in MSO over the empty signature.
First, replace all "x = y" by "forall P, P x <-> P y".
Then, do the transformation to put all second order quantifiers first, then all first order quantifiers and finally the boolean stuff. It's also second order quantifier followed by a monadic first order formula. And monadic first order formulas have the finite model property (because you can say that two elements of the model are equivalent if they are in the same predicates, and then the quotient model is still a model and …
I'm not sure yet how to remove the second order forall quantifiers though.
xavierm02
xavierm02
14:55
@HaskellFun Both are the same I think. If you look at "a->b" as "not(a) \/ b", and since we don't consider models with empty domains, you can get the ∃ outside of the arrow. Then you can swap if with the first order ∃ and you've got your first formula.
user228268
15:22
Ok will think about it, but if you are right then task is solved
user228268
17:15
Ok, using p -> q <---> p or ~q was a good idea to see it.
user228268
thanks!

« first day (2 days earlier)    last day (14 days later) »