Quest. Cont. About Theorem And Inference Rule

[belout...@gmail.com]

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 .

Furthermore, What about The suggested Inference Rules ?


A A
R1: --------------- R2:----------------
A ==> Enabled(A) Enabled(A)

Thanks For Help

[Stephan Merz]

Hi again,

> On 30 Apr 2017, at 18:17, belout...@gmail.com 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.