Go backward to Quantification over Flexible Variables Go up to Top Go forward to Refinement Mappings

Quantification in TLA

• Syntax:
  • <general formula> <=> <STLA formula>
    | exists <flexible variable>: <general formula>
    | exists <rigid variable>: <general formula>
    | <general formula>and <general formula>
    | not <general formula>
• Semantics:
  • sigma[[exists x: F]] <=> exists rho, tau in St^infinity:
       (#sigma= #rho) and (rho =_x tau) and tau[[F]]
  • sigma[[exists c: F]] <=> exists c in Val: sigma[[F]]
• Proof rules:
  • E1.

    |- F(f/x) => exists x: F

  • E2.

    F =>G

    (exists x: F) => G

    , x not free in G.
  • F1.

    |- F(e/c) => exists c: F

  • F2.

    F =>G

    (exists c: F) => G

    , c not free in G.