« first day (1 day earlier)      last day (15 days later) » 

user21820
user21820
03:15
@HaskellFun: @xavierm02's idea works. define path(x,y) = "exists set P ( P is a minimal closed set under edge traversal and P contains both x,y )".
@xavierm02: Thanks for the link about MSO being unable to define finite subset. But the answer does not contain any proof of the crucial claim. Any reference for that?
 
9 hours later…
xavierm02
xavierm02
12:48
@user21820 Nope. I'd guess it's proved by induction on the formula. The exact property should be that for every formula F there are some "there are at least n elements" property whose boolean combination G is so that M |= F iff M |= G. It works for x=x because you can take "at least 0 elements" and for x=y because you can take "at most one element". Then, for boolean combinations of Fs, you take the same combinations of Gs.
For forall x, F, you just take G (which should work because formulas are implicitly universally quantified). And for exists x, F, you take the G for not(forall x, (not (F))).
(I'm really not sure but I couldn't find any reference so I tried to do it myself)
user21820
user21820
13:05
@xavierm02: That sounds correct for first-order logic. But MSO?
xavierm02
xavierm02
13:25
@user21820 Well the only thing that changes is that you have a second type of forall quantifier. But it's still implicitly universally quantified so the induction step from F to forall P, F should work just as well. And then, there's a new base case P x. But since P is implicitly universally quantified, it means forall P, P x, which is false since for P the always false predicate, it's false. So you can take "at least 1 element and at most 0 element" or some other absurd statement.
user21820
user21820
13:54
@xavierm02: I'm not in the mood for thinking about it now, but neither argument sounds structurally right to me anymore. It does not distinguish between 1-input and 2-input predicates.
xavierm02
xavierm02
14:41
@user21820 Yeah. It's not a real argument, just some random thought.
xavierm02
xavierm02
15:04
First fix attempt: It should be, for all mu, M, mu |= F iff M, mu |= G
or maybe not
user228268
15:17
@xavierm02 could you refer to this?
"Oh, no. I see a problem. Lets us note, that in my formula in my post (question) I propose formula something like:
forall_a....
where a is node.
So, my formula begins with first order element. It should begin with:
(firstly, quantify over second order elements, no first order formula (here can't happen quanitying by first order elements)
for formula in MSO should looks like:
forall_X exists_Y.... (formula in FO)

I have other idea, so:
forall_X, forall_Y
if X is closre of some node x and
user228268
15:31
@user21820, for me You told that this idea works. I shown above, that it should be of form:
quantify by second order elements (first order formula)
user21820
user21820
@HaskellFun: I've no time to read what you wrote now.
user228268
ok
user21820
user21820
@user21820 <-- Just follow this and it will be correct.
user228268
no, it is not to correct
user21820
user21820
It is correct.
user228268
15:37
it is not form of (quantify over second elements) (first order formula)
user228268
MSO requiers thar (from point view of my lecturer)
user228268
It is why I propopsed other idea (but based on @xavierm02 idea)
xavierm02
xavierm02
16:25
@HaskellFun I don't understand your question
Ah
You want the second order quantifiers on the outside
I was looking at this to try to get ideas for the definability of finiteness but it could help you too: math.stackexchange.com/questions/2099964/…
Wait. The formula is of the form <-- second order quantifiers --> <-- first order quantifiers --> <-- boolean stuff -->
user228268
16:44
you formula ?
xavierm02
xavierm02
Both.
user228268
Hmm, but your formula
user228268
only
user228268
states that
user228268
S is closure of some node x
user228268
16:51
you must express more
user228268
I mean
user228268
that you must say something like that:

forall_a [[exists_b exists_c [ (b =\= c) ...
user228268
∀a[{∃b∃c((b≠c)∧Path(a,b)∧Path(a,c))}→(∃d(Path(b,d)∧Path(c,d))]
user228268
for taks above formula must be said
user228268
(task with church-roser relation)
user228268
16:54
You helped me to express Path(x,y)
user228268
but Path uses second order elements (quantifiers by sets)
user228268
so applying this solution with my formula for church-rosser relation problem
user228268
we get this problem that I said
xavierm02
xavierm02
aaaaah
I thought you were talking about the formula for path
user228268
so my formula works
user228268
17:08
for church-rosser problem
user228268
(it based on your solution)
user228268
yeah?
xavierm02
xavierm02
You don't need z' to be in X and Y. It's implied by being in closure(Z).
But it looks like it's fine.
I need to go now, I'll come back later to recheck.
user228268
ok, thanks
xavierm02
xavierm02
You can use the transformation on page 16 here though: logic.at/lvas/185301/Leivant_higher-order-logic.pdf
What is says, basically, is that you can always push the second order quantifiers before the first order ones
if poth are the same it's trivial
if it's some exists and some forall, you have to use a trick
user228268
17:13
Ok, I look at it later. At this moment I am happy with my formula :)
user228268
17:50
@xavierm02 I am not sure it it is ok:
∀X∀Y∃Z
[ ∃x∃y (Closure(x, X) ∧ Closure(y,Y) ∧ (X n Y =\= emptyset)) → (X u Y) \susbeteq Z]
user228268
On the whole, it shoud look like:
∀X∀Y
[ ∃x∃y (Closure(x, X) ∧ Closure(y,Y) ∧ (X n Y =\= emptyset)) → ∃Z (X u Y) \susbeteq Z]
user228268
On the whole, I can't tell a difference
user228268
(this second violate condition abuot sequence of quantifiers

« first day (1 day earlier)      last day (15 days later) »