no message

source/domain_theories/numbers/nat.mmt

-namespace latin:/❚
-
-fixmeta latin:/?SFOLEQND❚
-
-import rules scala://lf.mmt.kwarc.info❚
-import uom scala://uom.api.mmt.kwarc.info❚
-
-theory Nat =
-  nat   : tp❙
-  Nat = tm nat❘# ℕ❙
-  zero  : ℕ❙
-  succ  : ℕ ⟶ ℕ❘ # 1 ' prec 15❙
-  
-  even: ℕ ⟶ prop ❙
-  uneven: ℕ ⟶ prop ❙
-  
-  rule rules?Realize ℕ uom?StandardNat❙
-  rule rules?Realize zero uom?Arithmetic/Zero❙
-  rule rules?Realize succ uom?Arithmetic/Succ❙
-❚
-  
-theory NatPlus =
-  include ?Nat❙
-  plus : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 + 2 prec 50❙
-  
-  plus_zero : ⊦ ∀ͭ[n] n+zero =ͭ n❙
-  plus_succ : ⊦ ∀ͭ[m]∀ͭ[n] n+(succ m) =ͭ succ(n+m)❙
-  
-  plus_zero_left: ⊦ ∀ͭ[n] zero+n =ͭ n❘
-               // = proof ommited❘
-  ❙
-
-  assoc : ⊦ ∀ͭ[l]∀ͭ[m]∀ͭ[n] (l+m)+n =ͭ l+(m+n)❘
-               // = proof ommited❘  
-  ❙
-  
-  comm : ⊦ ∀ͭ[m]∀ͭ[n] m+n =ͭ n+m❘
-               // = proof ommited❘  
-  ❙
-  
-  // realization rules ommited❙
-❚
-
-theory NatPlusTimes =
-  include ?NatPlus❙
-  times : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 * 2 prec 60❙
-  
-  // axioms and realization rules ommited❙
-❚
-
-theory Int =
-	include ?NatPlusTimes❙
-	int   : tp❙
-  Int = tm int❘# ℤ❙
-  
-  inclusion: ℕ ⟶ ℤ❘# int 1 prec 10❙
-  isucc: ℤ ⟶ ℤ❘ # s 1 prec 15❙
-  ipred: ℤ ⟶ ℤ❘ # p 1 prec 15❙
-  ineg: ℤ ⟶ ℤ❘ # - 1 prec 15❙
-  iplus: ℤ ⟶ ℤ ⟶ ℤ❘ # 1 + 2 prec 50❙
-  iminus: ℤ ⟶ ℤ ⟶ ℤ❘= [a,b] a + (- b)❘ # 1 - 2 prec 50 ❙
-  itimes: ℤ ⟶ ℤ ⟶ ℤ❘ # 1 * 2 prec 60❙
-  
-  ieven: ℤ ⟶ prop ❘ # even 1 prec 70❙
-  iuneven: ℤ ⟶ prop ❘ # uneven 1 prec 70❙
-  
-  // axioms and realization rules ommited❙
-❚
\ No newline at end of file

source/domain_theories/numbers/nat_axiomatic.mmt

@@ -89,7 +89,7 @@ theory Nat =
 
   greater: tm num ⟶ tm num⟶ prop ❘# 1 > 2 prec 30❘
   	= [x,y] y < x❙
-  lesserequal: tm num ⟶ tm num ⟶ prop ❘# 1 %n 2 prec 30❘
+  lesserequal: tm num ⟶ tm num ⟶ prop ❘# 1 ≤ 2 prec 30❘
     	= [x,y] ¬ (x < y) ❙
   greaterequal:  tm num ⟶ tm num ⟶ prop ❘# 1 ≥ 2 prec 30❘
   	= [x,y] ¬ (x < y ) ❙

source/fundamentals/base_languages.mmt

@@ -21,6 +21,20 @@ theory UntypedLogic =
 theory TypedLogic =
   include ?Logic❙
   include ?TypedTerms❙
+  liftPred2: {S,A,B} (          tm A ⟶           tm B  ⟶          prop)
+                   ⟶ (tm S ⟶ tm A) ⟶ (tm S ⟶ tm B) ⟶ (tm S ⟶ prop)❘
+      = [S,A,B,o,f,g] [x] o (f x) (g x)❘
+      # liftFun2 4❙
+
+  lift0: {S} prop ⟶ (tm S ⟶ prop)❘
+      = [S,o] [x]o❘
+      # lift0 2❙
+  lift1: {S} (prop ⟶ prop) ⟶ (tm S ⟶ prop) ⟶ (tm S ⟶ prop)❘
+      = [S,o,f] [x]o (f x)❘
+      # lift1 2❙
+  lift2: {S} (prop ⟶ prop ⟶ prop) ⟶ (tm S ⟶ prop) ⟶ (tm S ⟶ prop) ⟶ (tm S ⟶ prop)❘
+      = [S,o,f,g] [x]o (f x) (g x)❘
+      # lift2 2❙
 ❚
 
 /T logics with flexible type systems

source/logic/build.msl

@@ -7,7 +7,7 @@ file source/logic/propositional/build.msl
 file source/logic/metalogic/build.msl
 file source/logic/fol_like/build.msl
 file source/logic/hol_like/build.msl
-file source/logic/model_theory/build.msl
+file source/logic/modal_like/build.msl
 
 // unclear where this should go because it defines Scala rules
 // file source/logic/drt/build.msl
\ No newline at end of file

source/logic/fol_like/build.msl

@@ -29,7 +29,3 @@ build MMT/LATIN2 mmt-omdoc ./booleans.mmt
 // depends on sfol and booleans
 build MMT/LATIN2 mmt-omdoc ./pl-sfol.mmt
 
-// depend on some of the above
-build MMT/LATIN2 mmt-omdoc ./multimodal.mmt
-build MMT/LATIN2 mmt-omdoc ./dynamic.mmt
-

source/logic/modal_like/build.msl

+file ../../../build_config.msl
+
+// syntax
+
+build MMT/LATIN2 mmt-omdoc ./modal.mmt
+build MMT/LATIN2 mmt-omdoc ./multimodal.mmt
+build MMT/LATIN2 mmt-omdoc ./dynamic.mmt
+build MMT/LATIN2 mmt-omdoc ./ltl.mmt
+build MMT/LATIN2 mmt-omdoc ./ctl.mmt
+
+
+// semantics
+
+// needed for all of the others
+build MMT/LATIN2 mmt-omdoc ./parametric_evaluation.mmt
+
+build MMT/LATIN2 mmt-omdoc ./kripke.mmt
+build MMT/LATIN2 mmt-omdoc ./kripke_multimodal.mmt
+build MMT/LATIN2 mmt-omdoc ./kripke_dynamic.mmt
+build MMT/LATIN2 mmt-omdoc ./kripke/ltl.mmt
+build MMT/LATIN2 mmt-omdoc ./kripke/ctl.mmt

source/logic/modal_like/ctl.mmt

+namespace latin:/❚
+
+fixmeta ur:?LF❚
+
+/T Computation Tree Logic
+   CTL propositions are meant to be evaluated relative to a state by quantifying over all traces emanating from it.
+   All CTL operators occur in two variants (e.g., AX and EX) depending on how we quantify over those traces.
+   We use an auxiliary type of trace-propositions in order to formalize A and E as separate operators that are composed with X.❚
+
+theory CTLBase =
+  include ?Propositions❙
+  traceprop : type❙
+  foralltraces : traceprop ⟶ prop❘ # A 1 prec 20❙
+  forsometrace : traceprop ⟶ prop❘ # E 1 prec 20❙
+❚
+
+theory TraceNext = 
+  include ?CTLBase❙
+  next: prop ⟶ traceprop❘ # X 1 prec 20❙
+❚
+
+theory TraceFinally =
+  include ?CTLBase❙
+  finally: prop ⟶ traceprop❘# F 1 prec 20❙
+❚
+
+/T dual of TraceFinally❚
+theory TraceAlways =
+  include ?CTLBase❙
+  always: prop ⟶ traceprop❘# G 1 prec 20❙
+❚
+
+theory TraceUntil =
+  include ?CTLBase❙
+  until: prop ⟶ prop ⟶ traceprop❘# 1 U 2 prec 20❙
+❚
+
+/T dual of until❚
+theory TraceRelease =
+  include ?CTLBase❙
+  release: prop ⟶ prop ⟶ traceprop❘# 1 R 2 prec 20❙
+❚
+
+theory CTL =
+  include ?CTLBase❙
+  include ?PL❙
+  include ?TraceNext❙
+  include ?TraceFinally❙
+  include ?TraceAlways❙
+  include ?TraceUntil❙
+  include ?TraceRelease❙
+❚
+

source/logic/fol_like/dynamic.mmt → source/logic/modal_like/dynamic.mmt

 namespace latin:/❚
 
-/T Dynamic Logic is a Multi-Modal Logic originally introduced by
+/T Dynamic Logic is a multimodal Logic originally introduced by
   Vaugham Pratt in 1996 for reasoning about imperative programs
   and later extended to more general uses in linguistics and philosophy.
   See https://en.wikipedia.org/wiki/Dynamic_logic_(modal_logic) for details.
@@ -29,11 +29,11 @@ theory Programs =
 ❚
 
 /T Dynamic Logic is just the multimodal logic 
-   where the modality is given by Π programs. ❚
+   where the modalities are the programs. ❚
 theory DynamicLogic =
   include ?MML❙
   realize ?Programs❙
-  prog = modality ❙
+  prog = modality❙
 ❚
 
 /T A simple non-deterministic programming language ❚

source/logic/modal_like/kripke.mmt

+namespace latin:/kripkemodels❚
+
+fixmeta latin:/?TypedLogic❚
+
+/T the set of worlds of a Kripke frame❚
+theory Worlds =
+  world: tp❘# W❙
+❚
+
+/T a Kripe frame consists of a set of worlds and an accessibility relation on them❚
+theory KripkeFrame =
+  include ?Worlds❙
+  accessible : tm W ⟶ tm W ⟶ prop❘ # 1 acc 2 prec 30❙
+❚
+
+/T like a Kripke frame, but adds operations for working with paths/traces of worlds❚ 
+theory KripkeTraces =
+  include ?KripkeFrame❙
+  include ?KripkeFrame❙
+  trace: tp❙
+  include ☞latin:/?Nat❙
+  
+  worldAt: tm trace ⟶ ℕ ⟶ tm W❘ # 1 ' 2 prec 50❙
+  suffixAt: tm trace ⟶ ℕ ⟶ tm trace❘# 1 ^ 2 prec 50❙
+❚
+
+/T This should be mixed into Kripke models if propositions are interpreted as world-indexed Booleans.❚
+theory EvaluationInWorlds =
+  include ?Worlds❙
+  realize ?EvaluationParameter❙
+  param = world❙
+❚
+
+/T This should be mixed into Kripke models if propositions are interpreted as trace-indexed Booleans.❚
+theory EvaluationInTraces =
+  include ?KripkeTraces❙
+  realize ?EvaluationParameter❙
+  param = trace❙
+❚
+
+/T an abbreviation for a Kripke model with HOL as an expressive meta-language.❚
+theory KripkeModelHOL : latin:/?HOLND =
+  include ?KripkeFrame❙
+  include ?EvaluationInWorlds❙
+❚
+
+/T the semantics of the modal operators❚
+view MLSemantics : latin:/?ML → ?KripkeModelHOL =
+  include ?ParametricPLSemantics❙
+  include ?ParametricLogicSemantics❙
+  box = [p] [v] ∀ͭ [w] v acc w ⇒ p w❙
+  diamond = [p] [v] ∃ͭ [w] v acc w ∧ p w❙ 
+❚
+
+view MLHilbertSemantics : latin:/?MLHilbert → ?KripkeModelHOL =
+  include ?MLSemantics❙
+  include ?ParametricPLHilbertSemantics❙
+❚

source/logic/modal_like/kripke_ctl.mmt

+namespace latin:/kripkemodels❚
+
+/T A CTL model is a Kripke model in which a proposition is evaluated at a state/world w yielding a property of traces.
+   The operators A and E then reduce those to a property of states by quantifying over all traces starting at w.
+❚
+
+theory CTLModel : latin:/?SFOLEQND =
+  include ?KripkeTraces❙
+  include ?EvaluationInWorlds❙
+❚
+
+view CTLSemantics : latin:/?CTL → ?CTLModel =
+  include ?ParametricPLSemantics❙
+  traceprop = tm trace ⟶ prop❙
+  foralltraces = [r,w] ∀ͭ[t] t'0 =ͭ w ⇒ r t❙
+  forsometrace = [r,w] ∃ͭ[t] t'0 =ͭ w ∧ r t❙
+  next = [f,t] f (t'1)❙
+  finally = [f,t] ∃ͭ [i] f(t'i)❙
+  always  = [f,t] ∀ͭ [i] f(t'i)❙
+  until = [f,g,t] ∃ͭ [i] ∀ͭ[j] (j<i ⇒ f(t'j)) ∧ g(t'i)❙
+  release = [f,g,t] ∃ͭ [i] ∀ͭ[j] (j≤i ⇒ g(t'j)) ∧ f(t'i) ∨ ∀ͭ[j] g(t'j)❙
+❚

source/logic/model_theory/kripke_dynamic.mmt → source/logic/modal_like/kripke_dynamic.mmt

@@ -3,8 +3,9 @@ namespace latin:/kripkemodels❚
 fixmeta ur:?LF❚
 
 /T a theory of states, i.e. assignments to program variables ❚
-theory State : latin:/?HOL =
-  include ?Worlds❙
+theory State : latin:/?HOLND =
+  include ?KripkeModelHOL❙
+  
   cell : tp ⟶ tp❙
   state: tm W ⟶ {S} tm cell S ⟶ tm S❘ # 3 * 1 prec 50 ❙
   
@@ -24,7 +25,7 @@ view DynamicLogicSemantics : latin:/?DynamicLogic → ?State =
 
 view NonDetProgSemantics : latin:/?NonDetProg → ?State =
   include ☞latin:/?Programs❘ = ?DynamicLogicSemantics❙
-  include ?PLSemantics❙
+  include ?ParametricPLSemantics❙
   comp = [p,q] [u,w] ∃ͭ [v] p u v ∧ q v w❙
   distrib = [p,q] [v,w] p v w ∨ q v w❙
   iteration = [p] [v,w] trclos p v w❙
@@ -41,7 +42,7 @@ view PropDynamicLogicSemantics : latin:/?PropDynamicLogic → ?State =
 
 view TypedDynamicSemantics : latin:/?TypedDynamicLogic → ?State =
   include ?PropDynamicLogicSemantics❙
-  include ?SFOLSemantics❙
+  include ?ParametricSFOLSemantics❙
   var = [S] tm cell S❙
   retrieve = [S,n] [w] n*w❙
   assign = [S,n,x] [v,w] extends v w n x❙ 

source/logic/modal_like/kripke_ltl.mmt

+namespace latin:/kripkemodels❚
+
+// An LTL model is a Kripke model in which a proposition is evaluated at a trace.
+   
+   Atomic formulas are evaluated at the head of the trace.
+   This is not formalized here and must instead be formalized in the translation of the pattern for atom-constructors. E.g., p:prop must be translated to {pW: tm W ⟶ prop, p = [t] pW (t'0)}. 
+❚
+
+theory LTLModel : latin:/?SFOLND =
+  include ?KripkeFrame❙
+  include ?EvaluationInTraces❙
+❚
+
+view LTLSemantics : latin:/?LTL → ?LTLModel =
+  include ?ParametricPLSemantics❙
+  next = [f,t] f (t^1)❙
+  finally = [f,t] ∃ͭ [i] f(t^i)❙
+  always  = [f,t] ∀ͭ [i] f(t^i)❙
+  until = [f,g,t] ∃ͭ [i] ∀ͭ[j] (j<i ⇒ f(t^j)) ∧ g(t^i)❙
+  release = [f,g,t] ∃ͭ [i] ∀ͭ[j] (j≤i ⇒ g(t^j)) ∧ f(t^i) ∨ ∀ͭ[j] g(t^j)❙
+❚

source/logic/model_theory/kripke_multimodal.mmt → source/logic/modal_like/kripke_multimodal.mmt

@@ -2,14 +2,20 @@ namespace latin:/kripkemodels❚
 
 fixmeta ur:?LF❚
 
-view MMLSemantics : latin:/?MML → ?Worlds =
-  include ?LogicSemantics❙
+/T Kripke models for multi-modal logics must provide an accessibility relation for every modal operator.
+❚
+
+view MMLSemantics : latin:/?MML → ?EvaluationInWorlds + latin:/?SFOL =
+  include ?ParametricLogicSemantics❙
+  /T one accessibility per modality❚
   modality = tm W ⟶ tm W ⟶ prop❙
+  /T universal quantification over accessible states❙
   box = [m,p] [v] ∀ͭ [w] m v w ⇒ p w❙
+  /T existential quantification over accessible states❙
   diamond = [m,p] [v] ∃ͭ [w] m v w ∧ p w❙
 ❚
 
-view SMMLSemantics : latin:/?SMML → ?Worlds =
+view SMMLSemantics : latin:/?SMML → ?EvaluationInWorlds + latin:/?HOLND =
   include ?MMLSemantics❙
-  include ?SFOLSemantics❙
+  include ?ParametricSFOLSemantics❙
 ❚

source/logic/modal_like/ltl.mmt

+namespace latin:/❚
+
+fixmeta ur:?LF❚
+
+/T Linear Temporal Logic
+   LTL propositions are meant to be evaluated relative to a trace in a state transition system.
+   Atomic formulas are meant to be evaluated in the first state of the path.❚
+
+/T basic modality (corresponds to box/diamond)❚
+theory Next =
+  include ?Propositions❙
+  /T $◯ p$ means [p:prop] holds in the next state, i.e., relative to the tail of the path.❙
+  next: prop ⟶ prop❘# ◯ 1 prec 20❙
+❚
+
+theory Finally =
+  include ?Propositions❙
+  /T $◇ p$ means [p:prop] holds in some state on the path.❙
+  finally: prop ⟶ prop❘# ◇ 1 prec 20❙
+❚
+
+/T dual of Finally❚
+theory Always =
+  include ?Propositions❙
+  /T $□ p$ means [p:prop] holds everywhere on the path.❙
+  always: prop ⟶ prop❘# □ 1 prec 20❙
+❚
+
+theory Until =
+  include ?Propositions❙
+  /T $p U q$ means [p:prop] holds on a prefix of the path up followed by a state in which [q:prop] holds.❙
+  until: prop ⟶ prop ⟶ prop❘# 1 U 2 prec 20❙
+❚
+
+/T dual of until❚
+theory Release =
+  include ?Propositions❙
+  /T $p R q$ means [q:prop] holds longer than [p:prop] doesn't hold.❙
+  release: prop ⟶ prop ⟶ prop❘# 1 R 2 prec 20❙
+❚
+
+theory LTL =
+  include ?PL❙
+  include ?Next❙
+  include ?Finally❙
+  include ?Always❙
+  include ?Until❙
+  include ?Release❙
+❚
+

source/logic/propositional/modal.mmt → source/logic/modal_like/modal.mmt

@@ -2,6 +2,8 @@ namespace latin:/❚
 
 fixmeta ur:?LF❚
 
+/T Basic modal operators.❚
+
 theory Box =
   include ?Propositions❙
   box: prop ⟶ prop❘# □ 1 prec 20❙
@@ -23,4 +25,4 @@ theory MLHilbert =
   include ?ML❙
   // Rules with hypothetical premises are not sound in Kripke models; so we need to use a Hilbert calculus.❙
   include ?PLHilbert❙
-❚
+❚
\ No newline at end of file

source/logic/fol_like/multimodal.mmt → source/logic/modal_like/multimodal.mmt

@@ -2,6 +2,11 @@ namespace latin:/❚
 
 fixmeta ur:?LF❚
 
+/T Logics with multiple modalities can be formalized by instantiating the box and diamond for each modality.
+   But that process precludes quantifying over modalities.
+   A more scalable obtaining is obtained by using MultiModal as the base language and
+   populating the type 'modality' as needed.❚
+
 theory MultiModal =
   include ?Logic❙
   modality: type❙

source/logic/model_theory/kripke.mmt → source/logic/modal_like/parametric_evaluation.mmt

-namespace latin:/kripkemodels❚
-
-fixmeta ur:?LF❚
-
-theory Worlds : latin:/?HOLND =
-  world: tp❘# W❙
-
-  liftPred2: {S,A,B} (          tm A ⟶           tm B  ⟶          prop)
-                   ⟶ (tm S ⟶ tm A) ⟶ (tm S ⟶ tm B) ⟶ (tm S ⟶ prop)❘
-      = [S,A,B,o,f,g] [x] o (f x) (g x)❘
-      # liftFun2 4❙
-
-  lift0: {S} prop ⟶ (tm S ⟶ prop)❘
-      = [S,o] [x]o❘
-      # lift0 2❙
-  lift1: {S} (prop ⟶ prop) ⟶ (tm S ⟶ prop) ⟶ (tm S ⟶ prop)❘
-      = [S,o,f] [x]o (f x)❘
-      # lift1 2❙
-  lift2: {S} (prop ⟶ prop ⟶ prop) ⟶ (tm S ⟶ prop) ⟶ (tm S ⟶ prop) ⟶ (tm S ⟶ prop)❘
-      = [S,o,f,g] [x]o (f x) (g x)❘
-      # lift2 2❙
-      
-  liftbind : {S} ({T}  (        tm T            ⟶ prop)  ⟶          prop) ⟶
-                  {T} ((tm S ⟶ tm T) ⟶ (tm S ⟶ prop)) ⟶ (tm S ⟶ prop)❘
-           = [S][B][T][F][x] B (S→T) [f] F (apply1 f) x❘
-           # liftbind 2❙
-  
-❚
-
-ref latin:/?DisjunctionHilbert2ND❚
-ref latin:/?NegationHilbert2ND❚
-ref latin:/?ImplicationHilbert2ND❚
-ref latin:/?EquivalenceHilbert2ND❚
-
-theory KripkeFrame : latin:/?TypedLogic =
-  include ?Worlds❙
-  accessible : tm W ⟶ tm W ⟶ prop❘ # 1 acc 2 prec 30❙
-❚
-
-theory KripkeModel =
-  include ☞latin:/?SFOLEQ❙
-  include ?KripkeFrame❙
-❚
-
-view PropSemantics : latin:/?Propositions → ?Worlds =
-  prop = tm W ⟶ prop❙
-❚
-
-view LogicSemantics : latin:/?Logic → ?Worlds =
-  include ?PropSemantics❙
-  ded = [f] {w} ⊦ f w❙
-❚
-
-view PLSemantics : latin:/?PL → ?Worlds =
-  include ?PropSemantics❙
-  true = lift0 true❙
-  false = lift0 false❙
-  and = lift2 and❙
-  or = lift2 or❙
-  impl = lift2 impl❙
-  not = lift1 not❙
-  equiv = lift2 equiv❙
-❚
-
-view PLHilbertSemantics : latin:/?PLHilbert → ?Worlds =
-  include ?PLSemantics❙
-  include ?LogicSemantics❙
-  
-  trueI = [w] trueI❙
-  falseE = [f] [g,w] f w falseE inconE❙
-  
-  andI  = [F,G,f,g][w] andI (f w) (g w)❙
-  andEl = [F,G,fg] [w] fg w andEl❙
-  andEr = [F,G,fg] [w] fg w andEr❙
-
-  orIl = [F,G,f] [w] f w orIl❙
-  orIr = [F,G,f] [w] f w orIr❙
-  orE_ax = [F,G,H][w] orE_ax❙
-  
-  implE = [F,G,fg,f] [w] (fg w) implE (f w)❙
-  K_ax = [F,G,w] K_ax❙
-  S_ax = [F,G,H,w] S_ax❙
-  
-  notI_ax = [F,w] notI_ax❙ 
-  notE = [F,nf,f] [g,w] (nf w) notE (f w) inconE❙
-  
-  equivI_ax = [F,G,w] equivI_ax❙
-  equivEl = [F,G,fg,f] [w] (fg w) equivEl (f w)❙
-  equivEr = [F,G,fg,g] [w] (fg w) equivEr (g w)❙
-  
-  classical = [F,p] [w] classical [Fwincon] [A] p ([Fw,Gv,v] Fwincon (Fw w) (Gv v)) ([u] A) w❙
-❚
-
-view TermSemantics : latin:/?TypedTerms → ?Worlds =
-  /T constant universe; alternative would be tp = tm W ⟶ tp❙
-  tp = tp❙
-  tm = [S] tm W ⟶ tm S❙
-❚
-
-view SFOLSemantics : latin:/?SFOLEQ → ?Worlds =
-  include ?TermSemantics❙
-  include ?PLSemantics❙
-  include ?LogicSemantics❙
-  tforall = liftbind tforall❙
-  texists = liftbind texists❙
-  tequal = [S] liftFun2 (tequal S)❙
-❚
-
-view MLSemantics : latin:/?ML → ?KripkeModel =
-  include ?PLSemantics❙
-  include ?LogicSemantics❙
-  box = [p] [v] ∀ͭ [w] v acc w ⇒ p w❙
-  diamond = [p] [v] ∃ͭ [w] v acc w ∧ p w❙ 
-❚
-
-view MLHilbertSemantics : latin:/?MLHilbert → ?KripkeModel =
-  include ?MLSemantics❙
-  include ?PLHilbertSemantics❙
-❚
+namespace latin:/kripkemodels❚
+
+fixmeta ur:?LF❚
+
+/T The views in this file lift the interpretation of the usual connectives from Booleans to a parametrized family of Booleans.
+For example, ⟦F ∧ G⟧(p) = ⟦F⟧(p)∧⟦G⟧(p).  
+These can be used in, e.g., Kripke models, where p is the current world.
+Truth is lifted by requiring the parametrized family to be true everywhere.
+
+By keeping the parameter type flexible, different indexing choices are possible, e.g., world-indexed vs. trace-indexed evaluation.
+
+The theory EvaluationParameter should be realized by the codomain of the interpretation to define the parameter type.
+Then the views can be included into the interpretation.
+❚
+
+theory EvaluationParameter : latin:/?TypedLogic =
+  param : tp❙
+❚
+
+view ParametricPropSemantics : latin:/?Propositions → ?EvaluationParameter =
+  prop = tm param ⟶ prop❙
+❚
+
+view ParametricLogicSemantics : latin:/?Logic → ?EvaluationParameter =
+  include ?ParametricPropSemantics❙
+  ded = [f] {x} ⊦ f x❙
+❚
+
+ref latin:/?DisjunctionHilbert2ND❚
+ref latin:/?NegationHilbert2ND❚
+ref latin:/?ImplicationHilbert2ND❚
+ref latin:/?EquivalenceHilbert2ND❚
+
+view ParametricPLSemantics : latin:/?PL → ?EvaluationParameter + latin:/?PL =
+  include ?ParametricPropSemantics❙
+  true = lift0 true❙
+  false = lift0 false❙
+  and = lift2 and❙
+  or = lift2 or❙
+  impl = lift2 impl❙
+  not = lift1 not❙
+  equiv = lift2 equiv❙
+❚
+
+view ParametricPLHilbertSemantics : latin:/?PLHilbert → ?EvaluationParameter + latin:/?PLND =
+  include ?ParametricPLSemantics❙
+  include ?ParametricLogicSemantics❙
+  
+  trueI = [w] trueI❙
+  falseE = [f] [g,w] f w falseE inconE❙
+  
+  andI  = [F,G,f,g][w] andI (f w) (g w)❙
+  andEl = [F,G,fg] [w] fg w andEl❙
+  andEr = [F,G,fg] [w] fg w andEr❙
+
+  orIl = [F,G,f] [w] f w orIl❙
+  orIr = [F,G,f] [w] f w orIr❙
+  orE_ax = [F,G,H][w] orE_ax❙
+  
+  implE = [F,G,fg,f] [w] (fg w) implE (f w)❙
+  K_ax = [F,G,w] K_ax❙
+  S_ax = [F,G,H,w] S_ax❙
+  
+  notI_ax = [F,w] notI_ax❙ 
+  notE = [F,nf,f] [g,w] (nf w) notE (f w) inconE❙
+  
+  equivI_ax = [F,G,w] equivI_ax❙
+  equivEl = [F,G,fg,f] [w] (fg w) equivEl (f w)❙
+  equivEr = [F,G,fg,g] [w] (fg w) equivEr (g w)❙
+  
+  classical = [F,p] [w] classical [Fwincon] [A] p ([Fw,Gv,v] Fwincon (Fw w) (Gv v)) ([u] A) w❙
+❚
+
+view ParametricTermSemantics : latin:/?TypedTerms → ?EvaluationParameter =
+  /T constant universe; alternative would be tp = tm W ⟶ tp❙
+  tp = tp❙
+  tm = [S] tm param ⟶ tm S❙
+❚
+
+view ParametricSFOLSemantics : latin:/?SFOLEQ → ?EvaluationParameter + latin:/?HOLND =
+  include ?ParametricTermSemantics❙
+  include ?ParametricPLSemantics❙
+  include ?ParametricLogicSemantics❙
+  tforall = liftbind tforall❙
+  texists = liftbind texists❙
+  tequal = [S] liftFun2 (tequal S)❙
+❚

source/logic/model_theory/build.msl

-file ../../../build_config.msl
-
-// model_theory
-// depends in general on fundamentals and big parts of logic (these dependencies are not mentioned here)!
-
-// no dependencies
-build MMT/LATIN2 mmt-omdoc logic/model_theory/kripke.mmt
-
-// dependent on kripke
-build MMT/LATIN2 mmt-omdoc logic/model_theory/kripke_multimodal.mmt
-
-// dependent on kripke and kripke_multimodal
-build MMT/LATIN2 mmt-omdoc logic/model_theory/kripke_dynamic.mmt

source/logic/propositional/build.msl

@@ -14,6 +14,3 @@ build MMT/LATIN2 mmt-omdoc logic/propositional/pl_hilbert.mmt
 build MMT/LATIN2 mmt-omdoc logic/propositional/pl_derived.mmt
 build MMT/LATIN2 mmt-omdoc logic/propositional/pl-tableaux.mmt
 build MMT/LATIN2 mmt-omdoc logic/propositional/pl-views.mmt
-
-// dependent on pl and pl_hilbert
-build MMT/LATIN2 mmt-omdoc logic/propositional/modal.mmt

source/logic/substructural/build.msl

+file ../../../build_config.msl
+
+build . mmt-omdoc ./linear.mmt