Re: [tlaplus] LTL axiomatic system

On 15 Aug 2016, at 19:29, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

However, one nice aspect of propositional temporal logic (PTL) is that it is decidable. So, you could use some decision procedure for PTL such as ls4 (http://www.cs.man.ac.uk/~sudam/, the system that we use in the TLA+ Proof System) and ask it if the formula

[](P <=> Q) /\ [](R <=> S) => []( (P until R) <=> (Q until S) )

Hi Stephan,

thank you for answer. LS4 is no longer available apparently.

Indeed, but there are similar decision procedures, e.g. TRP++ (https://cgi.csc.liv.ac.uk/~konev/software/trp++/) or the Logics Workbench (http://www.lwb.unibe.ch, you can even enter your formula via a Web form).

Since you plugged it into TLAPLUS, if I enter the formula will I have the answer? Because in that case I will often use it this way.

Yes, you can (except that "until" is not accepted):

LEMMA 

  ASSUME NEW TEMPORAL P, NEW TEMPORAL Q

  PROVE  [](P <=> Q) => ([]<>P <=> []<>Q)

BY PTL

Another question and then I dfefinitely go and buy books: why have you added the [] operators to your formula because
in the inference rule you don't need them either in the premisser or in the conclusion.

The sensible interpretation of the inference rule that you gave is that the formulas stated in the antecedent are supposed to hold everywhere (i.e., always in the future), hence they must be boxed in the formula. The formula

(P <=> Q) => ([]<>P <=> []<>Q)

is not valid since P and Q are assumed to be equivalent only in the initial state, and nothing is known about their relationship in other states. More generally, a rule (temporal sequent)

Gamma, F |- B

for some set of formulas Gamma is equivalent to the sequent

Gamma |- []F => B

but not the sequent

Gamma |- F => B

In other words, the standard deduction theorem of classical logic has to be modified for temporal (and similar modal) logics. Leslie often refers to this as "temporal logic being evil".

Best,

Stephan