Skip to content

Commit dd06e39

Browse files
benbrastmckiebenbrastmckie
committed
feat(Logics/Temporal, Propositional): temporal formula type with propositional structure
1 parent 7cc0961 commit dd06e39

5 files changed

Lines changed: 388 additions & 8 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: 53 additions & 5 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
1919
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/Propositional/Defs.lean‎

Lines changed: 21 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,11 @@ Authors: Thomas Waring, Benjamin Brast-McKie
66

77
module
88

9-
import Cslib.Init
109
public import Cslib.Foundations.Logic.Connectives
1110
public import Cslib.Foundations.Logic.InferenceSystem
12-
public import Mathlib.Data.FunLike.Basic
13-
public import Mathlib.Data.Set.Basic
1411
public import Mathlib.Order.TypeTags
12+
public import Mathlib.Tactic.Finiteness.Attr
13+
public import Mathlib.Data.Set.Operations
1514

1615
/-! # Propositions and theories
1716
@@ -34,6 +33,25 @@ public import Mathlib.Order.TypeTags
3433
- `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given
3534
theory.
3635
36+
## Architecture
37+
38+
Two proof systems are defined for this propositional language:
39+
40+
- **Layer 1 — Natural Deduction** (`NaturalDeduction/Basic.lean`): a `Theory.Derivation` inductive
41+
with 10 primitive constructors (axiom, assumption, conjunction intro/elim ×2, disjunction
42+
intro ×2/elim, implication intro/elim). The theory parameter controls logic strength: `MPL`
43+
(Johansson's minimal logic, [Johansson1937]), `IPL` (intuitionistic), and `CPL` (classical).
44+
45+
- **Layer 2 — Hilbert System** (`ProofSystem/`): an axiom predicate hierarchy
46+
(`MinPropAxiom` / `IntPropAxiom` / `PropositionalAxiom`) with sequent derivability and a
47+
Hilbert-style proof-theoretic treatment.
48+
49+
- **Bridge**: `NaturalDeduction/Equivalence.lean` establishes extensional equivalence between the
50+
two proof systems for all three logic strengths, in both closed-context (`hilbert_iff_nd`,
51+
`hilbert_iff_nd_min`, `hilbert_iff_nd_int`, `hilbert_iff_nd_cl`) and context-based forms
52+
(`hilbert_iff_nd_ctx`, `hilbert_iff_nd_ctx_min`, `hilbert_iff_nd_ctx_int`,
53+
`hilbert_iff_nd_ctx_cl`).
54+
3755
## Notation
3856
3957
We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,

‎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
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)