feat(Logics/Temporal): temporal formula type with propositional structure

[benbrastmckie]

Summary

Extends Connectives.lean from PR #648 with temporal operator typeclasses, then defines two formula types that instantiate them:

        PropositionalConnectives
           (HasBot + HasImp)
                    |
         FutureTemporalConnectives
               (+ HasUntil)
              /              \
   LTLConnectives      TemporalConnectives
    (+ HasNext)            (+ HasSince)

FutureTemporalConnectives factors out the shared future fragment so code generic over future-only logics need not commit to past or next-step operators. Temporal.Formula instantiates TemporalConnectives (future + past); LTL.Formula instantiates LTLConnectives (future + next).

Dependency

Stacked on PR #648 (feat(Foundations): propositional connectives typeclass hierarchy). Please review/merge #648 first.

New files

• `Cslib/Logics/Temporal/Syntax/Formula.lean` -- `Temporal.Formula` inductive type with `TemporalConnectives` instance
• `Cslib/Logics/LTL/Syntax/Formula.lean` -- `LTL.Formula` inductive type with `LTLConnectives` instance and `toTemporal` embedding

Modified files

• `Cslib/Foundations/Logic/Connectives.lean` -- added `HasUntil`, `HasSince`, `HasNext`, `FutureTemporalConnectives`, `LTLConnectives`, `TemporalConnectives`
• `Cslib.lean` -- added temporal and LTL imports
• `references.bib` -- added Kamp1968, Pnueli1977, Burgess1984, VardiWolper1986, GPSS1980

Design rationale

`next` is a primitive in `LTL.Formula` rather than derived from `untl`. The encoding `next φ = φ U ⊥` holds on discrete non-ending sequences but fails in general temporal models; keeping `next` primitive supports broader model classes. The `toTemporal` embedding translates `next φ` as strict `untl φ ⊥` and `untl` as reflexive until.

Argument convention follows Burgess (1984): `untl event guard` where the first argument is the event (holds at the witness point) and the second is the guard (holds at all intermediate points).

Deferred

• LTL satisfaction semantics over omega-words (follow-up PR)
• LTS-based semantics redesign
• `Encodable`/`Countable`/`Infinite`/`Denumerable` instances

References

• [Kamp1968] H. Kamp, Tense Logic and the Theory of Linear Order, PhD thesis, UCLA, 1968.
• [Pnueli1977] A. Pnueli, "The Temporal Logic of Programs," 18th FOCS, 1977.
• [Burgess1984] J. P. Burgess, "Basic Tense Logic," Handbook of Philosophical Logic, vol. II, 1984.
• [VardiWolper1986] M. Y. Vardi and P. Wolper, "An Automata-Theoretic Approach to Automatic Program Verification," 1st LICS, 1986.

AI Tools Used

Claude Code was used to rebase onto PR #648, resolve merge conflicts, adjust temporal operators, fix import minimization, and verify CI. All mathematical decisions reviewed by the human author.

[ctchou]

General comments:

• We should start with a temporal logic with only future-time temporal operators. Past-time temporal operators are not very useful in deductive program verification and complicate the semantics.
• I would like to have a temporal logic that can talk about the (omega-)executions of LTS, not just a sequence of states.
• Also, we should be able to talk about LTS transitions.
• I don't understand what Encodable/Countable/Infinite/Denumerable instances are doing there. They seem to be completely irrelevant.

[benbrastmckie]

Thanks for the comments. The latest push addresses these points:

1. Future-only temporal operators. FutureTemporalConnectives (propositional + until) is now a shared base class. LTL.Formula instantiates LTLConnectives (future + next) with only future-time primitives. Temporal.Formula instantiates TemporalConnectives (future + past) for tense logic.

2. Omega-executions of LTS, not just state sequences. LTL.Satisfies is removed from this PR. Connection to LTS.OmegaExecution — which already carries both ss : ωSequence State and μs : ωSequence Label — is the right approach. A follow-up PR can define satisfaction directly over OmegaExecution pairs rather than bare state sequences.

3. Büchi automata and ω-regular languages. A natural follow-up is to prove the LTL-to-Büchi translation theorem, connecting LTL.Satisfies to ωLanguage.IsRegular via the existing boolean closure results.

4. Encodable/Countable/Infinite/Denumerable. Removed. Deferred to a completeness PR where they are actually needed.