Regular Propositions of a Compatibility Frame

@cite{holliday-mandelkern-2024}

The bundled type RegularProp F of ◇-regular subsets of a compatibility frame F, equipped with its OrthocomplementedLattice structure.

Construction

RegularProp F is a bundled structure (mathlib Submodule/SetLike pattern) wrapping a Set S together with its regularity proof. The underlying mathematical object is (regularClosure F).fixedPoints — the fixed points of the c_◇ closure operator (Holliday–Mandelkern footnote 19); this file proves the lattice operations on these fixed points form an orthocomplemented lattice.

The four OrthocomplementedLattice axioms:

axiom	difficulty	uses regularity?
compl_antitone	trivial from orthoNeg def	no
inf_compl_le_bot	one-liner via reflexivity	no
top_le_sup_compl	from orthoNeg² containment	no
compl_compl	the substantive theorem (Prop 4.8)	YES

The load-bearing fact is orthoNeg_orthoNeg_of_isRegular — the involutivity of orthoNeg on regular sets, which is precisely Holliday–Mandelkern's Proposition 4.8.

Architecture

This file depends on:

• Linglib.Theories.Semantics.Modality.Orthologic.Frames — substrate (compatibility frames, orthoNeg, disj, isRegular, regularClosure).
• Linglib.Core.Order.Ortholattice — abstract OrthocomplementedLattice typeclass.

The RegularProp F carrier is the natural mathlib subobject for any future ortholattice consumer (BSML, inquisitive semantics, truthmaker semantics — all of which traffic in non-Boolean propositional algebras).

theorem Semantics.Modality.Orthologic.orthoNeg_isRegular {S : Type u_1} (F : CompatFrame S) (A : Set S) : isRegular F (orthoNeg F A)

The orthocomplement of any set is regular (whether or not the original set is).

theorem Semantics.Modality.Orthologic.inter_isRegular {S : Type u_1} {F : CompatFrame S} {A B : Set S} (hA : isRegular F A) (hB : isRegular F B) : isRegular F (A ∩ B)

Regular sets are closed under intersection.

theorem Semantics.Modality.Orthologic.disj_isRegular {S : Type u_1} (F : CompatFrame S) (A B : Set S) : isRegular F (disj F A B)

The disjunction disj F A B = orthoNeg F (orthoNeg F A ∩ orthoNeg F B) is regular (immediate from orthoNeg_isRegular).

theorem Semantics.Modality.Orthologic.empty_isRegular {S : Type u_1} (F : CompatFrame S) : isRegular F ∅

The empty set is regular (vacuously: take y = x by reflexivity).

theorem Semantics.Modality.Orthologic.univ_isRegular {S : Type u_1} (F : CompatFrame S) : isRegular F Set.univ

The full set is regular (trivially).

theorem Semantics.Modality.Orthologic.orthoNeg_orthoNeg_of_isRegular {S : Type u_1} (F : CompatFrame S) {A : Set S} (hA : isRegular F A) : orthoNeg F (orthoNeg F A) = A

The load-bearing involutivity: orthoNeg² A = A for regular A. @cite{holliday-mandelkern-2024} Proposition 4.8.

structure Semantics.Modality.Orthologic.RegularProp {S : Type u_1} (F : CompatFrame S) : Type u_1

A regular proposition of a compatibility frame F: a Set S satisfying the ◇-regularity condition. Bundled as a structure with SetLike instance, mirroring mathlib's subobject pattern (Submodule, Subgroup, Subalgebra).

• carrier : Set S

  The underlying set of the regular proposition.

• regular' : isRegular F self.carrier

  The regularity proof.

theorem Semantics.Modality.Orthologic.RegularProp.ext_iff {S : Type u_1} {F : CompatFrame S} {x y : RegularProp F} : x = y ↔ x.carrier = y.carrier

theorem Semantics.Modality.Orthologic.RegularProp.ext {S : Type u_1} {F : CompatFrame S} {x y : RegularProp F} (carrier : x.carrier = y.carrier) : x = y

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instSetLike {S : Type u_1} {F : CompatFrame S} : SetLike (RegularProp F) S

Equations

• Semantics.Modality.Orthologic.RegularProp.instSetLike = { coe := Semantics.Modality.Orthologic.RegularProp.carrier, coe_injective' := ⋯ }

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.mem_mk {S : Type u_1} {F : CompatFrame S} (A : Set S) (hA : isRegular F A) (x : S) : x ∈ { carrier := A, regular' := hA } ↔ x ∈ A

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.coe_mk {S : Type u_1} {F : CompatFrame S} (A : Set S) (hA : isRegular F A) : ↑{ carrier := A, regular' := hA } = A

theorem Semantics.Modality.Orthologic.RegularProp.regular {S : Type u_1} {F : CompatFrame S} (A : RegularProp F) : isRegular F ↑A

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instMin {S : Type u_1} {F : CompatFrame S} : Min (RegularProp F)

Equations

• Semantics.Modality.Orthologic.RegularProp.instMin = { min := fun (A B : Semantics.Modality.Orthologic.RegularProp F) => { carrier := ↑A ∩ ↑B, regular' := ⋯ } }

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instMax {S : Type u_1} {F : CompatFrame S} : Max (RegularProp F)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instBot {S : Type u_1} {F : CompatFrame S} : Bot (RegularProp F)

Equations

• Semantics.Modality.Orthologic.RegularProp.instBot = { bot := { carrier := ∅, regular' := ⋯ } }

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instTop {S : Type u_1} {F : CompatFrame S} : Top (RegularProp F)

Equations

• Semantics.Modality.Orthologic.RegularProp.instTop = { top := { carrier := Set.univ, regular' := ⋯ } }

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instCompl {S : Type u_1} {F : CompatFrame S} : Compl (RegularProp F)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.coe_inf {S : Type u_1} {F : CompatFrame S} (A B : RegularProp F) : ↑(A ⊓ B) = ↑A ∩ ↑B

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.coe_sup {S : Type u_1} {F : CompatFrame S} (A B : RegularProp F) : ↑(A ⊔ B) = disj F ↑A ↑B

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.coe_bot {S : Type u_1} {F : CompatFrame S} : ↑⊥ = ∅

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.coe_top {S : Type u_1} {F : CompatFrame S} : ↑⊤ = Set.univ

@[simp]

theorem Semantics.Modality.Orthologic.RegularProp.coe_compl {S : Type u_1} {F : CompatFrame S} (A : RegularProp F) : ↑Aᶜ = orthoNeg F ↑A

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instPartialOrder {S : Type u_1} {F : CompatFrame S} : PartialOrder (RegularProp F)

Equations

• Semantics.Modality.Orthologic.RegularProp.instPartialOrder = PartialOrder.ofSetLike (Semantics.Modality.Orthologic.RegularProp F) S

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instLattice {S : Type u_1} {F : CompatFrame S} : Lattice (RegularProp F)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instBoundedOrder {S : Type u_1} {F : CompatFrame S} : BoundedOrder (RegularProp F)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Semantics.Modality.Orthologic.RegularProp.instOrthocomplementedLattice {S : Type u_1} {F : CompatFrame S} : OrthocomplementedLattice (RegularProp F)

Equations

• One or more equations did not get rendered due to their size.