L_TU: A Logic for Truth-Conditional and Use-Conditional Meaning

@cite{gutzmann-2015}

The central formal contribution of @cite{gutzmann-2015}'s "Use-Conditional Meaning": a three-dimensional compositional semantics that extends @cite{potts-2005}'s two-dimensional L_CI.

Key Insight

Every expression carries three meaning dimensions:

• t-dim: truth-conditional content (evaluated at worlds)
• s-dim: active use-conditional content (being composed, world-indexed)
• u-dim: completed use-conditional propositions (evaluated at contexts)

The s-dimension is a staging area: use-conditional content composes there before being "stored" in the u-dimension via use-conditional elimination (UE). After UE, the t-dimension copies back into s-dim, making it available for further truth-conditional composition.

Composition

Two rules drive the system:

1. Multidimensional application (MA): applies t-dims pointwise, s-dims pointwise, and merges u-dims via conjunction.
2. Use-conditional elimination (UE): when the s-dim reaches type u, shift it to u-dim (conjoining with existing u-content) and reset s-dim to a copy of t-dim.

UCI Typology

Use-conditional items (UCIs) are classified by three binary features:

• [±functional]: does the UCI take a truth-conditional argument?
• [±2-dimensional]: does the UCI contribute to both dimensions?
• [±resource-sensitive]: is the UCI's argument "consumed" (shunted)?

These yield five valid UCI classes (isolated expletive, isolated mixed, functional expletive, functional shunting, functional mixed).

inductive Semantics.UseConditional.UCType : Type

The L_TU type system (@cite{gutzmann-2015}, (4.45)).

Basic types: e (entities), t (truth values), u (use-conditional propositions, opaque). A type is use-conditional iff it equals u or is a function type whose codomain is use-conditional.

• e : UCType
• t : UCType
• u : UCType
• func : UCType → UCType → UCType

def Semantics.UseConditional.instDecidableEqUCType.decEq (x✝ x✝¹ : UCType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.e Semantics.UseConditional.UCType.e = isTrue ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.e Semantics.UseConditional.UCType.t = isFalse Semantics.UseConditional.instDecidableEqUCType.decEq._proof_1
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.e Semantics.UseConditional.UCType.u = isFalse Semantics.UseConditional.instDecidableEqUCType.decEq._proof_2
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.e (a.func a_1) = isFalse ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.t Semantics.UseConditional.UCType.e = isFalse Semantics.UseConditional.instDecidableEqUCType.decEq._proof_4
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.t Semantics.UseConditional.UCType.t = isTrue ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.t Semantics.UseConditional.UCType.u = isFalse Semantics.UseConditional.instDecidableEqUCType.decEq._proof_5
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.t (a.func a_1) = isFalse ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.u Semantics.UseConditional.UCType.e = isFalse Semantics.UseConditional.instDecidableEqUCType.decEq._proof_7
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.u Semantics.UseConditional.UCType.t = isFalse Semantics.UseConditional.instDecidableEqUCType.decEq._proof_8
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.u Semantics.UseConditional.UCType.u = isTrue ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq Semantics.UseConditional.UCType.u (a.func a_1) = isFalse ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq (a.func a_1) Semantics.UseConditional.UCType.e = isFalse ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq (a.func a_1) Semantics.UseConditional.UCType.t = isFalse ⋯
• Semantics.UseConditional.instDecidableEqUCType.decEq (a.func a_1) Semantics.UseConditional.UCType.u = isFalse ⋯

@[implicit_reducible]

instance Semantics.UseConditional.instDecidableEqUCType : DecidableEq UCType

Equations

• Semantics.UseConditional.instDecidableEqUCType = Semantics.UseConditional.instDecidableEqUCType.decEq

def Semantics.UseConditional.instReprUCType.repr : UCType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.UseConditional.instReprUCType : Repr UCType

Equations

• Semantics.UseConditional.instReprUCType = { reprPrec := Semantics.UseConditional.instReprUCType.repr }

def Semantics.UseConditional.UCType.IsUCType : UCType → Prop

A type is use-conditional iff it is u or a function into a use-conditional type. This determines which dimension an expression's content targets during composition.

Equations

• Semantics.UseConditional.UCType.u.IsUCType = True
• (a.func τ).IsUCType = τ.IsUCType
• x✝.IsUCType = False

@[implicit_reducible]

instance Semantics.UseConditional.UCType.decIsUCType : DecidablePred IsUCType

Equations

• Semantics.UseConditional.UCType.e.decIsUCType = isFalse ⋯
• Semantics.UseConditional.UCType.t.decIsUCType = isFalse ⋯
• Semantics.UseConditional.UCType.u.decIsUCType = isTrue trivial
• (a.func a_1).decIsUCType = a_1.decIsUCType

theorem Semantics.UseConditional.u_is_uc : UCType.u.IsUCType

theorem Semantics.UseConditional.t_is_not_uc : ¬UCType.t.IsUCType

theorem Semantics.UseConditional.func_into_u_is_uc : (UCType.e.func UCType.u).IsUCType

structure Semantics.UseConditional.UCIClass : Type

UCI classification by three binary features (@cite{gutzmann-2015}, Ch 2).

• functional: takes a truth-conditional argument (vs isolated)
• twoDimensional: contributes to both t-dim and s-dim (vs expletive)
• resourceSensitive: argument is consumed/shunted (vs passed through)

• functional : Bool
• twoDimensional : Bool
• resourceSensitive : Bool

def Semantics.UseConditional.instDecidableEqUCIClass.decEq (x✝ x✝¹ : UCIClass) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.UseConditional.instDecidableEqUCIClass : DecidableEq UCIClass

Equations

• Semantics.UseConditional.instDecidableEqUCIClass = Semantics.UseConditional.instDecidableEqUCIClass.decEq

@[implicit_reducible]

instance Semantics.UseConditional.instReprUCIClass : Repr UCIClass

Equations

• Semantics.UseConditional.instReprUCIClass = { reprPrec := Semantics.UseConditional.instReprUCIClass.repr }

def Semantics.UseConditional.instReprUCIClass.repr : UCIClass → ℕ → Std.Format

Equations

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

def Semantics.UseConditional.isolatedExpletive : UCIClass

Isolated expletive: no argument, only use-conditional content. Example: damn in "the damn dog."

Equations

• Semantics.UseConditional.isolatedExpletive = { functional := false, twoDimensional := false, resourceSensitive := false }

def Semantics.UseConditional.isolatedMixed : UCIClass

Isolated mixed: no argument, contributes to both dimensions. Example: ethnic slurs with descriptive + expressive content.

Equations

• Semantics.UseConditional.isolatedMixed = { functional := false, twoDimensional := true, resourceSensitive := false }

def Semantics.UseConditional.functionalExpletive : UCIClass

Functional expletive: takes an argument, only use-conditional output. Example: German modal particles ja, denn; sentence mood operators.

Equations

• Semantics.UseConditional.functionalExpletive = { functional := true, twoDimensional := false, resourceSensitive := false }

def Semantics.UseConditional.functionalShunting : UCIClass

Functional shunting: takes an argument that is consumed (not returned). Example: @cite{potts-2005}'s comma feature for appositives.

Equations

• Semantics.UseConditional.functionalShunting = { functional := true, twoDimensional := false, resourceSensitive := true }

def Semantics.UseConditional.functionalMixed : UCIClass

Functional mixed: takes an argument, contributes to both dimensions. Example: some honorific systems.

Equations

• Semantics.UseConditional.functionalMixed = { functional := true, twoDimensional := true, resourceSensitive := false }

inductive Semantics.UseConditional.UCExprKind : Type

How a use-conditional expression interacts with composition (@cite{gutzmann-2015}, §6.5).

A UCI is a use-conditional item: it contributes u-content by taking truth-conditional arguments. A UC-modifier takes another UCI as its argument and modifies its use-conditional behavior.

This distinction drives two different mechanisms for mood restriction:

• UCIs are restricted by use-conditional conflict (their independent u-content is incompatible with certain mood operators)
• UC-modifiers are restricted selectionally (the mood operator they modify is absent from certain clause types)

• uci : UCExprKind

  Use-conditional item: maps truth-conditional content to u-content. Type: ⟨⟨s,t⟩, u⟩ (functional) or u (isolated).

• ucModifier : UCExprKind

  Use-conditional modifier: maps UCIs to UCIs. Type: ⟨⟨⟨s,t⟩,u⟩, ⟨⟨s,t⟩,u⟩⟩. Modifies an existing mood operator (e.g., German wohl modifies EPIS).

@[implicit_reducible]

instance Semantics.UseConditional.instDecidableEqUCExprKind : DecidableEq UCExprKind

Equations

• Semantics.UseConditional.instDecidableEqUCExprKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.UseConditional.instReprUCExprKind : Repr UCExprKind

Equations

• Semantics.UseConditional.instReprUCExprKind = { reprPrec := Semantics.UseConditional.instReprUCExprKind.repr }

def Semantics.UseConditional.instReprUCExprKind.repr : UCExprKind → ℕ → Std.Format

Equations

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

inductive Semantics.UseConditional.RestrictionKind : Type

How an expression's mood restriction arises (@cite{gutzmann-2015}, §6.5).

The two mechanisms are empirically distinguishable: selectional restrictions produce type-mismatch infelicity, while use-conditional conflict produces pragmatic deviance.

• selectional : RestrictionKind

  The expression modifies a mood operator that is absent from certain clause types — a type mismatch. Example: German wohl modifies EPIS, which is absent from imperatives.

• ucConflict : RestrictionKind

  The expression's independent u-content is incompatible with certain sentence moods. Example: German ja's common-ground reminder conflicts with the epistemic uncertainty of interrogatives.

@[implicit_reducible]

instance Semantics.UseConditional.instDecidableEqRestrictionKind : DecidableEq RestrictionKind

Equations

• Semantics.UseConditional.instDecidableEqRestrictionKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.UseConditional.instReprRestrictionKind.repr : RestrictionKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.UseConditional.instReprRestrictionKind : Repr RestrictionKind

Equations

• Semantics.UseConditional.instReprRestrictionKind = { reprPrec := Semantics.UseConditional.instReprRestrictionKind.repr }

structure Semantics.UseConditional.ThreeDimMeaning (C : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A three-dimensional meaning in L_TU (@cite{gutzmann-2015}, (4.46)).

C is the context type (for use-conditional propositions, sets of contexts), W is the world type (for truth-conditional propositions, sets of worlds).

The crucial type distinction: uDim is C → Bool while tDim/sDim are W → Bool. Use-conditional propositions constrain the context of utterance, not the described world — matching Kaplan's character/content distinction.

• tDim : W → Prop

  Truth-conditional content: the at-issue proposition

• sDim : W → Prop

  Active use-conditional content being composed

• uDim : C → Prop

  Completed use-conditional propositions (stored, inaccessible to further truth-conditional composition)

def Semantics.UseConditional.multidimApp {C : Type u_1} {W : Type u_2} (f a : ThreeDimMeaning C W) : ThreeDimMeaning C W

Multidimensional application (@cite{gutzmann-2015}, (4.46)).

The full MA rule applies functions intradimensionally: dimension 1 applies σ(β₁), dimension 2 applies ρ(β₂), and u-dimensions merge via ⊙ (conjunction). At the propositional level — where both inputs are already of type ⟨s,t⟩ — function application reduces to pointwise conjunction, which is what this definition implements. The sub-propositional case (where dims 1-2 are genuine function applications) is not formalized.

Equations

• Semantics.UseConditional.multidimApp f a = { tDim := fun (w : W) => f.tDim w ∧ a.tDim w, sDim := fun (w : W) => f.sDim w ∧ a.sDim w, uDim := fun (c : C) => f.uDim c ∧ a.uDim c }

def Semantics.UseConditional.ucElim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (eval : (W → Prop) → C → Prop) : ThreeDimMeaning C W

Use-conditional elimination (@cite{gutzmann-2015}, (4.54)).

When the s-dimension reaches type u (its content is a completed use-conditional proposition), UE:

1. Shifts s-dim content to u-dim (conjoining with existing u-content)
2. Resets s-dim to a copy of t-dim

The eval parameter bridges the world-indexed s-dim to the context-indexed u-dim, typically by projecting the world from the context.

Equations

• Semantics.UseConditional.ucElim m eval = { tDim := m.tDim, sDim := m.tDim, uDim := fun (c : C) => m.uDim c ∧ eval m.sDim c }

def Semantics.UseConditional.ofTruthConditional {C : Type u_1} {W : Type u_2} (p : W → Prop) : ThreeDimMeaning C W

Lift a truth-conditional proposition to a three-dimensional meaning.

Both t-dim and s-dim carry the propositional content. u-dim is trivially satisfied (no use-conditional content yet). Corresponds to a pure truth-conditional lexical item before LER extension.

Equations

• Semantics.UseConditional.ofTruthConditional p = { tDim := p, sDim := p, uDim := fun (x : C) => True }

def Semantics.UseConditional.ofUCI {C : Type u_1} {W : Type u_2} (ucContent : W → Prop) : ThreeDimMeaning C W

Lift a use-conditional function to a three-dimensional meaning.

t-dim is trivially true (UCIs do not contribute truth conditions). s-dim carries the active UCI content. u-dim is trivially true until ucElim fires.

Equations

• Semantics.UseConditional.ofUCI ucContent = { tDim := fun (x : W) => True, sDim := ucContent, uDim := fun (x : C) => True }

def Semantics.UseConditional.toTwoDim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (evalU : (C → Prop) → W → Prop) : Pragmatics.Expressives.TwoDimProp W

Project a three-dimensional meaning to a TwoDimProp (final interpretation).

After all composition and UE steps, the final meaning of a sentence has t-dim = truth-conditional content and u-dim = accumulated use-conditional propositions. The s-dim equals t-dim (reset by UE) and is discarded.

The evalU function projects the context-indexed u-dim (C → Bool) to a world-indexed CI content (W → Bool) for the TwoDimProp.ci field. This corresponds to @cite{gutzmann-2015}'s lowering operator ⇓_c which converts u-propositions to world sets by fixing context parameters except the world.

Equations

• Semantics.UseConditional.toTwoDim m evalU = { atIssue := m.tDim, ci := evalU m.uDim }

theorem Semantics.UseConditional.ucElim_preserves_tDim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (eval : (W → Prop) → C → Prop) : (ucElim m eval).tDim = m.tDim

UE does not affect truth conditions.

This is the formal guarantee of non-interaction: storing use-conditional content in the u-dimension never changes what a sentence says about the world.

theorem Semantics.UseConditional.ucElim_resets_sDim {C : Type u_1} {W : Type u_2} (m : ThreeDimMeaning C W) (eval : (W → Prop) → C → Prop) : (ucElim m eval).sDim = m.tDim

After UE, the s-dimension is reset to the t-dimension.

theorem Semantics.UseConditional.multidimApp_merges_uDim {C : Type u_1} {W : Type u_2} (f a : ThreeDimMeaning C W) (c : C) : (multidimApp f a).uDim c ↔ f.uDim c ∧ a.uDim c

MA merges u-dimensions via conjunction. Completed use-conditional propositions from both constituents are preserved.

theorem Semantics.UseConditional.ofTruthConditional_trivial_uDim {C : Type u_1} {W : Type u_2} (p : W → Prop) (c : C) : (ofTruthConditional p).uDim c

A pure truth-conditional expression has trivial use conditions.

theorem Semantics.UseConditional.ofUCI_trivial_tDim {C : Type u_1} {W : Type u_2} (ucContent : W → Prop) (w : W) : (ofUCI ucContent).tDim w

A UCI has trivial truth conditions.

inductive Semantics.UseConditional.LTUDeriv (C : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A derivation in the propositional fragment of L_TU.

Derivation trees encode the composition history: which expressions were combined via MA, and where UE was applied. This lets us state and prove properties of all possible derivations, not just specific ones.

• leaf {C : Type u_1} {W : Type u_2} : ThreeDimMeaning C W → LTUDeriv C W

  A lexical item (leaf of the derivation tree)

• app {C : Type u_1} {W : Type u_2} : LTUDeriv C W → LTUDeriv C W → LTUDeriv C W

  Multidimensional application of two sub-derivations

• elim {C : Type u_1} {W : Type u_2} : LTUDeriv C W → ((W → Prop) → C → Prop) → LTUDeriv C W

  Use-conditional elimination applied to a sub-derivation

def Semantics.UseConditional.LTUDeriv.eval {C : Type u_1} {W : Type u_2} : LTUDeriv C W → ThreeDimMeaning C W

Evaluate a derivation to its three-dimensional meaning.

Equations

• (Semantics.UseConditional.LTUDeriv.leaf m).eval = m
• (d₁.app d₂).eval = Semantics.UseConditional.multidimApp d₁.eval d₂.eval
• (d.elim f).eval = Semantics.UseConditional.ucElim d.eval f

def Semantics.UseConditional.LTUDeriv.stripUC {C : Type u_1} {W : Type u_2} : LTUDeriv C W → LTUDeriv C W

Strip all use-conditional content from a derivation's leaves, replacing s-dim with t-dim and u-dim with trivial content. This produces a "truth-conditional shadow" of the derivation.

Equations

• (Semantics.UseConditional.LTUDeriv.leaf m).stripUC = Semantics.UseConditional.LTUDeriv.leaf { tDim := m.tDim, sDim := m.tDim, uDim := fun (x : C) => True }
• (d₁.app d₂).stripUC = d₁.stripUC.app d₂.stripUC
• (d.elim f).stripUC = d.stripUC.elim f

theorem Semantics.UseConditional.non_interaction {C : Type u_1} {W : Type u_2} (d : LTUDeriv C W) (w : W) : d.eval.tDim w ↔ d.stripUC.eval.tDim w

Non-interaction theorem (@cite{gutzmann-2015}).

For ANY derivation built from multidimensional application and use-conditional elimination, the truth-conditional content of the result depends ONLY on the truth-conditional content of the inputs.

Stripping all use-conditional content from the leaves does not change the final t-dimension. Use-conditional meaning can never leak into truth conditions — not through MA, not through UE, not through any combination of the two. This is the fundamental architectural guarantee of L_TU.

theorem Semantics.UseConditional.non_interaction_ext {C : Type u_1} {W : Type u_2} (d : LTUDeriv C W) : d.eval.tDim = d.stripUC.eval.tDim

Non-interaction at the function level (extensional form).

theorem Semantics.UseConditional.multidimApp_uci_tDim {C : Type u_1} {W : Type u_2} (tc uci : ThreeDimMeaning C W) (h : ∀ (w : W), uci.tDim w) (w : W) : (multidimApp tc uci).tDim w ↔ tc.tDim w

Composing with a UCI does not change truth conditions.

When a functional expletive UCI (with trivial t-dim) is composed with truth-conditional content via MA, the t-dim of the result equals the t-dim of the truth-conditional input. This is the formal content of "UCIs do not contribute truth conditions."

theorem Semantics.UseConditional.multidimApp_tc_preserves_uci_tDim {C : Type u_1} {W : Type u_2} (uci tc : ThreeDimMeaning C W) (h : ∀ (w : W), uci.tDim w) (w : W) : (multidimApp uci tc).tDim w ↔ tc.tDim w

Composing with truth-conditional content does not change truth conditions of an expression whose t-dim is already trivial.

theorem Semantics.UseConditional.toTwoDim_multidimApp {C : Type u_1} {W : Type u_2} (f a : ThreeDimMeaning C W) (evalU : (C → Prop) → W → Prop) (hConj : ∀ (p q : C → Prop) (w : W), evalU (fun (c : C) => p c ∧ q c) w ↔ evalU p w ∧ evalU q w) : toTwoDim (multidimApp f a) evalU = (toTwoDim f evalU).and (toTwoDim a evalU)

The 3D→2D bridge commutes with MA when the lowering operator distributes over conjunction.

If evalU preserves conjunctive structure (i.e., lowering a conjunction of u-propositions equals the conjunction of lowered u-propositions), then projecting a composed 3D meaning to 2D is the same as composing the individual 2D projections.

This is the formal guarantee that L_TU's 3D composition "collapses" correctly into @cite{potts-2005}'s 2D framework.