Sept 2022 Lo1 to ltl

0 votes

= ∀t1.t2.((t1 < t2 ^ a(t2) ) -> (a(t1)->b(t2))                          ---> 1

= ∀t1.(Ǝt2.(t1 < t2 ^ a(t2) ) ->(a(t1) -> b(t2))                        ----> 2

Can you please explain these two equivalences 1, 2 are achieved?

Sept 2022 9.d

1 Answer

0 votes

First of all, you have a small mistake in there, as the time over the "b" variables should be "t1" and not "t2" (this is important!). That said you can then do the following:

t1.t2.((t1 < t2 & a(t2) ) -> (a(t1)->b(t1)))

t1.t2.(!(t1 < t2 & a(t2) ) | (a(t1)->b(t1)))     [by definition of the implication]

t1.(t2.!(t1 < t2 & a(t2) ) | (a(t1)->b(t1)))     [as (a(t1)->b(t1)) does not depend on t2]

t1.(!Ǝt2.(t1 < t2 & a(t2) ) | (a(t1)->b(t1)))     [pull the negation outwards]

t1.(Ǝt2.(t1 < t2 & a(t2) ) -> (a(t1)->b(t1)))     [by definition of the implication again]

which is finally the result you wanted. In its core, the reason for that is that one part of the inner term can be excluded from the bounds of the quantification of "t2", and due to the negation that arises from resolving the implication, this quantification symbol is flipped to an "Exists".

From a more "logical explanation" point you can argue that as follows:

t2.((t1 < t2 & a(t2) ) -> (a(t1)->b(t1))) is true if either (a(t1)->b(t1)) holds (in this case the quantification is irrelevant) or if that is not the case, (t1 < t2 & a(t2) ) must be false (which then of course needs to be false for all time points "t2"). Thus if there exists a time point "t2" where (t1 < t2 & a(t2) ) is known to be true, this implies that (a(t1)->b(t1)) needs to hold, for the whole term to be true.

This previous sentence is however the exact natural language definition of:

Ǝt2.(t1 < t2 & a(t2) ) -> (a(t1)->b(t1))

which explains the equivalence logically due to the explanation.

by (3.4k points)

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
+1 vote
1 answer
0 votes
1 answer