From 7cc09612349f95ce0aa835eb70a71280ce42857b Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Tue, 16 Jun 2026 12:53:54 -0700 Subject: [PATCH 1/5] feat(Logics/Propositional): five-primitive formula type with primitive bot Add `bot` as a primitive constructor of `Proposition Atom`, eliminating all `[Bot Atom]` constraints from propositional logic signatures. - New `Connectives.lean`: typeclass hierarchy (HasBot, HasImp, HasAnd, HasOr) - `Defs.lean`: five-primitive Proposition type with derived neg, top, iff - `Basic.lean`: natural deduction with impI/impE, andI/andE1/andE2, orI1/orI2 - `Theory.lean`: remove [Bot Atom], add instIsIntuitionisticIntuitionisticCompletion - Replace German-language references with Avigad 2022, Prawitz 1965 - Semantics files deferred to follow-up PR per reviewer request Reconciles with merged PR #536 (InferenceSystem-parameterized typeclasses). Co-Authored-By: Claude Opus 4.6 (1M context) --- Cslib.lean | 1 + Cslib/Foundations/Logic/Connectives.lean | 71 +++++++++ Cslib/Logics/Propositional/Defs.lean | 105 +++++++----- .../Propositional/NaturalDeduction/Basic.lean | 149 +++++++++--------- .../NaturalDeduction/Theory.lean | 91 ++++++----- references.bib | 8 + 6 files changed, 280 insertions(+), 145 deletions(-) create mode 100644 Cslib/Foundations/Logic/Connectives.lean diff --git a/Cslib.lean b/Cslib.lean index 6e70be7b9..e1389503e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Set.Saturation public import Cslib.Foundations.Data.StackTape public import Cslib.Foundations.Lint.Basic +public import Cslib.Foundations.Logic.Connectives public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence public import Cslib.Foundations.Relation.Attr diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean new file mode 100644 index 000000000..16d13e043 --- /dev/null +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Benjamin Brast-McKie +-/ + +module + +import Cslib.Init + +/-! # Connective Typeclasses for Propositional Logic + +This module defines a typeclass hierarchy for propositional logical connectives. Each formula +type registers itself as an instance of the appropriate connective class, enabling polymorphic +axiom definitions and notation that work uniformly across different formula types. + +## Design + +The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`, +following the operator-typeclass direction of fmontesi's PR #607 (one class per operator): +- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr` +- **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`) + +Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather +than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and +`φ ∨ ψ := ¬φ → ψ` are only propositionally equivalent to `∧` and `∨` in classical logic +([Avigad2022]); they fail in intuitionistic and minimal logic. Making `and` +and `or` primitive via `HasAnd`/`HasOr` supports all three logic strengths with a single +typeclass hierarchy. + +Negation and verum stay derived: each concrete formula type defines `neg φ := φ → ⊥` and +`top := ⊥ → ⊥` as `abbrev`s, which are valid in minimal, intuitionistic, and classical logic +alike, so no typeclass machinery is needed for them. + +## References + +* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022] +-/ + +@[expose] public section + +namespace Cslib.Logic + +/-- A type has a falsum (bottom) connective. -/ +class HasBot (F : Type*) where + /-- The falsum/bottom connective. -/ + bot : F + +/-- A type has an implication connective. -/ +class HasImp (F : Type*) where + /-- The implication connective. -/ + imp : F → F → F + +/-- A type has a conjunction connective. -/ +class HasAnd (F : Type*) where + /-- The conjunction connective. -/ + and : F → F → F + +/-- A type has a disjunction connective. -/ +class HasOr (F : Type*) where + /-- The disjunction connective. -/ + or : F → F → F + +/-- Propositional connectives: falsum and implication. + +`HasAnd` and `HasOr` are defined as standalone atomic classes in this module. +When all four connectives are needed, use +`[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/ +class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F + +end Cslib.Logic diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index e9c603d91..edf49f384 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -1,37 +1,47 @@ /- -Copyright (c) 2025 Thomas Waring. All rights reserved. +Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring +Authors: Thomas Waring, Benjamin Brast-McKie -/ module +import Cslib.Init +public import Cslib.Foundations.Logic.Connectives public import Cslib.Foundations.Logic.InferenceSystem public import Mathlib.Data.FunLike.Basic -public import Mathlib.Data.Set.Image +public import Mathlib.Data.Set.Basic public import Mathlib.Order.TypeTags /-! # Propositions and theories ## Main definitions -- `Proposition` : the type of propositions over a given type of atom. This type has a `Bot` -instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited. +- `Proposition` : the type of propositions over a given type of atom. Primitives are `atom`, + `bot` (falsum), `imp` (implication), `and` (conjunction), and `or` (disjunction). Negation + (`neg`), verum (`top`), and biconditional (`iff`) are derived connectives (`abbrev`s). This + follows the natural deduction tradition ([Avigad2022]) in which `neg A` abbreviates `A → ⊥` + rather than being taken as primitive. - `Theory` : set of `Proposition`. -- `IsIntuitionistic` : a theory is intuitionistic if it contains the principle of explosion. -- `IsClassical` : an intuitionistic theory is classical if it further contains double negation -elimination. +- `IsIntuitionistic` : an inference system is intuitionistic if it derives the principle of + explosion. +- `IsClassical` : an inference system is classical if it further derives double negation + elimination. - `Proposition.subst` : replace `atom x` in a `A : Proposition Atom` with `f x`, for a function `f : Atom → Proposition Atom'`. This induces a monad structure on `Proposition`, with `pure := Proposition.atom`. `Theory` is a functor, by mapping each proposition `A ∈ T` to `f <$> A`. - `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given -theory. + theory. ## Notation We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum, conjunction, disjunction, implication and negation. + +## References + +* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022] -/ @[expose] public section @@ -42,44 +52,61 @@ variable {Atom : Type u} [DecidableEq Atom] namespace Cslib.Logic.PL -/-- Propositions. -/ +/-- Propositions. Primitives are atoms, falsum, implication, conjunction, and disjunction. -/ inductive Proposition (Atom : Type u) : Type u where /-- Propositional atoms -/ | atom (x : Atom) + /-- Falsum / bottom -/ + | bot + /-- Implication -/ + | imp (a b : Proposition Atom) /-- Conjunction -/ | and (a b : Proposition Atom) /-- Disjunction -/ | or (a b : Proposition Atom) - /-- Implication -/ - | impl (a b : Proposition Atom) deriving DecidableEq, BEq -instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩ -instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩ +/-- Negation as a derived connective: ¬A := A → ⊥ -/ +abbrev Proposition.neg : Proposition Atom → Proposition Atom := (Proposition.imp · .bot) -/-- We view negation as a defined connective ~A := A → ⊥ -/ -abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥) +/-- Verum / top as a derived connective: ⊤ := ⊥ → ⊥ -/ +abbrev Proposition.top : Proposition Atom := .imp .bot .bot -/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ -abbrev Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default) +/-- Biconditional as a derived connective: A ↔ B := (A → B) ∧ (B → A) -/ +abbrev Proposition.iff (A B : Proposition Atom) : Proposition Atom := + (A.imp B).and (B.imp A) -instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩ - -example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl +instance : Bot (Proposition Atom) := ⟨.bot⟩ +instance : Top (Proposition Atom) := ⟨.top⟩ @[inherit_doc] scoped infix:36 " ∧ " => Proposition.and @[inherit_doc] scoped infix:35 " ∨ " => Proposition.or -@[inherit_doc] scoped infix:30 " → " => Proposition.impl +@[inherit_doc] scoped infix:30 " → " => Proposition.imp +@[inherit_doc] scoped infix:20 " ↔ " => Proposition.iff @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg +/-- Register `Proposition` as an instance of `PropositionalConnectives`. -/ +instance : PropositionalConnectives (Proposition Atom) where + bot := .bot + imp := .imp + +/-- Register `HasAnd` instance for `Proposition`. -/ +instance : HasAnd (Proposition Atom) where + and := .and + +/-- Register `HasOr` instance for `Proposition`. -/ +instance : HasOr (Proposition Atom) where + or := .or + /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic language. -/ def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') : Proposition Atom → Proposition Atom' | atom x => f x - | and A B => (A.subst f) ∧ (B.subst f) - | or A B => (A.subst f) ∨ (B.subst f) - | impl A B => (A.subst f) → (B.subst f) + | bot => .bot + | imp A B => .imp (A.subst f) (B.subst f) + | and A B => .and (A.subst f) (B.subst f) + | or A B => .or (A.subst f) (B.subst f) -- This is probably a lawful monad, but that doesn't seem to be important. instance : Monad Proposition where @@ -99,24 +126,26 @@ instance : Functor Theory where map f := Set.image (f <$> ·) /-- The empty theory corresponds to minimal propositional logic. -/ -abbrev MPL (Atom : Type u) : Theory (Atom) := ∅ +abbrev MPL : Theory (Atom) := ∅ /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/ -abbrev IPL (Atom : Type u) [Bot Atom] : Theory Atom := {⊥ → A | A : Proposition Atom} +abbrev IPL : Theory Atom := + Set.range (Proposition.imp ⊥ ·) omit [DecidableEq Atom] in -lemma efq_mem_ipl [Bot Atom] (A : Proposition Atom) : (⊥ → A) ∈ IPL Atom := ⟨A, rfl⟩ - -/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/ -@[reducible] -def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) := - (WithBot.some <$> T) ∪ IPL (WithBot Atom) +lemma efq_mem_ipl (A : Proposition Atom) : (⊥ → A) ∈ IPL (Atom := Atom) := ⟨A, rfl⟩ /-- Classical logic further adds double negation elimination. -/ -abbrev CPL (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom} +abbrev CPL : Theory Atom := + Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A) omit [DecidableEq Atom] in -lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩ +lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩ + +/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/ +@[reducible] +def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) := + (WithBot.some <$> T) ∪ IPL open InferenceSystem @@ -124,16 +153,16 @@ open InferenceSystem generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an implication connective. -/ @[scoped grind] -class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*) +class IsIntuitionistic (Atom : Type u) (S : Type*) [InferenceSystem S (Proposition Atom)] where - /-- The principle of explosion (ex falso quolibet). -/ + /-- The principle of explosion (ex falso quodlibet). -/ efq (A : Proposition Atom) : S⇓(⊥ → A) /-- An inference system is classical if it validates double-negation elimination. TODO: this should be generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an implication connective. -/ @[scoped grind] -class IsClassical (Atom : Type u) [Bot Atom] (S : Type*) +class IsClassical (Atom : Type u) (S : Type*) [InferenceSystem S (Proposition Atom)] where /-- Double-negation elimination. -/ dne (A : Proposition Atom) : S⇓(¬¬A → A) diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index 560ecb69e..51ac2669a 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2025 Thomas Waring. All rights reserved. +Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring +Authors: Thomas Waring, Benjamin Brast-McKie -/ module @@ -42,21 +42,20 @@ abbreviates a derivation of `A` in the empty context: `T⇓(∅ ⊢ A)`. ## Implementation notes -We formalise here a single type of derivations, meaning there is a single collection of inference -rules (those for minimal logic). The extension to intuitionistic and classical logic are modelled -by adding *axioms* --- for instance, intuitionistic derivations are allowed to appeal to axioms of -the form `⊥ → A` for any proposition `A`. This differs from many on-paper presentations, which add -that principle as a deduction rule: from `Γ ⊢ ⊥` derive `Γ ⊢ A`. Discussion on proper way to -capture such developments in cslib is ongoing, see the following -[zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Logic/with/585843520). +The primitive inference rules are: axiom (from theory), assumption (from context), +conjunction introduction and elimination (×2), disjunction introduction (×2) and elimination, +and implication introduction and elimination — 10 constructors in total. Ex falso quodlibet +(bottom elimination) is a derived rule requiring `[IsIntuitionistic T]`. + +Logic strength is controlled by the theory parameter: +- `MPL` (minimal propositional logic, see [Avigad2022] §3): no axioms beyond the + 10 primitive rules; bottom has no special status. +- `IPL` (intuitionistic propositional logic): adds the principle of explosion `⊥ → A`. +- `CPL` (classical propositional logic): adds double negation elimination `¬¬A → A`. ## References -- Dag Prawitz, *Natural Deduction: a proof-theoretical study*. -- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely -presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*, and -in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (Suggestions of better -references welcome!) +* [J. Avigad, *Mathematical Logic and Computation*][Avigad2022] -/ @[expose] public section @@ -83,31 +82,38 @@ abbrev Sequent {Atom} := Ctx Atom × Proposition Atom scoped notation Γ:60 " ⊢ " A => (⟨Γ, A⟩ : Sequent) /-- A `T`-derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ, -possibly appealing to axioms from `T`. -/ +possibly appealing to axioms from `T`. Primitives: axiom, assumption, conjunction intro/elim, +disjunction intro/elim, and implication intro/elim. +Ex falso quodlibet (bottom elimination) is a derived rule requiring `[IsIntuitionistic T]`. -/ inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom → Type u where /-- Axiom -/ | ax {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ T) : Derivation Γ A /-- Assumption -/ | ass {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ Γ) : Derivation Γ A /-- Conjunction introduction -/ - | andI {Γ : Ctx Atom} {A B : Proposition Atom} : + | andI {A B : Proposition Atom} (Γ : Ctx Atom) : Derivation Γ A → Derivation Γ B → Derivation Γ (A ∧ B) - /-- Conjunction elimination left -/ - | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ A - /-- Conjunction elimination right -/ - | andE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ B - /-- Disjunction introduction left -/ - | orI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ (A ∨ B) - /-- Disjunction introduction right -/ - | orI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ B → Derivation Γ (A ∨ B) + /-- Left conjunction elimination -/ + | andE1 {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation Γ (A ∧ B) → Derivation Γ A + /-- Right conjunction elimination -/ + | andE2 {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation Γ (A ∧ B) → Derivation Γ B + /-- Left disjunction introduction -/ + | orI1 {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation Γ A → Derivation Γ (A ∨ B) + /-- Right disjunction introduction -/ + | orI2 {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation Γ B → Derivation Γ (A ∨ B) /-- Disjunction elimination -/ - | orE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation Γ (A ∨ B) → - Derivation (insert A Γ) C → Derivation (insert B Γ) C → Derivation Γ C + | orE {A B C : Proposition Atom} (Γ : Ctx Atom) : + Derivation Γ (A ∨ B) → Derivation (insert A Γ) C → Derivation (insert B Γ) C → + Derivation Γ C /-- Implication introduction -/ - | implI {A B : Proposition Atom} (Γ : Ctx Atom) : + | impI {A B : Proposition Atom} (Γ : Ctx Atom) : Derivation (insert A Γ) B → Derivation Γ (A → B) - /-- Implication elimination -/ - | implE {Γ : Ctx Atom} {A B : Proposition Atom} : + /-- Implication elimination (modus ponens) -/ + | impE {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A → B) → Derivation Γ A → Derivation Γ B /-- Inference system for derivations under the theory `T`. -/ @@ -156,7 +162,7 @@ theorem Theory.equiv_iff {A B : Proposition Atom} : exact ⟨D, E⟩ /-- Minimally equivalent propositions. -/ -abbrev Equiv : Proposition Atom → Proposition Atom → Prop := (MPL Atom).Equiv +abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv @[inherit_doc] scoped infix:29 " ≡ " => Equiv @@ -170,17 +176,17 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : T.Derivation Γ A → T'.Derivation Δ A | ax hA => ax <| hTheory hA | ass hA => ass <| hCtx hA - | andI D D' => andI (D.weak hTheory hCtx) (D'.weak hTheory hCtx) - | andE₁ D => andE₁ <| D.weak hTheory hCtx - | andE₂ D => andE₂ <| D.weak hTheory hCtx - | orI₁ D => orI₁ <| D.weak hTheory hCtx - | orI₂ D => orI₂ <| D.weak hTheory hCtx - | orE D D' D'' => - orE (D.weak hTheory hCtx) - (D'.weak hTheory <| Finset.insert_subset_insert _ hCtx) - (D''.weak hTheory <| Finset.insert_subset_insert _ hCtx) - | @implI _ _ _ A B Γ D => implI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx - | implE D D' => implE (D.weak hTheory hCtx) (D'.weak hTheory hCtx) + | @andI _ _ _ A B Γ D₁ D₂ => andI Δ (D₁.weak hTheory hCtx) (D₂.weak hTheory hCtx) + | @andE1 _ _ _ A B Γ D => andE1 Δ (D.weak hTheory hCtx) + | @andE2 _ _ _ A B Γ D => andE2 Δ (D.weak hTheory hCtx) + | @orI1 _ _ _ A B Γ D => orI1 Δ (D.weak hTheory hCtx) + | @orI2 _ _ _ A B Γ D => orI2 Δ (D.weak hTheory hCtx) + | @orE _ _ _ _ _ _ _ D DA DB => + orE Δ (D.weak hTheory hCtx) + (DA.weak hTheory (Finset.insert_subset_insert _ hCtx)) + (DB.weak hTheory (Finset.insert_subset_insert _ hCtx)) + | @impI _ _ _ A B Γ D => impI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx + | impE D D' => impE (D.weak hTheory hCtx) (D'.weak hTheory hCtx) /-- Weakening the theory only. -/ def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom} @@ -213,9 +219,9 @@ substitution, which would replace appeals to `A` in `E` by the whole derivation -/ def Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} (D : T⇓(Γ ⊢ A)) (E : T⇓(insert A Δ ⊢ B)) : T⇓((Γ ∪ Δ) ⊢ B) := by - refine implE (A := A) ?_ (D.weakCtx Finset.subset_union_left) + refine impE (A := A) ?_ (D.weakCtx Finset.subset_union_left) have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind - exact implI (Γ ∪ Δ) <| E.weakCtx this + exact impI (Γ ∪ Δ) <| E.weakCtx this /-- Proof irrelevant cut rule. -/ theorem DerivableIn.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} : @@ -249,22 +255,22 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom} exact (Ds B h).weakCtx <| by grind case neg h => exact ass <| by grind - | andI E E' => andI (E.subs Ds) (E'.subs Ds) - | andE₁ E => andE₁ <| E.subs Ds - | andE₂ E => andE₂ <| E.subs Ds - | orI₁ E => orI₁ <| E.subs Ds - | orI₂ E => orI₂ <| E.subs Ds - | @orE _ _ _ _ C C' _ E E' E'' .. => by - apply orE (E.subs Ds) - · rw [show insert C (Γ \ Γ' ∪ Δ) = (insert C Γ \ Γ') ∪ insert C Δ by grind] - exact E'.subs Ds |>.weakCtx (by grind) - · rw [show insert C' (Γ \ Γ' ∪ Δ) = (insert C' Γ \ Γ') ∪ insert C' Δ by grind] - exact E''.subs Ds |>.weakCtx (by grind) - | @implI _ _ _ A' _ _ E .. => by - apply implI + | @andI _ _ _ A' B' Γ E₁ E₂ => andI _ (E₁.subs Ds) (E₂.subs Ds) + | @andE1 _ _ _ A' B' Γ E => andE1 _ (E.subs Ds) + | @andE2 _ _ _ A' B' Γ E => andE2 _ (E.subs Ds) + | @orI1 _ _ _ A' B' Γ E => orI1 _ (E.subs Ds) + | @orI2 _ _ _ A' B' Γ E => orI2 _ (E.subs Ds) + | @orE _ _ _ A' B' C' Γ E EA EB => by + apply orE _ (E.subs Ds) + · rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind] + exact EA.subs Ds |>.weakCtx (by grind) + · rw [show insert B' (Γ \ Γ' ∪ Δ) = (insert B' Γ \ Γ') ∪ insert B' Δ by grind] + exact EB.subs Ds |>.weakCtx (by grind) + | @impI _ _ _ A' _ _ E .. => by + apply impI rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind] exact E.subs Ds |>.weakCtx (by grind) - | implE E E' => implE (E.subs Ds) (E'.subs Ds) + | impE E E' => impE (E.subs Ds) (E'.subs Ds) /-- Transport a derivation along a substitution of atoms. -/ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] @@ -272,16 +278,17 @@ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decida T.Derivation Γ B → (T.subst f).Derivation (Γ.subst f) (B >>= f) | ax h => ax <| Set.mem_image_of_mem (· >>= f) h | ass h => ass <| Finset.mem_image_of_mem (· >>= f) h - | andI D E => andI (D.substAtom f) (E.substAtom f) - | andE₁ D => andE₁ (D.substAtom f) - | andE₂ D => andE₂ (D.substAtom f) - | orI₁ D => orI₁ (D.substAtom f) - | orI₂ D => orI₂ (D.substAtom f) - | orE D E E' => orE (D.substAtom f) - ((Finset.image_insert (· >>= f) _ _) ▸ E.substAtom f) - ((Finset.image_insert (· >>= f) _ _) ▸ E'.substAtom f) - | implI _ D => implI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f) - | implE D E => implE (D.substAtom f) (E.substAtom f) + | andI _ D₁ D₂ => andI _ (D₁.substAtom f) (D₂.substAtom f) + | andE1 _ D => andE1 _ (D.substAtom f) + | andE2 _ D => andE2 _ (D.substAtom f) + | orI1 _ D => orI1 _ (D.substAtom f) + | orI2 _ D => orI2 _ (D.substAtom f) + | orE _ D DA DB => + orE _ (D.substAtom f) + ((Finset.image_insert (· >>= f) _ _) ▸ (DA.substAtom f)) + ((Finset.image_insert (· >>= f) _ _) ▸ (DB.substAtom f)) + | impI _ D => impI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f) + | impE D E => impE (D.substAtom f) (E.substAtom f) theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom'] {T : Theory Atom} @@ -292,12 +299,12 @@ theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decidabl /-! ### Properties of equivalence -/ /-- A derivation of the canonical tautology. -/ -def Theory.derivationTop [Inhabited Atom] : T⇓(⊤ : Proposition Atom) := - implI ∅ <| ass <| by grind +def Theory.derivationTop : T⇓(⊤ : Proposition Atom) := + impI ∅ <| ass <| by grind -theorem derivableIn_top [Inhabited Atom] : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩ +theorem derivableIn_top : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩ -theorem derivable_iff_equiv_top [Inhabited Atom] (A : Proposition Atom) : +theorem derivable_iff_equiv_top (A : Proposition Atom) : DerivableIn T A ↔ A ≡[T] ⊤ := by constructor <;> intro h · refine ⟨derivationTop.weakCtx <| by grind, ?_⟩ diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean index 8cdaa806d..cb75cc979 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2025 Thomas Waring. All rights reserved. +Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring +Authors: Thomas Waring, Benjamin Brast-McKie -/ module @@ -9,9 +9,12 @@ public import Cslib.Logics.Propositional.NaturalDeduction.Basic /-! # Results on propositional theories -In this file we prove the expected results that `IPL Atom` is an intuitionistic theory, and -`CPL Atom` is a classical theory. We provide derived rules for common intuitionistic and classical +In this file we prove the expected results that `IPL` is an intuitionistic theory, and +`CPL` is a classical theory. We provide derived rules for common intuitionistic and classical proof patterns. + +Since `Proposition` has `bot` as a primitive constructor, no `[Bot Atom]` constraint is needed: +`⊥ : Proposition Atom` is always available as `.bot`. -/ @[expose] public section @@ -22,13 +25,24 @@ namespace Cslib.Logic.PL open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical -variable {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom} +variable {Atom : Type u} [DecidableEq Atom] {T : Theory Atom} namespace Theory -instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where +/-- `IPL` is intuitionistic: it contains `⊥ → A` for all `A`. -/ +instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL (Atom := Atom)) where efq A := ax (efq_mem_ipl A) +/-- `CPL` is classical: it contains `¬¬A → A` for all `A`. -/ +instance instIsClassicalCPL : IsClassical Atom (CPL (Atom := Atom)) where + dne A := ax (dne_mem_cpl A) + +/-- The intuitionistic completion of any theory is intuitionistic. -/ +instance instIsIntuitionisticIntuitionisticCompletion [DecidableEq (WithBot Atom)] + (T : Theory Atom) : + IsIntuitionistic (WithBot Atom) T.intuitionisticCompletion where + efq A := ax (Set.mem_union_right _ (efq_mem_ipl A)) + /-- Derivation of efq in an arbitrary context. -/ def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom) : T⇓(Γ ⊢ ⊥ → A) := (efq A : T⇓(⊥ → A)).weakCtx (Finset.empty_subset Γ) @@ -36,66 +50,71 @@ def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Propo /-- Efq as a derived rule. -/ def IsIntuitionistic.efqRule [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom) (D : T⇓(Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) := - implE (A := ⊥) (efqCtx Γ A) D + impE (A := ⊥) (efqCtx Γ A) D /-- Prove any proposition from contradictory hypotheses. -/ def IsIntuitionistic.contra [IsIntuitionistic Atom T] {Γ : Ctx Atom} (A B : Proposition Atom) (hΓ : A ∈ Γ) (hΓ' : (¬A) ∈ Γ) : T⇓(Γ ⊢ B) := - efqRule Γ B <| implE (ass hΓ') (ass hΓ) - -instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where - dne A := ax (dne_mem_cpl A) + efqRule Γ B <| impE (ass hΓ') (ass hΓ) /-- Proof by contradiction as a derived rule. -/ def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition Atom} (D : T⇓(insert (¬ A) Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) := - implE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weakCtx <| Finset.empty_subset ..) D.implI + impE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weakCtx <| Finset.empty_subset ..) D.impI instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where - efq A := implI _ <| byContra <| ass (by grind) + efq A := impI _ <| byContra <| ass (by grind) /-- Law of excluded middle in a classical theory. -/ def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬ A) := by apply byContra - apply implE (ass <| Finset.mem_insert_self ..) - apply orI₂; apply implI - apply implE (A := A ∨ ¬ A) (ass <| by grind) - exact orI₁ <| ass <| Finset.mem_insert_self .. + apply impE (ass <| Finset.mem_insert_self ..) + apply orI2 + apply impI + apply impE (A := A ∨ ¬ A) (ass <| by grind) + apply orI1 + exact ass <| Finset.mem_insert_self .. /-- Pierce's law in a classical theory. -/ def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A → B) → A) → A) := by - apply implI; apply byContra - apply implE (ass <| Finset.mem_insert_self ..) - apply implE (A := A → B) (ass <| by grind); apply implI + apply impI; apply byContra + apply impE (ass <| Finset.mem_insert_self ..) + apply impE (A := A → B) (ass <| by grind); apply impI apply contra A B <;> grind /-- The axiom system consisting of instances of LEM. -/ -def LEM (Atom : Type u) [Bot Atom] : Theory Atom := {A ∨ ¬ A | A : Proposition Atom} +def LEM : Theory Atom := {A ∨ ¬ A | A : Proposition Atom} omit [DecidableEq Atom] in -lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩ +lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM (Atom := Atom) := ⟨A, rfl⟩ /-- The axiom system consisting of instances of Pierce's law. -/ -def Pierce (Atom : Type u) : Theory Atom := +def Pierce : Theory Atom := {((A → B) → A) → A | (A : Proposition Atom) (B : Proposition Atom)} -omit [DecidableEq Atom] [Bot Atom] in -lemma pierce_mem_pierce (A B : Proposition Atom) : (((A → B) → A) → A) ∈ Pierce Atom := ⟨A, B, rfl⟩ +omit [DecidableEq Atom] in +lemma pierce_mem_pierce (A B : Proposition Atom) : + (((A → B) → A) → A) ∈ Pierce (Atom := Atom) := ⟨A, B, rfl⟩ -instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where +instance instIsClassicalLEM : IsClassical Atom (LEM ∪ IPL : Theory Atom) where dne A := by - apply implI - apply orE (ax <| Set.mem_union_left _ <| lem_mem_lem A) + apply impI + apply orE + · exact ax <| Set.mem_union_left _ <| lem_mem_lem A · exact ass (Finset.mem_insert_self A _) - · apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A)) - apply implE (A := ¬ A) <;> exact ass (by grind) + · apply impE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A)) + apply impE (A := ¬ A) + · exact ass (Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _))) + · exact ass (Finset.mem_insert_self _ _) -instance instIsClassicalPierce : IsClassical Atom (Pierce Atom ∪ IPL Atom : Theory Atom) where +instance instIsClassicalPierce : IsClassical Atom (Pierce ∪ IPL : Theory Atom) where dne A := by - apply implI - apply implE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥) - apply implI - apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A)) - apply implE (A := ¬ A) <;> exact ass (by grind) + apply impI + apply impE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥) + apply impI + apply impE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A)) + apply impE (A := ¬ A) + · exact ass (Finset.mem_insert.mpr (Or.inr (Finset.mem_insert_self _ _))) + · exact ass (Finset.mem_insert_self _ _) end Cslib.Logic.PL.Theory diff --git a/references.bib b/references.bib index 973371b65..8b4450757 100644 --- a/references.bib +++ b/references.bib @@ -1,3 +1,11 @@ +@book{Avigad2022, + author = {Jeremy Avigad}, + title = {Mathematical Logic and Computation}, + publisher = {Cambridge University Press}, + year = {2022}, + isbn = {978-1-108-84072-1} +} + @inproceedings{Aceto1999, author = {Luca Aceto and Anna Ing{\'{o}}lfsd{\'{o}}ttir}, From 194f0c3d7a6218b51a72b731e0dbc5a0e0e246f6 Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Wed, 17 Jun 2026 10:25:41 -0700 Subject: [PATCH 2/5] doc: fix docstrings for primitive bot perspective MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Update intuitionisticCompletion docstring — the old wording "Attach a bottom element" was misleading since bot is already a constructor. Change "five-primitive propositional signature" to "five constructors" in Connectives.lean to avoid conflating generators with operations. Co-Authored-By: Claude Opus 4.6 (1M context) --- Cslib/Foundations/Logic/Connectives.lean | 2 +- Cslib/Logics/Propositional/Defs.lean | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean index 16d13e043..18a847236 100644 --- a/Cslib/Foundations/Logic/Connectives.lean +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -16,7 +16,7 @@ axiom definitions and notation that work uniformly across different formula type ## Design -The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`, +The hierarchy adopts five constructors `{atom, bot, imp, and, or}`, following the operator-typeclass direction of fmontesi's PR #607 (one class per operator): - **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr` - **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`) diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index edf49f384..2242eaa90 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -142,7 +142,9 @@ abbrev CPL : Theory Atom := omit [DecidableEq Atom] in lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩ -/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/ +/-- Extend a theory `T` to an intuitionistic theory over a larger atom type by adding the principle +of explosion. The atom type is extended with `WithBot` to ensure the result is over a strictly +larger language. -/ @[reducible] def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) := (WithBot.some <$> T) ∪ IPL From 3e11b1f5bd17c740fcdf99daa0203dce41350c22 Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Wed, 17 Jun 2026 16:44:05 -0700 Subject: [PATCH 3/5] 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) --- Cslib.lean | 2 + Cslib/Foundations/Logic/Connectives.lean | 60 +++++++++- Cslib/Logics/LTL/Syntax/Formula.lean | 140 ++++++++++++++++++++++ Cslib/Logics/Temporal/Syntax/Formula.lean | 119 ++++++++++++++++++ references.bib | 133 ++++++++++++++++++++ 5 files changed, 448 insertions(+), 6 deletions(-) create mode 100644 Cslib/Logics/LTL/Syntax/Formula.lean create mode 100644 Cslib/Logics/Temporal/Syntax/Formula.lean diff --git a/Cslib.lean b/Cslib.lean index e1389503e..e05658900 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -137,6 +137,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic public import Cslib.Logics.HML.Basic public import Cslib.Logics.HML.LogicalEquivalence +public import Cslib.Logics.LTL.Syntax.Formula public import Cslib.Logics.LinearLogic.CLL.Basic public import Cslib.Logics.LinearLogic.CLL.CutElimination public import Cslib.Logics.LinearLogic.CLL.EtaExpansion @@ -149,6 +150,7 @@ public import Cslib.Logics.Modal.LogicalEquivalence public import Cslib.Logics.Propositional.Defs public import Cslib.Logics.Propositional.NaturalDeduction.Basic public import Cslib.Logics.Propositional.NaturalDeduction.Theory +public import Cslib.Logics.Temporal.Syntax.Formula public import Cslib.MachineLearning.PACLearning.Defs public import Cslib.MachineLearning.PACLearning.VCDimension public import Cslib.MachineLearning.PACLearning.VersionSpace diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean index 18a847236..17ffa6cef 100644 --- a/Cslib/Foundations/Logic/Connectives.lean +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -8,23 +8,26 @@ module import Cslib.Init -/-! # Connective Typeclasses for Propositional Logic +/-! # Connective Typeclasses for Propositional and Temporal Logic -This module defines a typeclass hierarchy for propositional logical connectives. Each formula +This module defines a typeclass hierarchy for logical connectives. Each formula type registers itself as an instance of the appropriate connective class, enabling polymorphic axiom definitions and notation that work uniformly across different formula types. ## Design -The hierarchy adopts five constructors `{atom, bot, imp, and, or}`, +The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`, following the operator-typeclass direction of fmontesi's PR #607 (one class per operator): -- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr` -- **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`) +- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasUntil`, `HasSince`, `HasNext` +- **Bundled classes**: `PropositionalConnectives` (extends `HasBot` and `HasImp`), + `FutureTemporalConnectives` (extends `PropositionalConnectives` and `HasUntil`), + `LTLConnectives` (extends `FutureTemporalConnectives` and `HasNext`), + `TemporalConnectives` (extends `FutureTemporalConnectives` and `HasSince`) Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and `φ ∨ ψ := ¬φ → ψ` are only propositionally equivalent to `∧` and `∨` in classical logic -([Avigad2022]); they fail in intuitionistic and minimal logic. Making `and` +([Wajsberg1938], [McKinsey1939]); they fail in intuitionistic and minimal logic. Making `and` and `or` primitive via `HasAnd`/`HasOr` supports all three logic strengths with a single typeclass hierarchy. @@ -35,6 +38,15 @@ alike, so no typeclass machinery is needed for them. ## References * [J. Avigad, *Mathematical Logic and Computation*][Avigad2022] +* [I. Johansson, *Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus*][Johansson1937] +* [M. Wajsberg, *Untersuchungen über den Aussagenkalkül von A. Heyting*][Wajsberg1938] +* [J. C. C. McKinsey, + *Proof of the Independence of the Primitive Symbols of Heyting's Calculus*][McKinsey1939] +* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965] +* [A. S. Troelstra, D. van Dalen, + *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988] +* [A. Church, *Introduction to Mathematical Logic*][Church1956] +* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935] -/ @[expose] public section @@ -51,6 +63,21 @@ class HasImp (F : Type*) where /-- The implication connective. -/ imp : F → F → F +/-- A type has an until temporal operator. -/ +class HasUntil (F : Type*) where + /-- The until temporal operator. -/ + untl : F → F → F + +/-- A type has a since temporal operator. -/ +class HasSince (F : Type*) where + /-- The since temporal operator. -/ + snce : F → F → F + +/-- A type has a next-step temporal operator. -/ +class HasNext (F : Type*) where + /-- The next-step temporal operator. -/ + next : F → F + /-- A type has a conjunction connective. -/ class HasAnd (F : Type*) where /-- The conjunction connective. -/ @@ -68,4 +95,25 @@ When all four connectives are needed, use `[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/ class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F +/-- Future temporal connectives: propositional connectives plus until (no since, no next). + +This bundle is shared by both `LTLConnectives` (which adds `HasNext`) and +`TemporalConnectives` (which adds `HasSince`). Factoring out the future fragment +allows code generic over future-only temporal logics without committing to past or +next-step operators. -/ +class FutureTemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F + +/-- LTL connectives: future temporal connectives plus a primitive next-step operator. + +Linear Temporal Logic uses `next` as a primitive rather than deriving it from `until` +(the encoding `next φ = φ U ⊥` does not hold in all models). `FutureTemporalConnectives` +provides `bot`, `imp`, and `untl`; this bundle adds `next`. -/ +class LTLConnectives (F : Type*) extends FutureTemporalConnectives F, HasNext F + +/-- Temporal connectives: propositional connectives plus until and since. + +Extends `FutureTemporalConnectives` with the `since` operator, forming the standard +two-sorted temporal signature (future + past). -/ +class TemporalConnectives (F : Type*) extends FutureTemporalConnectives F, HasSince F + end Cslib.Logic diff --git a/Cslib/Logics/LTL/Syntax/Formula.lean b/Cslib/Logics/LTL/Syntax/Formula.lean new file mode 100644 index 000000000..82d692e41 --- /dev/null +++ b/Cslib/Logics/LTL/Syntax/Formula.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Benjamin Brast-McKie +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Logic.Connectives +public import Cslib.Logics.Temporal.Syntax.Formula + +/-! # LTL Formula Type + +This module defines the formula type for Linear Temporal Logic with primitives +`{atom, bot, imp, next, untl}`. The primitive `next` operator is kept separate from +`untl` following the Burgess convention: in full temporal logic, `next φ` is sometimes +encoded as `φ U ⊥`, but this encoding does not hold in all models (it relies on +discreteness and non-triviality). An independent primitive `next` avoids this coupling. + +## Main definitions + +- `Formula` : Inductive type for LTL formulas with constructors + `atom`, `bot`, `imp`, `next`, `untl` +- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point +- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points +- `Formula.toTemporal` : Embedding of `LTL.Formula` into `Temporal.Formula` + +## Notation + +Propositional connectives (scoped to `Cslib.Logic.LTL`): +- `¬` (prefix, 40) : negation (`Formula.neg`) +- `∧` (infix, 36) : conjunction (`Formula.and`) +- `∨` (infix, 35) : disjunction (`Formula.or`) +- `→` (infix, 30) : implication (`Formula.imp`) +- `↔` (infix, 30) : biconditional (`Formula.iff`) + +Temporal operators (scoped to `Cslib.Logic.LTL`): +- `U` (infix, 40) : until (`Formula.untl`) +- `X` (prefix, 40) : next-step (`Formula.next`) +- `𝐅` (prefix, 40) : some future / eventually (`Formula.someFuture`) +- `𝐆` (prefix, 40) : all future / globally (`Formula.allFuture`) + +## Derived Operators + +Derived operators follow the Burgess convention: in `untl event guard`, the first argument +is the **event** (holds at the witness point) and the second is the **guard** (holds at all +intermediate points). `someFuture φ` is `φ U ⊤` (φ is the event, ⊤ is the trivial guard). + +## References + +* [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977] +* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968] +* [J. P. Burgess, *Axioms for Tense Logic. I. "Since" and "Until"*][Burgess1982I] +* [J. P. Burgess, *Basic Tense Logic*][Burgess1984] +* [M. Y. Vardi, P. Wolper, + *An automata-theoretic approach to automatic program verification*][VardiWolper1986] +-/ + +@[expose] public section + +namespace Cslib.Logic.LTL + +/-- LTL formula type. Primitives: atoms, falsum, implication, next-step, and until. + +`next` is a primitive constructor and is not 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. -/ +inductive Formula (Atom : Type u) : Type u where + /-- Atomic proposition. -/ + | atom (p : Atom) + /-- Falsum / bottom. -/ + | bot + /-- Implication. -/ + | imp (φ₁ φ₂ : Formula Atom) + /-- Next-step operator: Xφ holds at t iff φ holds at t+1. -/ + | next (φ : Formula Atom) + /-- Until temporal operator: φ₁ U φ₂ (Burgess: event U guard). -/ + | untl (φ₁ φ₂ : Formula Atom) +deriving DecidableEq, BEq + +/-- Negation: ¬φ := φ → ⊥ -/ +abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot + +/-- Verum / top: ⊤ := ⊥ → ⊥ -/ +abbrev Formula.top : Formula Atom := .imp .bot .bot + +/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/ +abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom := + .imp (.imp φ₁ .bot) φ₂ + +/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/ +abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom := + .imp (.imp φ₁ (.imp φ₂ .bot)) .bot + +/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/ +abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom := + (φ₁.imp φ₂).and (φ₂.imp φ₁) + +/-- Some future (eventually): F φ := φ U ⊤. + Uses Burgess convention: φ is the event (holds at witness), ⊤ is the trivial guard. -/ +abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom := + .untl φ .top + +/-- All future (globally): G φ := ¬F ¬φ -/ +abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom := + .neg (.someFuture (.neg φ)) + +@[inherit_doc] scoped prefix:40 "¬" => Formula.neg +@[inherit_doc] scoped infix:36 " ∧ " => Formula.and +@[inherit_doc] scoped infix:35 " ∨ " => Formula.or +@[inherit_doc] scoped infix:30 " → " => Formula.imp +@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff +@[inherit_doc] scoped infix:40 " U " => Formula.untl +@[inherit_doc] scoped prefix:40 "X" => Formula.next +@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture +@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture + +/-- Register `LTL.Formula` as an instance of `LTLConnectives`. -/ +instance : LTLConnectives (Formula Atom) where + bot := .bot + imp := .imp + untl := .untl + next := .next + +instance : Bot (Formula Atom) := ⟨.bot⟩ +instance : Top (Formula Atom) := ⟨.top⟩ + +/-- Embed `LTL.Formula` into `Temporal.Formula`. Translates `next φ` as `φ U ⊥` +(strict until forces the immediate successor on ℕ) and `untl` as reflexive until. -/ +def Formula.toTemporal : Formula Atom → Temporal.Formula Atom + | .atom p => .atom p + | .bot => .bot + | .imp φ ψ => .imp (toTemporal φ) (toTemporal ψ) + | .next φ => .untl (toTemporal φ) .bot + | .untl φ ψ => (toTemporal φ).reflexiveUntl (toTemporal ψ) + +end Cslib.Logic.LTL + +end diff --git a/Cslib/Logics/Temporal/Syntax/Formula.lean b/Cslib/Logics/Temporal/Syntax/Formula.lean new file mode 100644 index 000000000..07060dc29 --- /dev/null +++ b/Cslib/Logics/Temporal/Syntax/Formula.lean @@ -0,0 +1,119 @@ +/- +Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Benjamin Brast-McKie +-/ + +module + +public import Cslib.Init +public import Cslib.Foundations.Logic.Connectives +public import Mathlib.Order.Notation + +/-! # Temporal Logic Formula + +This module defines the formula type for temporal logic with primitives +`{atom, bot, imp, untl, snce}`. The `untl` (until) and `snce` (since) operators are +the basic future and past temporal modalities from which all derived temporal operators +(globally, eventually, somePast, allPast) are obtained. + +## Main definitions + +- `Formula` : Inductive type for temporal logic formulas with constructors + `atom`, `bot`, `imp`, `untl`, `snce` +- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point +- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points +- `Formula.somePast` (𝐏): `φ S ⊤` — φ held at some past point +- `Formula.allPast` (𝐇): `¬𝐏¬φ` — φ held at all past points + +## References + +* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968] +* [D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, *On the temporal analysis of fairness*][GPSS1980] +-/ + +@[expose] public section + +namespace Cslib.Logic.Temporal + +/-- Temporal logic formula type. Primitives: atoms, falsum, implication, until, and since. -/ +inductive Formula (Atom : Type u) : Type u where + /-- Atomic proposition. -/ + | atom (p : Atom) + /-- Falsum / bottom. -/ + | bot + /-- Implication. -/ + | imp (φ₁ φ₂ : Formula Atom) + /-- Until temporal operator: φ₁ U φ₂. -/ + | untl (φ₁ φ₂ : Formula Atom) + /-- Since temporal operator: φ₁ S φ₂. -/ + | snce (φ₁ φ₂ : Formula Atom) +deriving DecidableEq, BEq + +/-- Negation: ¬φ := φ → ⊥ -/ +abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot + +/-- Verum / top: ⊤ := ⊥ → ⊥ -/ +abbrev Formula.top : Formula Atom := .imp .bot .bot + +/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/ +abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom := + .imp (.imp φ₁ .bot) φ₂ + +/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/ +abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom := + .imp (.imp φ₁ (.imp φ₂ .bot)) .bot + +/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/ +abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom := + (φ₁.imp φ₂).and (φ₂.imp φ₁) + +/-- Some future (eventually): 𝐅 φ := φ U ⊤. -/ +abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom := + .untl φ .top + +/-- All future (globally): 𝐆 φ := ¬𝐅¬φ. -/ +abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom := + .neg (.someFuture (.neg φ)) + +/-- Some past: 𝐏 φ := φ S ⊤. -/ +abbrev Formula.somePast (φ : Formula Atom) : Formula Atom := + .snce φ .top + +/-- All past: 𝐇 φ := ¬𝐏¬φ. -/ +abbrev Formula.allPast (φ : Formula Atom) : Formula Atom := + .neg (.somePast (.neg φ)) + +@[inherit_doc] scoped prefix:40 "¬" => Formula.neg +@[inherit_doc] scoped infix:36 " ∧ " => Formula.and +@[inherit_doc] scoped infix:35 " ∨ " => Formula.or +@[inherit_doc] scoped infix:30 " → " => Formula.imp +@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff +@[inherit_doc] scoped infix:40 " U " => Formula.untl +@[inherit_doc] scoped infix:40 " S " => Formula.snce +@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture +@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture +@[inherit_doc] scoped prefix:40 "𝐏" => Formula.somePast +@[inherit_doc] scoped prefix:40 "𝐇" => Formula.allPast + +/-- Register `Temporal.Formula` as an instance of `TemporalConnectives`. -/ +instance : TemporalConnectives (Formula Atom) where + bot := .bot + imp := .imp + untl := .untl + snce := .snce + +instance : Bot (Formula Atom) := ⟨.bot⟩ +instance : Top (Formula Atom) := ⟨.top⟩ + +/-- Reflexive until: derives non-strict until from strict until. -/ +abbrev Formula.reflexiveUntl (φ ψ : Formula Atom) : Formula Atom := + φ.or (ψ.and (.untl φ ψ)) + +/-- Reflexive since: derives non-strict since from strict since. -/ +abbrev Formula.reflexiveSnce (φ ψ : Formula Atom) : Formula Atom := + φ.or (ψ.and (.snce φ ψ)) + +end Cslib.Logic.Temporal + +end diff --git a/references.bib b/references.bib index 8b4450757..6f53a5716 100644 --- a/references.bib +++ b/references.bib @@ -120,6 +120,16 @@ @misc{ WikipediaMyhillNerode2026 note = {[Online; accessed 9-April-2026]} } +@book{Church1956, + author = {Church, Alonzo}, + title = {Introduction to Mathematical Logic}, + volume = {1}, + publisher = {Princeton University Press}, + address = {Princeton}, + year = {1956}, + isbn = {978-0-691-02906-1} +} + @article{ Chargueraud2012, title = {The {Locally} {Nameless} {Representation}}, volume = {49}, @@ -157,6 +167,17 @@ @article{ FLP1985 numpages = {9} } +@article{Gentzen1935, + author = {Gentzen, Gerhard}, + title = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. {I}}, + journal = {Mathematische Zeitschrift}, + volume = {39}, + number = {1}, + pages = {176--210}, + year = {1935}, + doi = {10.1007/BF01201353} +} + @article{ Girard1987, title={Linear logic}, author={Girard, Jean-Yves}, @@ -212,6 +233,37 @@ @article{ Hennessy1985 bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{Johansson1937, + author = {Johansson, Ingebrigt}, + title = {Der Minimalkalk{\"u}l, ein reduzierter intuitionistischer Formalismus}, + journal = {Compositio Mathematica}, + volume = {4}, + pages = {119--136}, + year = {1937}, + url = {http://www.numdam.org/item/CM_1937__4__119_0/} +} + +@article{McKinsey1939, + author = {McKinsey, J. C. C.}, + title = {Proof of the Independence of the Primitive Symbols of {H}eyting's Calculus + of Propositions}, + journal = {Journal of Symbolic Logic}, + volume = {4}, + number = {4}, + pages = {155--158}, + year = {1939}, + doi = {10.2307/2268715} +} + +@article{Wajsberg1938, + author = {Wajsberg, Mordchaj}, + title = {Untersuchungen {\"u}ber den Aussagenkalk{\"u}l von {A}. {H}eyting}, + journal = {Wiadomo{\'s}ci Matematyczne}, + volume = {46}, + pages = {45--101}, + year = {1938} +} + @book{ KatzLindell2020, author = {Jonathan Katz and Yehuda Lindell}, @@ -304,6 +356,15 @@ @Book{ Montesi2023 keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory} } +@book{Prawitz1965, + author = {Prawitz, Dag}, + title = {Natural Deduction: A Proof-Theoretical Study}, + publisher = {Almqvist \& Wiksell}, + address = {Stockholm}, + year = {1965}, + note = {Reprinted by Dover Publications, 2006} +} + @article{ Nipkow2001, title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, author = {Nipkow, Tobias}, @@ -345,6 +406,18 @@ @Book{ Sangiorgi2011 doi = {10.1017/CBO9780511777110} } +@book{TroelstraVanDalen1988, + author = {Troelstra, A. S. and van Dalen, D.}, + title = {Constructivism in Mathematics: An Introduction}, + volume = {1}, + series = {Studies in Logic and the Foundations of Mathematics}, + number = {121}, + publisher = {North-Holland}, + address = {Amsterdam}, + year = {1988}, + isbn = {978-0-444-70506-8} +} + @incollection{ Thomas1990, author = {Wolfgang Thomas}, editor = {Jan van Leeuwen}, @@ -478,3 +551,63 @@ @book{Mitchell1997 publisher = {McGraw-Hill}, isbn = {0070428077} } + +@article{Burgess1982I, + author = {Burgess, John P.}, + title = {Axioms for Tense Logic. {I}. ``{Since}'' and ``{Until}''}, + journal = {Notre Dame Journal of Formal Logic}, + volume = {23}, + number = {4}, + pages = {367--374}, + year = {1982}, + doi = {10.1305/ndjfl/1093883455} +} + +@incollection{Burgess1984, + author = {Burgess, John P.}, + title = {Basic Tense Logic}, + booktitle = {Handbook of Philosophical Logic, Vol. {II}: Extensions of Classical Logic}, + editor = {Gabbay, Dov and Guenthner, Franz}, + pages = {89--133}, + publisher = {D. Reidel Publishing Company}, + address = {Dordrecht}, + year = {1984} +} + +@phdthesis{Kamp1968, + author = {Kamp, Hans}, + title = {Tense {{Logic}} and the {{Theory}} of {{Linear Order}}}, + year = {1968}, + school = {Ucla} +} + +@inproceedings{GPSS1980, + author = {Gabbay, Dov and Pnueli, Amir and Shelah, Saharon and Stavi, Jonathan}, + title = {On the Temporal Analysis of Fairness}, + booktitle = {Proceedings of the 7th Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on + Principles of Programming Languages}, + pages = {163--173}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + year = {1980}, + doi = {10.1145/567446.567462} +} + +@inproceedings{Pnueli1977, + author = {Pnueli, Amir}, + title = {The Temporal Logic of Programs}, + booktitle = {18th Annual Symposium on Foundations of Computer Science ({FOCS})}, + pages = {46--57}, + year = {1977}, + publisher = {{IEEE}}, + doi = {10.1109/SFCS.1977.32} +} + +@inproceedings{VardiWolper1986, + author = {Vardi, Moshe Y. and Wolper, Pierre}, + title = {An Automata-Theoretic Approach to Automatic Program Verification}, + booktitle = {Proceedings of the First Symposium on Logic in Computer Science ({LICS})}, + pages = {332--344}, + year = {1986}, + publisher = {{IEEE}} +} From 73cc31798a906ce0d5a0b8a5e5f4f5a6aa53d65b Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Thu, 18 Jun 2026 16:20:35 -0700 Subject: [PATCH 4/5] task 233 phase 1-3: revise PR #649 to LTL-only with standard notation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Remove HasSince and TemporalConnectives from Connectives.lean - Remove Temporal/Syntax/Formula.lean from PR (deferred to follow-up) - Remove toTemporal embedding from LTL/Syntax/Formula.lean - Update notation: X->◯, U->𝓤, 𝐅->◇, 𝐆->□ (standard LTL unicode) - Add leadsto abbreviation (p ⇝ q := □(p → ◇q)) with ⇝ notation - Add Cslib/Logics/LTL/Semantics/Satisfies.lean (satisfaction over omega-words) - Add Mathlib.Order.Notation import to resolve Bot/Top instances - Remove GPSS1980 from references.bib (past-time, deferred to Temporal PR) - Update Cslib.lean: add LTL.Semantics.Satisfies, remove Temporal.Syntax.Formula Session: sess_1781823963_4f9f03 --- Cslib.lean | 2 +- Cslib/Foundations/Logic/Connectives.lean | 16 +-- Cslib/Logics/LTL/Semantics/Satisfies.lean | 64 ++++++++++++ Cslib/Logics/LTL/Syntax/Formula.lean | 64 ++++++------ Cslib/Logics/Temporal/Syntax/Formula.lean | 119 ---------------------- references.bib | 34 ------- 6 files changed, 97 insertions(+), 202 deletions(-) create mode 100644 Cslib/Logics/LTL/Semantics/Satisfies.lean delete mode 100644 Cslib/Logics/Temporal/Syntax/Formula.lean diff --git a/Cslib.lean b/Cslib.lean index e05658900..acc40f38e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -137,6 +137,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic public import Cslib.Logics.HML.Basic public import Cslib.Logics.HML.LogicalEquivalence +public import Cslib.Logics.LTL.Semantics.Satisfies public import Cslib.Logics.LTL.Syntax.Formula public import Cslib.Logics.LinearLogic.CLL.Basic public import Cslib.Logics.LinearLogic.CLL.CutElimination @@ -150,7 +151,6 @@ public import Cslib.Logics.Modal.LogicalEquivalence public import Cslib.Logics.Propositional.Defs public import Cslib.Logics.Propositional.NaturalDeduction.Basic public import Cslib.Logics.Propositional.NaturalDeduction.Theory -public import Cslib.Logics.Temporal.Syntax.Formula public import Cslib.MachineLearning.PACLearning.Defs public import Cslib.MachineLearning.PACLearning.VCDimension public import Cslib.MachineLearning.PACLearning.VersionSpace diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean index 17ffa6cef..1815d8505 100644 --- a/Cslib/Foundations/Logic/Connectives.lean +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -18,11 +18,10 @@ axiom definitions and notation that work uniformly across different formula type The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`, following the operator-typeclass direction of fmontesi's PR #607 (one class per operator): -- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasUntil`, `HasSince`, `HasNext` +- **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasUntil`, `HasNext` - **Bundled classes**: `PropositionalConnectives` (extends `HasBot` and `HasImp`), `FutureTemporalConnectives` (extends `PropositionalConnectives` and `HasUntil`), - `LTLConnectives` (extends `FutureTemporalConnectives` and `HasNext`), - `TemporalConnectives` (extends `FutureTemporalConnectives` and `HasSince`) + `LTLConnectives` (extends `FutureTemporalConnectives` and `HasNext`) Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and @@ -68,11 +67,6 @@ class HasUntil (F : Type*) where /-- The until temporal operator. -/ untl : F → F → F -/-- A type has a since temporal operator. -/ -class HasSince (F : Type*) where - /-- The since temporal operator. -/ - snce : F → F → F - /-- A type has a next-step temporal operator. -/ class HasNext (F : Type*) where /-- The next-step temporal operator. -/ @@ -110,10 +104,4 @@ Linear Temporal Logic uses `next` as a primitive rather than deriving it from `u provides `bot`, `imp`, and `untl`; this bundle adds `next`. -/ class LTLConnectives (F : Type*) extends FutureTemporalConnectives F, HasNext F -/-- Temporal connectives: propositional connectives plus until and since. - -Extends `FutureTemporalConnectives` with the `since` operator, forming the standard -two-sorted temporal signature (future + past). -/ -class TemporalConnectives (F : Type*) extends FutureTemporalConnectives F, HasSince F - end Cslib.Logic diff --git a/Cslib/Logics/LTL/Semantics/Satisfies.lean b/Cslib/Logics/LTL/Semantics/Satisfies.lean new file mode 100644 index 000000000..9b73f4b28 --- /dev/null +++ b/Cslib/Logics/LTL/Semantics/Satisfies.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Benjamin Brast-McKie +-/ + +module + +public import Cslib.Logics.LTL.Syntax.Formula + +/-! # LTL Satisfaction over Omega-Words + +This module defines a basic satisfaction relation for LTL formulas over omega-words. +An omega-word is represented as a valuation `v : ℕ → (Atom → Prop)`, assigning to +each time point `i : ℕ` the set of atoms that hold at that point. + +The semantics follow the standard Kripke/Pnueli definition of LTL over ω-sequences. +Connection to `OmegaExecution` from the LTS library is deferred to future work. + +## Main definitions + +- `Satisfies v i φ` : formula `φ` holds at time `i` in valuation `v` +- `Valid v φ` : `φ` holds at all time points in `v` +- `Satisfiable φ` : `φ` holds at some time point in some valuation + +## References + +* [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977] +* [M. Y. Vardi, P. Wolper, + *An automata-theoretic approach to automatic program verification*][VardiWolper1986] +-/ + +@[expose] public section + +namespace Cslib.Logic.LTL + +variable {Atom : Type*} + +/-- Satisfaction relation for LTL over omega-words. + +`Satisfies v i φ` means formula `φ` holds at time point `i` in the omega-word `v`, +where `v : ℕ → (Atom → Prop)` assigns a set of true atoms to each time point. + +The `untl` case: `φ U ψ` holds at `i` when there exists a future time `j ≥ i` +where ψ holds (the event), and φ holds at all intermediate points `i ≤ k < j` +(the guard). -/ +def Satisfies (v : ℕ → (Atom → Prop)) (i : ℕ) : Formula Atom → Prop + | .atom p => v i p + | .bot => False + | .imp φ ψ => Satisfies v i φ → Satisfies v i ψ + | .next φ => Satisfies v (i + 1) φ + | .untl φ ψ => ∃ j ≥ i, Satisfies v j ψ ∧ ∀ k, i ≤ k → k < j → Satisfies v k φ + +/-- A formula holds at all time points in a given omega-word. -/ +def Valid (v : ℕ → (Atom → Prop)) (φ : Formula Atom) : Prop := + ∀ i, Satisfies v i φ + +/-- A formula is satisfiable: it holds at some time point in some omega-word. -/ +def Satisfiable (φ : Formula Atom) : Prop := + ∃ (v : ℕ → (Atom → Prop)) (i : ℕ), Satisfies v i φ + +end Cslib.Logic.LTL + +end diff --git a/Cslib/Logics/LTL/Syntax/Formula.lean b/Cslib/Logics/LTL/Syntax/Formula.lean index 82d692e41..2e5ebd290 100644 --- a/Cslib/Logics/LTL/Syntax/Formula.lean +++ b/Cslib/Logics/LTL/Syntax/Formula.lean @@ -8,23 +8,23 @@ module public import Cslib.Init public import Cslib.Foundations.Logic.Connectives -public import Cslib.Logics.Temporal.Syntax.Formula +public import Mathlib.Order.Notation /-! # LTL Formula Type This module defines the formula type for Linear Temporal Logic with primitives `{atom, bot, imp, next, untl}`. The primitive `next` operator is kept separate from -`untl` following the Burgess convention: in full temporal logic, `next φ` is sometimes -encoded as `φ U ⊥`, but this encoding does not hold in all models (it relies on -discreteness and non-triviality). An independent primitive `next` avoids this coupling. +`untl`: in full temporal logic, `next φ` is sometimes encoded as `φ U ⊥`, but this +encoding does not hold in all models (it relies on discreteness and non-triviality). +An independent primitive `next` avoids this coupling. ## Main definitions - `Formula` : Inductive type for LTL formulas with constructors `atom`, `bot`, `imp`, `next`, `untl` -- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point -- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points -- `Formula.toTemporal` : Embedding of `LTL.Formula` into `Temporal.Formula` +- `Formula.someFuture` (◇): `φ U ⊤` — φ holds at some future point +- `Formula.allFuture` (□): `¬◇¬φ` — φ holds at all future points +- `Formula.leadsto` (⇝): `□(p → ◇q)` — liveness: every p-state is eventually followed by q ## Notation @@ -36,23 +36,22 @@ Propositional connectives (scoped to `Cslib.Logic.LTL`): - `↔` (infix, 30) : biconditional (`Formula.iff`) Temporal operators (scoped to `Cslib.Logic.LTL`): -- `U` (infix, 40) : until (`Formula.untl`) -- `X` (prefix, 40) : next-step (`Formula.next`) -- `𝐅` (prefix, 40) : some future / eventually (`Formula.someFuture`) -- `𝐆` (prefix, 40) : all future / globally (`Formula.allFuture`) +- `𝓤` (infix, 40) : until (`Formula.untl`) +- `◯` (prefix, 40) : next-step (`Formula.next`) +- `◇` (prefix, 40) : some future / eventually (`Formula.someFuture`) +- `□` (prefix, 40) : all future / globally (`Formula.allFuture`) +- `⇝` (infix, 20) : leads-to, `□(p → ◇q)` (`Formula.leadsto`) ## Derived Operators -Derived operators follow the Burgess convention: in `untl event guard`, the first argument -is the **event** (holds at the witness point) and the second is the **guard** (holds at all -intermediate points). `someFuture φ` is `φ U ⊤` (φ is the event, ⊤ is the trivial guard). +In `untl φ ψ`, the first argument `φ` is the **guard** (holds at all intermediate +points) and the second `ψ` is the **event** (eventually holds at the witness point). +`someFuture φ` is `⊤ U φ` (⊤ is the trivial guard, φ is the event). ## References * [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977] * [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968] -* [J. P. Burgess, *Axioms for Tense Logic. I. "Since" and "Until"*][Burgess1982I] -* [J. P. Burgess, *Basic Tense Logic*][Burgess1984] * [M. Y. Vardi, P. Wolper, *An automata-theoretic approach to automatic program verification*][VardiWolper1986] -/ @@ -75,7 +74,7 @@ inductive Formula (Atom : Type u) : Type u where | imp (φ₁ φ₂ : Formula Atom) /-- Next-step operator: Xφ holds at t iff φ holds at t+1. -/ | next (φ : Formula Atom) - /-- Until temporal operator: φ₁ U φ₂ (Burgess: event U guard). -/ + /-- Until temporal operator: φ₁ U φ₂ (guard U event: φ₁ holds until φ₂). -/ | untl (φ₁ φ₂ : Formula Atom) deriving DecidableEq, BEq @@ -97,24 +96,30 @@ abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom := abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom := (φ₁.imp φ₂).and (φ₂.imp φ₁) -/-- Some future (eventually): F φ := φ U ⊤. - Uses Burgess convention: φ is the event (holds at witness), ⊤ is the trivial guard. -/ +/-- Some future (eventually): ◇φ := ⊤ U φ. + ⊤ is the trivial guard, φ is the event that eventually holds. -/ abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom := - .untl φ .top + .untl .top φ -/-- All future (globally): G φ := ¬F ¬φ -/ +/-- All future (globally): □φ := ¬◇¬φ -/ abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom := .neg (.someFuture (.neg φ)) +/-- Leads-to: p ⇝ q := □(p → ◇q). A liveness property asserting that + every state satisfying p is eventually followed by a state satisfying q. -/ +abbrev Formula.leadsto (p q : Formula Atom) : Formula Atom := + .allFuture (.imp p (.someFuture q)) + @[inherit_doc] scoped prefix:40 "¬" => Formula.neg @[inherit_doc] scoped infix:36 " ∧ " => Formula.and @[inherit_doc] scoped infix:35 " ∨ " => Formula.or @[inherit_doc] scoped infix:30 " → " => Formula.imp @[inherit_doc] scoped infix:30 " ↔ " => Formula.iff -@[inherit_doc] scoped infix:40 " U " => Formula.untl -@[inherit_doc] scoped prefix:40 "X" => Formula.next -@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture -@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture +@[inherit_doc] scoped infix:40 " 𝓤 " => Formula.untl +@[inherit_doc] scoped prefix:40 "◯" => Formula.next +@[inherit_doc] scoped prefix:40 "◇" => Formula.someFuture +@[inherit_doc] scoped prefix:40 "□" => Formula.allFuture +@[inherit_doc] scoped infix:20 " ⇝ " => Formula.leadsto /-- Register `LTL.Formula` as an instance of `LTLConnectives`. -/ instance : LTLConnectives (Formula Atom) where @@ -126,15 +131,6 @@ instance : LTLConnectives (Formula Atom) where instance : Bot (Formula Atom) := ⟨.bot⟩ instance : Top (Formula Atom) := ⟨.top⟩ -/-- Embed `LTL.Formula` into `Temporal.Formula`. Translates `next φ` as `φ U ⊥` -(strict until forces the immediate successor on ℕ) and `untl` as reflexive until. -/ -def Formula.toTemporal : Formula Atom → Temporal.Formula Atom - | .atom p => .atom p - | .bot => .bot - | .imp φ ψ => .imp (toTemporal φ) (toTemporal ψ) - | .next φ => .untl (toTemporal φ) .bot - | .untl φ ψ => (toTemporal φ).reflexiveUntl (toTemporal ψ) - end Cslib.Logic.LTL end diff --git a/Cslib/Logics/Temporal/Syntax/Formula.lean b/Cslib/Logics/Temporal/Syntax/Formula.lean deleted file mode 100644 index 07060dc29..000000000 --- a/Cslib/Logics/Temporal/Syntax/Formula.lean +++ /dev/null @@ -1,119 +0,0 @@ -/- -Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Benjamin Brast-McKie --/ - -module - -public import Cslib.Init -public import Cslib.Foundations.Logic.Connectives -public import Mathlib.Order.Notation - -/-! # Temporal Logic Formula - -This module defines the formula type for temporal logic with primitives -`{atom, bot, imp, untl, snce}`. The `untl` (until) and `snce` (since) operators are -the basic future and past temporal modalities from which all derived temporal operators -(globally, eventually, somePast, allPast) are obtained. - -## Main definitions - -- `Formula` : Inductive type for temporal logic formulas with constructors - `atom`, `bot`, `imp`, `untl`, `snce` -- `Formula.someFuture` (𝐅): `φ U ⊤` — φ holds at some future point -- `Formula.allFuture` (𝐆): `¬𝐅¬φ` — φ holds at all future points -- `Formula.somePast` (𝐏): `φ S ⊤` — φ held at some past point -- `Formula.allPast` (𝐇): `¬𝐏¬φ` — φ held at all past points - -## References - -* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968] -* [D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, *On the temporal analysis of fairness*][GPSS1980] --/ - -@[expose] public section - -namespace Cslib.Logic.Temporal - -/-- Temporal logic formula type. Primitives: atoms, falsum, implication, until, and since. -/ -inductive Formula (Atom : Type u) : Type u where - /-- Atomic proposition. -/ - | atom (p : Atom) - /-- Falsum / bottom. -/ - | bot - /-- Implication. -/ - | imp (φ₁ φ₂ : Formula Atom) - /-- Until temporal operator: φ₁ U φ₂. -/ - | untl (φ₁ φ₂ : Formula Atom) - /-- Since temporal operator: φ₁ S φ₂. -/ - | snce (φ₁ φ₂ : Formula Atom) -deriving DecidableEq, BEq - -/-- Negation: ¬φ := φ → ⊥ -/ -abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot - -/-- Verum / top: ⊤ := ⊥ → ⊥ -/ -abbrev Formula.top : Formula Atom := .imp .bot .bot - -/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/ -abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom := - .imp (.imp φ₁ .bot) φ₂ - -/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/ -abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom := - .imp (.imp φ₁ (.imp φ₂ .bot)) .bot - -/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/ -abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom := - (φ₁.imp φ₂).and (φ₂.imp φ₁) - -/-- Some future (eventually): 𝐅 φ := φ U ⊤. -/ -abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom := - .untl φ .top - -/-- All future (globally): 𝐆 φ := ¬𝐅¬φ. -/ -abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom := - .neg (.someFuture (.neg φ)) - -/-- Some past: 𝐏 φ := φ S ⊤. -/ -abbrev Formula.somePast (φ : Formula Atom) : Formula Atom := - .snce φ .top - -/-- All past: 𝐇 φ := ¬𝐏¬φ. -/ -abbrev Formula.allPast (φ : Formula Atom) : Formula Atom := - .neg (.somePast (.neg φ)) - -@[inherit_doc] scoped prefix:40 "¬" => Formula.neg -@[inherit_doc] scoped infix:36 " ∧ " => Formula.and -@[inherit_doc] scoped infix:35 " ∨ " => Formula.or -@[inherit_doc] scoped infix:30 " → " => Formula.imp -@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff -@[inherit_doc] scoped infix:40 " U " => Formula.untl -@[inherit_doc] scoped infix:40 " S " => Formula.snce -@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture -@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture -@[inherit_doc] scoped prefix:40 "𝐏" => Formula.somePast -@[inherit_doc] scoped prefix:40 "𝐇" => Formula.allPast - -/-- Register `Temporal.Formula` as an instance of `TemporalConnectives`. -/ -instance : TemporalConnectives (Formula Atom) where - bot := .bot - imp := .imp - untl := .untl - snce := .snce - -instance : Bot (Formula Atom) := ⟨.bot⟩ -instance : Top (Formula Atom) := ⟨.top⟩ - -/-- Reflexive until: derives non-strict until from strict until. -/ -abbrev Formula.reflexiveUntl (φ ψ : Formula Atom) : Formula Atom := - φ.or (ψ.and (.untl φ ψ)) - -/-- Reflexive since: derives non-strict since from strict since. -/ -abbrev Formula.reflexiveSnce (φ ψ : Formula Atom) : Formula Atom := - φ.or (ψ.and (.snce φ ψ)) - -end Cslib.Logic.Temporal - -end diff --git a/references.bib b/references.bib index 6f53a5716..6f5fac018 100644 --- a/references.bib +++ b/references.bib @@ -552,28 +552,6 @@ @book{Mitchell1997 isbn = {0070428077} } -@article{Burgess1982I, - author = {Burgess, John P.}, - title = {Axioms for Tense Logic. {I}. ``{Since}'' and ``{Until}''}, - journal = {Notre Dame Journal of Formal Logic}, - volume = {23}, - number = {4}, - pages = {367--374}, - year = {1982}, - doi = {10.1305/ndjfl/1093883455} -} - -@incollection{Burgess1984, - author = {Burgess, John P.}, - title = {Basic Tense Logic}, - booktitle = {Handbook of Philosophical Logic, Vol. {II}: Extensions of Classical Logic}, - editor = {Gabbay, Dov and Guenthner, Franz}, - pages = {89--133}, - publisher = {D. Reidel Publishing Company}, - address = {Dordrecht}, - year = {1984} -} - @phdthesis{Kamp1968, author = {Kamp, Hans}, title = {Tense {{Logic}} and the {{Theory}} of {{Linear Order}}}, @@ -581,18 +559,6 @@ @phdthesis{Kamp1968 school = {Ucla} } -@inproceedings{GPSS1980, - author = {Gabbay, Dov and Pnueli, Amir and Shelah, Saharon and Stavi, Jonathan}, - title = {On the Temporal Analysis of Fairness}, - booktitle = {Proceedings of the 7th Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on - Principles of Programming Languages}, - pages = {163--173}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - year = {1980}, - doi = {10.1145/567446.567462} -} - @inproceedings{Pnueli1977, author = {Pnueli, Amir}, title = {The Temporal Logic of Programs}, From 3e14712371f36f89032b686f6e128c4c9dbc4bd4 Mon Sep 17 00:00:00 2001 From: benbrastmckie Date: Fri, 19 Jun 2026 16:20:55 -0700 Subject: [PATCH 5/5] =?UTF-8?q?fix(LTL):=20use=20=CF=89Sequence=20State=20?= =?UTF-8?q?for=20satisfaction,=20fix=20docstrings?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rewrite Satisfies to use ωSequence State with a separate valuation v : Atom → State → Prop, addressing reviewer feedback. Remove forward reference to nonexistent TemporalConnectives in FutureTemporalConnectives docstring. Fix someFuture docstring argument order (⊤ U φ, not φ U ⊤). Co-Authored-By: Claude Opus 4.6 (1M context) --- Cslib/Foundations/Logic/Connectives.lean | 5 +-- Cslib/Logics/LTL/Semantics/Satisfies.lean | 52 +++++++++++++---------- Cslib/Logics/LTL/Syntax/Formula.lean | 2 +- 3 files changed, 32 insertions(+), 27 deletions(-) diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean index 1815d8505..dfa9ce513 100644 --- a/Cslib/Foundations/Logic/Connectives.lean +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -91,9 +91,8 @@ class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F /-- Future temporal connectives: propositional connectives plus until (no since, no next). -This bundle is shared by both `LTLConnectives` (which adds `HasNext`) and -`TemporalConnectives` (which adds `HasSince`). Factoring out the future fragment -allows code generic over future-only temporal logics without committing to past or +`LTLConnectives` extends this with `HasNext`. Factoring out the future fragment +allows code generic over future-only temporal logics without committing to next-step operators. -/ class FutureTemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F diff --git a/Cslib/Logics/LTL/Semantics/Satisfies.lean b/Cslib/Logics/LTL/Semantics/Satisfies.lean index 9b73f4b28..fa1bb5fbc 100644 --- a/Cslib/Logics/LTL/Semantics/Satisfies.lean +++ b/Cslib/Logics/LTL/Semantics/Satisfies.lean @@ -7,21 +7,26 @@ Authors: Benjamin Brast-McKie module public import Cslib.Logics.LTL.Syntax.Formula +public import Cslib.Foundations.Data.OmegaSequence.Init /-! # LTL Satisfaction over Omega-Words -This module defines a basic satisfaction relation for LTL formulas over omega-words. -An omega-word is represented as a valuation `v : ℕ → (Atom → Prop)`, assigning to -each time point `i : ℕ` the set of atoms that hold at that point. +This module defines a basic satisfaction relation for LTL formulas over omega-words +of states. A `State` type is equipped with a valuation `v : Atom → State → Prop` +that determines which atomic propositions hold at each state. An omega-word is an +`ωSequence State`, and satisfaction is evaluated at the first state of the sequence, +with temporal operators moving along the sequence via `head` and `tail`. The semantics follow the standard Kripke/Pnueli definition of LTL over ω-sequences. Connection to `OmegaExecution` from the LTS library is deferred to future work. ## Main definitions -- `Satisfies v i φ` : formula `φ` holds at time `i` in valuation `v` -- `Valid v φ` : `φ` holds at all time points in `v` -- `Satisfiable φ` : `φ` holds at some time point in some valuation +- `Satisfies v w φ` : formula `φ` holds at the first state of omega-word `w` + under valuation `v` +- `Valid v φ` : `φ` holds at the first state of every omega-word under `v` +- `Satisfiable φ` : `φ` holds at the first state of some omega-word under some + valuation ## References @@ -34,30 +39,31 @@ Connection to `OmegaExecution` from the LTS library is deferred to future work. namespace Cslib.Logic.LTL -variable {Atom : Type*} +variable {Atom State : Type*} -/-- Satisfaction relation for LTL over omega-words. +/-- Satisfaction relation for LTL over omega-words of states. -`Satisfies v i φ` means formula `φ` holds at time point `i` in the omega-word `v`, -where `v : ℕ → (Atom → Prop)` assigns a set of true atoms to each time point. +`Satisfies v w φ` means formula `φ` holds at the first state of the omega-word `w`, +where `v : Atom → State → Prop` determines which atoms hold at each state. -The `untl` case: `φ U ψ` holds at `i` when there exists a future time `j ≥ i` -where ψ holds (the event), and φ holds at all intermediate points `i ≤ k < j` -(the guard). -/ -def Satisfies (v : ℕ → (Atom → Prop)) (i : ℕ) : Formula Atom → Prop - | .atom p => v i p +The `untl` case: `φ U ψ` holds at the current state when there exists a future +position `j` where ψ holds (the event), and φ holds at all intermediate positions +`k < j` (the guard). -/ +def Satisfies (v : Atom → State → Prop) (w : ωSequence State) : Formula Atom → Prop + | .atom p => v p w.head | .bot => False - | .imp φ ψ => Satisfies v i φ → Satisfies v i ψ - | .next φ => Satisfies v (i + 1) φ - | .untl φ ψ => ∃ j ≥ i, Satisfies v j ψ ∧ ∀ k, i ≤ k → k < j → Satisfies v k φ + | .imp φ ψ => Satisfies v w φ → Satisfies v w ψ + | .next φ => Satisfies v w.tail φ + | .untl φ ψ => ∃ j, Satisfies v (w.drop j) ψ ∧ ∀ k < j, Satisfies v (w.drop k) φ -/-- A formula holds at all time points in a given omega-word. -/ -def Valid (v : ℕ → (Atom → Prop)) (φ : Formula Atom) : Prop := - ∀ i, Satisfies v i φ +/-- A formula holds at the first state of every omega-word under the given valuation. -/ +def Valid (v : Atom → State → Prop) (φ : Formula Atom) : Prop := + ∀ (w : ωSequence State), Satisfies v w φ -/-- A formula is satisfiable: it holds at some time point in some omega-word. -/ +/-- A formula is satisfiable: it holds at the first state of some omega-word + under some valuation. -/ def Satisfiable (φ : Formula Atom) : Prop := - ∃ (v : ℕ → (Atom → Prop)) (i : ℕ), Satisfies v i φ + ∃ (v : Atom → State → Prop) (w : ωSequence State), Satisfies v w φ end Cslib.Logic.LTL diff --git a/Cslib/Logics/LTL/Syntax/Formula.lean b/Cslib/Logics/LTL/Syntax/Formula.lean index 2e5ebd290..33f31263f 100644 --- a/Cslib/Logics/LTL/Syntax/Formula.lean +++ b/Cslib/Logics/LTL/Syntax/Formula.lean @@ -22,7 +22,7 @@ An independent primitive `next` avoids this coupling. - `Formula` : Inductive type for LTL formulas with constructors `atom`, `bot`, `imp`, `next`, `untl` -- `Formula.someFuture` (◇): `φ U ⊤` — φ holds at some future point +- `Formula.someFuture` (◇): `⊤ U φ` — φ holds at some future point - `Formula.allFuture` (□): `¬◇¬φ` — φ holds at all future points - `Formula.leadsto` (⇝): `□(p → ◇q)` — liveness: every p-state is eventually followed by q