Skip to content

Commit 3e11b1f

Browse files
benbrastmckieclaude
benbrastmckie
and
claude
committed
feat(Logics/Temporal): temporal formula type with propositional structure
Add temporal logic formula types for both full temporal logic (with until and since) and LTL (with until and next). Extend the connective typeclass hierarchy with HasUntil, HasSince, HasNext, FutureTemporalConnectives, LTLConnectives, and TemporalConnectives. New files: - Cslib/Logics/Temporal/Syntax/Formula.lean - Cslib/Logics/LTL/Syntax/Formula.lean Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 194f0c3 commit 3e11b1f

5 files changed

Lines changed: 448 additions & 6 deletions

File tree

‎Cslib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
137137
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
138138
public import Cslib.Logics.HML.Basic
139139
public import Cslib.Logics.HML.LogicalEquivalence
140+
public import Cslib.Logics.LTL.Syntax.Formula
140141
public import Cslib.Logics.LinearLogic.CLL.Basic
141142
public import Cslib.Logics.LinearLogic.CLL.CutElimination
142143
public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
@@ -149,6 +150,7 @@ public import Cslib.Logics.Modal.LogicalEquivalence
149150
public import Cslib.Logics.Propositional.Defs
150151
public import Cslib.Logics.Propositional.NaturalDeduction.Basic
151152
public import Cslib.Logics.Propositional.NaturalDeduction.Theory
153+
public import Cslib.Logics.Temporal.Syntax.Formula
152154
public import Cslib.MachineLearning.PACLearning.Defs
153155
public import Cslib.MachineLearning.PACLearning.VCDimension
154156
public import Cslib.MachineLearning.PACLearning.VersionSpace

‎Cslib/Foundations/Logic/Connectives.lean‎

Lines changed: 54 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,23 +8,26 @@ module
88

99
import Cslib.Init
1010

11-
/-! # Connective Typeclasses for Propositional Logic
11+
/-! # Connective Typeclasses for Propositional and Temporal Logic
1212
13-
This module defines a typeclass hierarchy for propositional logical connectives. Each formula
13+
This module defines a typeclass hierarchy for logical connectives. Each formula
1414
type registers itself as an instance of the appropriate connective class, enabling polymorphic
1515
axiom definitions and notation that work uniformly across different formula types.
1616
1717
## Design
1818
19-
The hierarchy adopts five constructors `{atom, bot, imp, and, or}`,
19+
The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`,
2020
following the operator-typeclass direction of fmontesi's PR #607 (one class per operator):
21-
- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`
22-
- **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`)
21+
- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasUntil`, `HasSince`, `HasNext`
22+
- **Bundled classes**: `PropositionalConnectives` (extends `HasBot` and `HasImp`),
23+
`FutureTemporalConnectives` (extends `PropositionalConnectives` and `HasUntil`),
24+
`LTLConnectives` (extends `FutureTemporalConnectives` and `HasNext`),
25+
`TemporalConnectives` (extends `FutureTemporalConnectives` and `HasSince`)
2326
2427
Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather
2528
than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and
2629
`φ ∨ ψ := ¬φ → ψ` are only propositionally equivalent to `∧` and `∨` in classical logic
27-
([Avigad2022]); they fail in intuitionistic and minimal logic. Making `and`
30+
([Wajsberg1938], [McKinsey1939]); they fail in intuitionistic and minimal logic. Making `and`
2831
and `or` primitive via `HasAnd`/`HasOr` supports all three logic strengths with a single
2932
typeclass hierarchy.
3033
@@ -35,6 +38,15 @@ alike, so no typeclass machinery is needed for them.
3538
## References
3639
3740
* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022]
41+
* [I. Johansson, *Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus*][Johansson1937]
42+
* [M. Wajsberg, *Untersuchungen über den Aussagenkalkül von A. Heyting*][Wajsberg1938]
43+
* [J. C. C. McKinsey,
44+
*Proof of the Independence of the Primitive Symbols of Heyting's Calculus*][McKinsey1939]
45+
* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965]
46+
* [A. S. Troelstra, D. van Dalen,
47+
*Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988]
48+
* [A. Church, *Introduction to Mathematical Logic*][Church1956]
49+
* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935]
3850
-/
3951

4052
@[expose] public section
@@ -51,6 +63,21 @@ class HasImp (F : Type*) where
5163
/-- The implication connective. -/
5264
imp : F → F → F
5365

66+
/-- A type has an until temporal operator. -/
67+
class HasUntil (F : Type*) where
68+
/-- The until temporal operator. -/
69+
untl : F → F → F
70+
71+
/-- A type has a since temporal operator. -/
72+
class HasSince (F : Type*) where
73+
/-- The since temporal operator. -/
74+
snce : F → F → F
75+
76+
/-- A type has a next-step temporal operator. -/
77+
class HasNext (F : Type*) where
78+
/-- The next-step temporal operator. -/
79+
next : F → F
80+
5481
/-- A type has a conjunction connective. -/
5582
class HasAnd (F : Type*) where
5683
/-- The conjunction connective. -/
@@ -68,4 +95,25 @@ When all four connectives are needed, use
6895
`[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/
6996
class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
7097

98+
/-- Future temporal connectives: propositional connectives plus until (no since, no next).
99+
100+
This bundle is shared by both `LTLConnectives` (which adds `HasNext`) and
101+
`TemporalConnectives` (which adds `HasSince`). Factoring out the future fragment
102+
allows code generic over future-only temporal logics without committing to past or
103+
next-step operators. -/
104+
class FutureTemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F
105+
106+
/-- LTL connectives: future temporal connectives plus a primitive next-step operator.
107+
108+
Linear Temporal Logic uses `next` as a primitive rather than deriving it from `until`
109+
(the encoding `next φ = φ U ⊥` does not hold in all models). `FutureTemporalConnectives`
110+
provides `bot`, `imp`, and `untl`; this bundle adds `next`. -/
111+
class LTLConnectives (F : Type*) extends FutureTemporalConnectives F, HasNext F
112+
113+
/-- Temporal connectives: propositional connectives plus until and since.
114+
115+
Extends `FutureTemporalConnectives` with the `since` operator, forming the standard
116+
two-sorted temporal signature (future + past). -/
117+
class TemporalConnectives (F : Type*) extends FutureTemporalConnectives F, HasSince F
118+
71119
end Cslib.Logic

‎Cslib/Logics/LTL/Syntax/Formula.lean‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
/-
2+
Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Benjamin Brast-McKie
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Cslib.Foundations.Logic.Connectives
11+
public import Cslib.Logics.Temporal.Syntax.Formula
12+
13+
/-! # LTL Formula Type
14+
15+
This module defines the formula type for Linear Temporal Logic with primitives
16+
`{atom, bot, imp, next, untl}`. The primitive `next` operator is kept separate from
17+
`untl` following the Burgess convention: in full temporal logic, `next φ` is sometimes
18+
encoded as `φ U ⊥`, but this encoding does not hold in all models (it relies on
19+
discreteness and non-triviality). An independent primitive `next` avoids this coupling.
20+
21+
## Main definitions
22+
23+
- `Formula` : Inductive type for LTL formulas with constructors
24+
`atom`, `bot`, `imp`, `next`, `untl`
25+
- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point
26+
- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points
27+
- `Formula.toTemporal` : Embedding of `LTL.Formula` into `Temporal.Formula`
28+
29+
## Notation
30+
31+
Propositional connectives (scoped to `Cslib.Logic.LTL`):
32+
- `¬` (prefix, 40) : negation (`Formula.neg`)
33+
- `∧` (infix, 36) : conjunction (`Formula.and`)
34+
- `∨` (infix, 35) : disjunction (`Formula.or`)
35+
- `→` (infix, 30) : implication (`Formula.imp`)
36+
- `↔` (infix, 30) : biconditional (`Formula.iff`)
37+
38+
Temporal operators (scoped to `Cslib.Logic.LTL`):
39+
- `U` (infix, 40) : until (`Formula.untl`)
40+
- `X` (prefix, 40) : next-step (`Formula.next`)
41+
- `𝐅` (prefix, 40) : some future / eventually (`Formula.someFuture`)
42+
- `𝐆` (prefix, 40) : all future / globally (`Formula.allFuture`)
43+
44+
## Derived Operators
45+
46+
Derived operators follow the Burgess convention: in `untl event guard`, the first argument
47+
is the **event** (holds at the witness point) and the second is the **guard** (holds at all
48+
intermediate points). `someFuture φ` is `φ U ⊤` (φ is the event, ⊤ is the trivial guard).
49+
50+
## References
51+
52+
* [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977]
53+
* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968]
54+
* [J. P. Burgess, *Axioms for Tense Logic. I. "Since" and "Until"*][Burgess1982I]
55+
* [J. P. Burgess, *Basic Tense Logic*][Burgess1984]
56+
* [M. Y. Vardi, P. Wolper,
57+
*An automata-theoretic approach to automatic program verification*][VardiWolper1986]
58+
-/
59+
60+
@[expose] public section
61+
62+
namespace Cslib.Logic.LTL
63+
64+
/-- LTL formula type. Primitives: atoms, falsum, implication, next-step, and until.
65+
66+
`next` is a primitive constructor and is not derived from `untl`. The encoding
67+
`next φ = φ U ⊥` holds on discrete non-ending sequences but fails in general temporal
68+
models; keeping `next` primitive supports broader model classes. -/
69+
inductive Formula (Atom : Type u) : Type u where
70+
/-- Atomic proposition. -/
71+
| atom (p : Atom)
72+
/-- Falsum / bottom. -/
73+
| bot
74+
/-- Implication. -/
75+
| imp (φ₁ φ₂ : Formula Atom)
76+
/-- Next-step operator: Xφ holds at t iff φ holds at t+1. -/
77+
| next (φ : Formula Atom)
78+
/-- Until temporal operator: φ₁ U φ₂ (Burgess: event U guard). -/
79+
| untl (φ₁ φ₂ : Formula Atom)
80+
deriving DecidableEq, BEq
81+
82+
/-- Negation: ¬φ := φ → ⊥ -/
83+
abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot
84+
85+
/-- Verum / top: ⊤ := ⊥ → ⊥ -/
86+
abbrev Formula.top : Formula Atom := .imp .bot .bot
87+
88+
/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/
89+
abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom :=
90+
.imp (.imp φ₁ .bot) φ₂
91+
92+
/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/
93+
abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom :=
94+
.imp (.imp φ₁ (.imp φ₂ .bot)) .bot
95+
96+
/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/
97+
abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom :=
98+
(φ₁.imp φ₂).and (φ₂.imp φ₁)
99+
100+
/-- Some future (eventually): F φ := φ U ⊤.
101+
Uses Burgess convention: φ is the event (holds at witness), ⊤ is the trivial guard. -/
102+
abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom :=
103+
.untl φ .top
104+
105+
/-- All future (globally): G φ := ¬F ¬φ -/
106+
abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom :=
107+
.neg (.someFuture (.neg φ))
108+
109+
@[inherit_doc] scoped prefix:40 "¬" => Formula.neg
110+
@[inherit_doc] scoped infix:36 " ∧ " => Formula.and
111+
@[inherit_doc] scoped infix:35 " ∨ " => Formula.or
112+
@[inherit_doc] scoped infix:30 " → " => Formula.imp
113+
@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff
114+
@[inherit_doc] scoped infix:40 " U " => Formula.untl
115+
@[inherit_doc] scoped prefix:40 "X" => Formula.next
116+
@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture
117+
@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture
118+
119+
/-- Register `LTL.Formula` as an instance of `LTLConnectives`. -/
120+
instance : LTLConnectives (Formula Atom) where
121+
bot := .bot
122+
imp := .imp
123+
untl := .untl
124+
next := .next
125+
126+
instance : Bot (Formula Atom) := ⟨.bot⟩
127+
instance : Top (Formula Atom) := ⟨.top⟩
128+
129+
/-- Embed `LTL.Formula` into `Temporal.Formula`. Translates `next φ` as `φ U ⊥`
130+
(strict until forces the immediate successor on ℕ) and `untl` as reflexive until. -/
131+
def Formula.toTemporal : Formula Atom → Temporal.Formula Atom
132+
| .atom p => .atom p
133+
| .bot => .bot
134+
| .imp φ ψ => .imp (toTemporal φ) (toTemporal ψ)
135+
| .next φ => .untl (toTemporal φ) .bot
136+
| .untl φ ψ => (toTemporal φ).reflexiveUntl (toTemporal ψ)
137+
138+
end Cslib.Logic.LTL
139+
140+
end

‎Cslib/Logics/Temporal/Syntax/Formula.lean‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
/-
2+
Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Benjamin Brast-McKie
5+
-/
6+
7+
module
8+
9+
public import Cslib.Init
10+
public import Cslib.Foundations.Logic.Connectives
11+
public import Mathlib.Order.Notation
12+
13+
/-! # Temporal Logic Formula
14+
15+
This module defines the formula type for temporal logic with primitives
16+
`{atom, bot, imp, untl, snce}`. The `untl` (until) and `snce` (since) operators are
17+
the basic future and past temporal modalities from which all derived temporal operators
18+
(globally, eventually, somePast, allPast) are obtained.
19+
20+
## Main definitions
21+
22+
- `Formula` : Inductive type for temporal logic formulas with constructors
23+
`atom`, `bot`, `imp`, `untl`, `snce`
24+
- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point
25+
- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points
26+
- `Formula.somePast` (𝐏): `φ S ⊤` — φ held at some past point
27+
- `Formula.allPast` (𝐇): `¬𝐏¬φ` — φ held at all past points
28+
29+
## References
30+
31+
* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968]
32+
* [D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, *On the temporal analysis of fairness*][GPSS1980]
33+
-/
34+
35+
@[expose] public section
36+
37+
namespace Cslib.Logic.Temporal
38+
39+
/-- Temporal logic formula type. Primitives: atoms, falsum, implication, until, and since. -/
40+
inductive Formula (Atom : Type u) : Type u where
41+
/-- Atomic proposition. -/
42+
| atom (p : Atom)
43+
/-- Falsum / bottom. -/
44+
| bot
45+
/-- Implication. -/
46+
| imp (φ₁ φ₂ : Formula Atom)
47+
/-- Until temporal operator: φ₁ U φ₂. -/
48+
| untl (φ₁ φ₂ : Formula Atom)
49+
/-- Since temporal operator: φ₁ S φ₂. -/
50+
| snce (φ₁ φ₂ : Formula Atom)
51+
deriving DecidableEq, BEq
52+
53+
/-- Negation: ¬φ := φ → ⊥ -/
54+
abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot
55+
56+
/-- Verum / top: ⊤ := ⊥ → ⊥ -/
57+
abbrev Formula.top : Formula Atom := .imp .bot .bot
58+
59+
/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/
60+
abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom :=
61+
.imp (.imp φ₁ .bot) φ₂
62+
63+
/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/
64+
abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom :=
65+
.imp (.imp φ₁ (.imp φ₂ .bot)) .bot
66+
67+
/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/
68+
abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom :=
69+
(φ₁.imp φ₂).and (φ₂.imp φ₁)
70+
71+
/-- Some future (eventually): 𝐅 φ := φ U ⊤. -/
72+
abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom :=
73+
.untl φ .top
74+
75+
/-- All future (globally): 𝐆 φ := ¬𝐅¬φ. -/
76+
abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom :=
77+
.neg (.someFuture (.neg φ))
78+
79+
/-- Some past: 𝐏 φ := φ S ⊤. -/
80+
abbrev Formula.somePast (φ : Formula Atom) : Formula Atom :=
81+
.snce φ .top
82+
83+
/-- All past: 𝐇 φ := ¬𝐏¬φ. -/
84+
abbrev Formula.allPast (φ : Formula Atom) : Formula Atom :=
85+
.neg (.somePast (.neg φ))
86+
87+
@[inherit_doc] scoped prefix:40 "¬" => Formula.neg
88+
@[inherit_doc] scoped infix:36 " ∧ " => Formula.and
89+
@[inherit_doc] scoped infix:35 " ∨ " => Formula.or
90+
@[inherit_doc] scoped infix:30 " → " => Formula.imp
91+
@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff
92+
@[inherit_doc] scoped infix:40 " U " => Formula.untl
93+
@[inherit_doc] scoped infix:40 " S " => Formula.snce
94+
@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture
95+
@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture
96+
@[inherit_doc] scoped prefix:40 "𝐏" => Formula.somePast
97+
@[inherit_doc] scoped prefix:40 "𝐇" => Formula.allPast
98+
99+
/-- Register `Temporal.Formula` as an instance of `TemporalConnectives`. -/
100+
instance : TemporalConnectives (Formula Atom) where
101+
bot := .bot
102+
imp := .imp
103+
untl := .untl
104+
snce := .snce
105+
106+
instance : Bot (Formula Atom) := ⟨.bot⟩
107+
instance : Top (Formula Atom) := ⟨.top⟩
108+
109+
/-- Reflexive until: derives non-strict until from strict until. -/
110+
abbrev Formula.reflexiveUntl (φ ψ : Formula Atom) : Formula Atom :=
111+
φ.or (ψ.and (.untl φ ψ))
112+
113+
/-- Reflexive since: derives non-strict since from strict since. -/
114+
abbrev Formula.reflexiveSnce (φ ψ : Formula Atom) : Formula Atom :=
115+
φ.or (ψ.and (.snce φ ψ))
116+
117+
end Cslib.Logic.Temporal
118+
119+
end

0 commit comments

Comments
 (0)