Re: [tlaplus] Quest. Cont. About Theorem And Inference Rule

[Stephan Merz <stepha...@xxxxxxxxx>]

Hi again,


> On 30 Apr 2017, at 18:17, belout...@xxxxxxxxx wrote:
> 
> Thanks Stephan For your rapid reply,
> 
> You say the proof is obvious. But, I can not see How to make the Proof in a formal way of this Theorem .

you have not explained what you mean by "formal" – which proof system are you thinking of?

Semantically, the reasoning is as follows:

ENABLED A is a state predicate that holds in state s if there exists some state t such that the pair (s,t) of states satisfies A.

The implication A => ENABLED A is an action formula and as such is evaluated over a pair of states,. So take an arbitrary pair (s,t)  of states. If (s,t) does not satisfy A, the implication holds trivially. If it does, then s also satisfies ENABLED A, since we know that there is a state t such that A holds of the pair (s,t).

Syntactically, you need to expand ENABLED into a quantification over all flexible state variables that have (free) occurrences in A, and so the implication generalizes the standard theorem

F => \E x: F

of first-order logic.

> 
> Furthermore, What about The suggested Inference Rules ?
> 
> 
>                A                              A
>          R1: ---------------              R2:----------------
>              A ==> Enabled(A)                 Enabled(A)
> 

Again, without an explanation of the proof system in which these rules are stated I cannot really know their intended meaning. In particular, should I read a premise "A" in a proof rule as asserting that A is true of an arbitrary pair of states? This would be a standard interpretation of proof rules in modal logic but would make rule R2 pretty useless. As for R1, since the consequent is already a theorem, the premise is unnecessary.

Have you read some formal exposition of the logic TLA [1,2]?

Hope this helps,
Stephan

[1] L. Lamport. The Temporal Logic of Actions. TOPLAS 16(3):872-923, 1994.
[2] S. Merz. The specification language TLA+. In: Logics of Specification Languages (D. Bjørner, M.C. Henson, eds.), Monographs in Theoretical Computer Science, pp. 401-451, 2008.


> Thanks For Help
> 
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.