Constant symbols are not allowed in a "$d" statement.

[Brian Larson]

In the process of cleaning-up my theorems for possible addition to set.mm I found a fundamental inconsistency in the definition of my discrete time operator ^. which is defined in terms of my continuous time operator @.

p@t says evaluate p at time t which is restricted to time the machine starts operation, t=0, to the present instant, t=now, when the software controlling the machine must decide what to do:

$( Define domain of time ` TIME ` from ` t = 0 ` to ` now ` $)
df-bl.time $a |- TIME = { x | ( x e. RR /\ 0 <_ x /\ x <_ now ) }  $.    

@ is used to declaratively specify machine timing behavior such as:

invariant  
  << LRL: : --Lower Rate Limit
    exists t~time  --there was a moment
      in (now-lrl)..now   --within the previous LRL interval
      that (n@t or p@t) >>  --with a pace or non-refractory sense

which defines the fundamental effectiveness property of pacemakers treating bradycardia.   If the physician decides that the Lower Rate Limit should be 60 beats per minute, the LRL interval (lrl) will be 1 s.  Then LRL asserts that forever the pacemaker is operating, a heart beat will have occurred, either intrinsically, n@t or paced p@t.

Naturally, ( p@t_1 ) @ t_2 <-> p@t_1.

Works great for threads with sporadic dispatch protocols.  For periodic threads, a discrete temporal operator shifts time of evaluation by an integer number of thread periods.

p^-3 means the value of p, three periods before now.  The discrete time operator is defined in terms of the continuous time operator for which $d A ^. $. caused the error.

  ${
  $d A ^. $.
$( Time Shift Value (for ` ^. ` not in ` A ` )  $)
df-bl.tsc $a |- ( ( A e. RR /\ B e. ZZ /\ D e. RR /\ ( now + ( D x. B ) ) e. TIME ) ->
( A ^. B ) = ( A @ ( now + ( D x. B ) ) ) ) $.
  $}
  

This is to be applied only when no ^. are used to express A because composition of ^. add the time shift values:

$( Distribute ` ^. ` over values $)
df-bl.tsdisc $a |- ( ( A e. RR /\ B e. ZZ /\ C e. ZZ ) ->
  ( ( A ^. B ) ^. C ) = ( A ^. ( B + C ) ) ) $.

If I am the only person using df-bl.tsc (or its wff equivalent df-bl.ts) I can be sure to use them atomically . . . except all of the proofs of distribution have the same problem.

The rigor of Metamath exposed a fundamental flaw in BLESS logic.

I'm considering removing ^. from the language entirely and try to prove the periodic threads using only the continuous time operator.

[Mario Carneiro]

You can't use $d to ensure that constants don't appear in a formula. I don't have all the context needed to understand why you need to do this, but one way to express it would be to have a predicate "|- ^.-free A" and have rules like "|- ( ^.-free A -> ( ^.-free B -> ^.-free ( A /\ B ) ) )" for all formula constructors except for ^. . But this wouldn't really be suitable for set.mm, it would have to be its own database because it would require new axioms. (It's not that unusual to have alternative databases for different logics, we already have about 10 such databases. set.mm is just the biggest one since it represents "conventional" logic in some sense.)

More likely, what you actually need here is some kind of modality like "A always holds" or "A holds N steps in the future", and it commutes with most operators but has special behavior around ^. .

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cf3b8654-0c1b-4b89-8f5e-63cfaa54a3f3n%40googlegroups.com.