ENABLED Operator Theorems

[kacem belout]

Hallo,

I noticed the following theorems concerning the ENABLED Operator that I  hopefully would like to prove them in a formal way ( i.e Formally ( Logically and/or symbolically) as using Inference Rules)

In the context of the Raw Logic (RTLA), for any Action A, we assert the following valid statements. Let me know if any one is not valid by giving a counterexample, thanks !.

Theorem 1 : A ==> ENABLED(A)

                 Proof : Now, I don't know How To formally and mechanically derive ENABLED(A) From A which is expressed in terms of primed variables and unprimed variables.

Theorem 2 : \Not ENABLED(A) ==> \Not A

                 Proof : Is equivalent to Theorm1 by propositional logic rule (implication equivalente to its contrapositive).

Theorem 3 : \Not A ==> \Not ENABLED(A)

Theorem 4 : \Not (ENABLED(A)) ==> ENABLED( \Not (A))

Theorem 5 :  ENABLED(A) <==> ENABLED(-1(A)) , where -1(A) == (A)-1 ; inverse of A.  (A)-1 == A ( v ' <- v , v <- v ')

Theorem 6 : For any state predicate P.  P <==> ENABLED(P)

Theorem 7 : For any state predicate P.  P ==> ENABLED((P) '), where ' == Prime operator.

Theorem 8 : For any state predicate P.  P ==> ENABLED(((p)')-1)

Another Thanks for your Help and Critics.

[Stephan Merz]

Hello,

> On 3 May 2017, at 10:46, kacem belout <belout...@gmail.com> wrote:
>
> Hallo,
>
> I noticed the following theorems concerning the ENABLED Operator that I hopefully would like to prove them in a formal way ( i.e Formally ( Logically and/or symbolically) as using Inference Rules)

as I tried to explain before, in order to give a precise meaning to your notion of "formal" proof, you would need to give clear definitions.

>
> In the context of the Raw Logic (RTLA), for any Action A, we assert the following valid statements.

I don't understand why you insist on Raw TLA: the difference between RTLA and TLA only exists at the temporal level, and you don't consider any temporal formulas. Also, it would help if you used actual TLA syntax.

> Let me know if any one is not valid by giving a counterexample, thanks !.
>
> Theorem 1 : A ==> ENABLED(A)
> Proof : Now, I don't know How To formally and mechanically derive ENABLED(A) From A which is expressed in terms of primed variables and unprimed variables.

See my previous answer: the implication holds for the same reason why F => \E X: F is a theorem of first-order logic.

>
> Theorem 2 : \Not ENABLED(A) ==> \Not A
> Proof : Is equivalent to Theorm1 by propositional logic rule (implication equivalente to its contrapositive).

Yes, so it's just a corollary to the previous theorem.

>
> Theorem 3 : \Not A ==> \Not ENABLED(A)

Wrong. Consider A == x = 0 /\ x' = 1 and a state s that assigns 0 to x. Then the stuttering step (s,s) satisfies ~ A and ENABLED A.

>
> Theorem 4 : \Not (ENABLED(A)) ==> ENABLED( \Not (A))

Consequence of Theorems 1 and 2.

>
> Theorem 5 : ENABLED(A) <==> ENABLED(-1(A)) , where -1(A) == (A)-1 ; inverse of A. (A)-1 == A ( v ' <- v , v <- v ')

Wrong, take again A == x=0 /\ x'=1. then

ENABLED A \equiv x = 0
ENABLED (A)-1 \equiv x = 1

>
> Theorem 6 : For any state predicate P. P <==> ENABLED(P)

Correct.

> Theorem 7 : For any state predicate P. P ==> ENABLED((P) '), where ' == Prime operator.

Correct. (ENABLED P' is true iff P is satisfiable.)

> Theorem 8 : For any state predicate P. P ==> ENABLED(((p)')-1)

Isn't (P')-1 = P, so this is the same as theorem 6?

Regards,
Stephan