Re: [tlaplus] Leibniz and ToBoolean Operators and Proof Fragment

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

Hello,

> On 2 May 2017, at 14:31, belout...@xxxxxxxxx wrote:
> 
> Hi all,
> Somme questions concerning technical concepts in the " TLA+2 A Preliminary Guide-January 2014".
> 
> 1)- Section 5.2, page7, says that the reasonable theorem of the module M is not valid in TLA+1. I think that the theorem is always valid, because the problem is with the INSTANTIATION. With instantiation meaning a kind of substitution, the given INSTANCE statement " INSTANCE M with C <- x, D <- y, F <- Prime " substitutes VARIABLES for CONSTANTS, where these two concepts come from different semantics levels in TLA theory. The theorem remain valid if we have substitute CONSTANTs for CONSTANTs. For example, with the following substitution(instantiation)  .... with C <- Cst1, D <- Cst2, ...,  where Cst1 and Cst2 are Constants, the following is true :
>           THEOREM  Cst1 = Cst2 ==> Cst1' = Cst2'

please observe that substitution of constant parameters by non-constant expressions is allowed only for constant modules. Being able to do so is considered useful enough to warrant the restriction that operator parameters must be substituted by Leibniz operators that the TLA+2 guide introduces. In particular, it allows you to define fundamental data structures in a constant module and apply them to state- or action-level expressions.

> 2)- At the bottom of subsubsection 7.8.2, page 34, we have a proof fragment that I think is about the following theorem : 
>                                       THEOREM  x > 3 ==> x > 2
> The below proof fragment is said to be correct because .....
>    <3>2  x > 3        
>    <3>3  x > 2
>          By <3>2  
> 
> I think that this proof fragment misses some fundamental facts that allow us to formally derive x > 2 from x > 3.
> Our suggestions to complete the fragment correctness are the following steps :
> 
>    The fact that 3 > 2 is true By Definition of > On Integer or Real
>     And
>    The fact that the Relation > is transitive.

Yes, of course. These are baked into the knowledge of TLAPS and its backends and are not indicated explicitly in proofs, just like we do not require justifications of logical or set-theoretic facts and accept the following justification of proof step <4>9.

  <4>7. S \cap T = {}
  <4>8. x \in S
  <4>9. x \notin T
     BY <4>7, <4>8


> 3)- section 8, page 36, gives a recursive definition for the Operator ToBoolean, and says that this Operator exists only in the semantics. I can not catch this idea ?.Furthermore, it gives a (syntactical- TLA+ level) definition as follows:
> 
>            ToBoolean(x) == x <--> TRUE    " x is Equivalent to TRUE "
> the question here is , how can we compute the value of ToBoolean(5) and ToBoolean(ToBoolean(5)) with x not in the set BOOLEAN.

The document refers to Section 16.1.3 of Specifying Systems for an explanation of the problem, and I assume that you have read this. Briefly, TLA+ is untyped and does not follow the conventional distinction of (non-Boolean) terms from (Boolean) formulas. For example, 5 /\ 7 is a well-formed expression of TLA+. There are different ways of interpreting such expressions, and the "liberal interpretation" that underlies TLAPS ensures that all standard laws of propositional and first-order logic remain valid without checking the type of the arguments.

For example, 

  (~ ~ x) \equiv x

is valid for arbitrary x, even for x=5. (But the formula in which you replace "\equiv" by "=" is not.)

We do not need to know if ToBoolean(5) equals TRUE or FALSE, but we assume (1) that it is a Boolean, and (2) that ToBoolean is idempotent on Booleans. For example, ToBoolean(ToBoolean(5)) = ToBoolean(5). All that is required are these two conditions. It is a fun fact that assuming the liberal interpretation you can actually define

ToBoolean(x) == x \equiv TRUE

but it doesn't help you understand the operator or compute the value of ToBoolean(5).

Regards,
Stephan