Syntax of PIP

This file defines the terms and formulas of PIP, a plural intensional presuppositional predicate calculus: first-order predicate calculus with set abstraction, equality, the set-theoretic relations ⊆, ∈, ∩, ∅ and the cardinality predicates SG and PL, extended by bracketed local variables [x], summation Σxφ, formula labels X ≡ φ with their uses X, world arguments on relation symbols, and presuppositions φ|ψ. Relation symbols are indexed by arity and take a world as a distinguished argument. Terms and formulas are one inductive type indexed by their kind.

It also defines the local variables of an expression, substitution for a variable, the presupposition-free expressions, the expansion of formula labels by their definitions, and the translation eliminating the PIP constructs. Truth is defined in Semantics.lean and felicity in Felicity.lean.

Main definitions

• Kind, Expr, Term, Formula — the syntax; Formula.disj, Formula.impl, Formula.iff_, Formula.forall_, Formula.some_ — the defined connectives; Term.sgPronoun — a singular summation pronoun.
• Expr.locals — the local variables; Expr.subst — substitution for a variable.
• Expr.PresupFree — expressions without presuppositions, decidably.
• Expr.substLabels, Expr.defs, assignment, Formula.expand, Formula.expandSelf — label assignment and expansion, as a bounded fixpoint of simultaneous substitution.
• Formula.closeList, Expr.elim — the translation into predicate calculus with set abstraction.

References

• [keshet-abney-2024]
• [abney-keshet-2025]

inductive PIP.Kind : Type

The kinds of PIP expressions.

• term : Kind
• formula : Kind

inductive PIP.Expr (V : Type u) (L : Type v) (P : ℕ → Type w) : Kind → Type (max u v w)

PIP expressions. Terms: external variables, bracketed local variables [x], set abstraction ⋃{x : φ}, summation Σxφ, intersection and the empty plurality. Formulas: the constant ⊤, predication P_w(τ₁, …, τₙ), equality, inclusion, membership, the cardinality predicates SG and PL, negation, conjunction, selective existential quantification, label definition X ≡ φ and label use X. An expression of either kind with a presupposition, e|ψ.

• var {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) : Expr V L P Kind.term
• bvar {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) : Expr V L P Kind.term
• abs {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) (φ : Expr V L P Kind.formula) : Expr V L P Kind.term
• sigma {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) (φ : Expr V L P Kind.formula) : Expr V L P Kind.term
• inter {V : Type u} {L : Type v} {P : ℕ → Type w} (s t : Expr V L P Kind.term) : Expr V L P Kind.term
• empty {V : Type u} {L : Type v} {P : ℕ → Type w} : Expr V L P Kind.term
• top {V : Type u} {L : Type v} {P : ℕ → Type w} : Expr V L P Kind.formula
• atom {V : Type u} {L : Type v} {P : ℕ → Type w} {n : ℕ} (r : P n) (w : Expr V L P Kind.term) (ts : Fin n → Expr V L P Kind.term) : Expr V L P Kind.formula
• eq {V : Type u} {L : Type v} {P : ℕ → Type w} (s t : Expr V L P Kind.term) : Expr V L P Kind.formula
• subset {V : Type u} {L : Type v} {P : ℕ → Type w} (s t : Expr V L P Kind.term) : Expr V L P Kind.formula
• mem {V : Type u} {L : Type v} {P : ℕ → Type w} (s t : Expr V L P Kind.term) : Expr V L P Kind.formula
• sg {V : Type u} {L : Type v} {P : ℕ → Type w} (t : Expr V L P Kind.term) : Expr V L P Kind.formula
• pl {V : Type u} {L : Type v} {P : ℕ → Type w} (t : Expr V L P Kind.term) : Expr V L P Kind.formula
• neg {V : Type u} {L : Type v} {P : ℕ → Type w} (φ : Expr V L P Kind.formula) : Expr V L P Kind.formula
• conj {V : Type u} {L : Type v} {P : ℕ → Type w} (φ ψ : Expr V L P Kind.formula) : Expr V L P Kind.formula
• exists_ {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) (φ : Expr V L P Kind.formula) : Expr V L P Kind.formula
• labelDef {V : Type u} {L : Type v} {P : ℕ → Type w} (X : L) (φ : Expr V L P Kind.formula) : Expr V L P Kind.formula
• label {V : Type u} {L : Type v} {P : ℕ → Type w} (X : L) : Expr V L P Kind.formula
• presup {V : Type u} {L : Type v} {P : ℕ → Type w} {k : Kind} (e : Expr V L P k) (ψ : Expr V L P Kind.formula) : Expr V L P k

@[reducible, inline]

abbrev PIP.Term (V : Type u) (L : Type v) (P : ℕ → Type w) : Type (max u v w)

Terms.

Equations

• PIP.Term V L P = PIP.Expr V L P PIP.Kind.term

@[reducible, inline]

abbrev PIP.Formula (V : Type u) (L : Type v) (P : ℕ → Type w) : Type (max u v w)

Formulas.

Equations

• PIP.Formula V L P = PIP.Expr V L P PIP.Kind.formula

def PIP.Formula.disj {V : Type u} {L : Type v} {P : ℕ → Type w} (φ ψ : Formula V L P) : Formula V L P

Disjunction, as ¬(¬φ ∧ ¬ψ).

Equations

• φ.disj ψ = ((PIP.Expr.neg φ).conj (PIP.Expr.neg ψ)).neg

def PIP.Formula.impl {V : Type u} {L : Type v} {P : ℕ → Type w} (φ ψ : Formula V L P) : Formula V L P

Implication, as ¬(φ ∧ ¬ψ).

Equations

• φ.impl ψ = (PIP.Expr.conj φ (PIP.Expr.neg ψ)).neg

def PIP.Formula.iff_ {V : Type u} {L : Type v} {P : ℕ → Type w} (φ ψ : Formula V L P) : Formula V L P

Biconditional, as (φ → ψ) ∧ (ψ → φ).

Equations

• φ.iff_ ψ = PIP.Expr.conj (φ.impl ψ) (ψ.impl φ)

def PIP.Formula.forall_ {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) (φ : Formula V L P) : Formula V L P

Universal quantification, as ¬∃x¬φ.

Equations

• PIP.Formula.forall_ x φ = (PIP.Expr.exists_ x (PIP.Expr.neg φ)).neg

def PIP.Formula.some_ {V : Type u} {L : Type v} {P : ℕ → Type w} (s t : Term V L P) : Formula V L P

Overlap some(s, t), as ¬(s ∩ t = ∅).

Equations

• PIP.Formula.some_ s t = ((PIP.Expr.inter s t).eq PIP.Expr.empty).neg

def PIP.Term.sgPronoun {V : Type u} {L : Type v} {P : ℕ → Type w} (x : V) (φ : Formula V L P) : Term V L P

Σxφ | SG(Σxφ): a singular summation pronoun over the description φ.

Equations

• PIP.Term.sgPronoun x φ = (PIP.Expr.sigma x φ).presup (PIP.Expr.sigma x φ).sg

Local variables and substitution

def PIP.Expr.locals {V : Type u} {L : Type v} {P : ℕ → Type w} [DecidableEq V] {k : Kind} : Expr V L P k → List V

The local variables of an expression: bracketed occurrences at top level, with summation, set abstraction and quantification binding theirs.

Equations

• (PIP.Expr.var x_2).locals = []
• (PIP.Expr.bvar x_2).locals = [x_2]
• (PIP.Expr.abs x_2 φ).locals = List.filter (fun (x : V) => decide (x ≠ x_2)) φ.locals
• (PIP.Expr.sigma x_2 φ).locals = []
• (s.inter t).locals = s.locals ++ t.locals
• PIP.Expr.empty.locals = []
• PIP.Expr.top.locals = []
• (PIP.Expr.atom r w ts).locals = w.locals ++ List.flatMap (fun (i : Fin n) => (ts i).locals) (List.finRange n)
• (s.eq t).locals = s.locals ++ t.locals
• (s.subset t).locals = s.locals ++ t.locals
• (s.mem t).locals = s.locals ++ t.locals
• t.sg.locals = t.locals
• t.pl.locals = t.locals
• φ.neg.locals = φ.locals
• (φ.conj ψ).locals = φ.locals ++ ψ.locals
• (PIP.Expr.exists_ x_2 φ).locals = List.filter (fun (x : V) => decide (x ≠ x_2)) φ.locals
• (PIP.Expr.labelDef X φ).locals = []
• (PIP.Expr.label X).locals = []
• (e.presup ψ).locals = e.locals ++ ψ.locals

def PIP.Term.bracket {V : Type u} {L : Type v} {P : ℕ → Type w} : Term V L P → Term V L P

Bracket a variable: [x] for x; other terms are unchanged.

Equations

• PIP.Term.bracket (PIP.Expr.var x_1) = PIP.Expr.bvar x_1
• x✝.bracket = x✝

def PIP.Expr.subst {V : Type u} {L : Type v} {P : ℕ → Type w} [DecidableEq V] (x : V) (t : Term V L P) {k : Kind} : Expr V L P k → Expr V L P k

Substitute t for the variable x, the β-reduction of λx: a bracketed occurrence [x] becomes the bracketed substitute, binders of x are skipped, and no capture check is made.

Equations

• PIP.Expr.subst x t (PIP.Expr.var x_3) = if x_3 = x then t else PIP.Expr.var x_3
• PIP.Expr.subst x t (PIP.Expr.bvar x_3) = if x_3 = x then t.bracket else PIP.Expr.bvar x_3
• PIP.Expr.subst x t (PIP.Expr.abs x_3 φ) = PIP.Expr.abs x_3 (if x_3 = x then φ else PIP.Expr.subst x t φ)
• PIP.Expr.subst x t (PIP.Expr.sigma x_3 φ) = PIP.Expr.sigma x_3 (if x_3 = x then φ else PIP.Expr.subst x t φ)
• PIP.Expr.subst x t (s.inter t_1) = (PIP.Expr.subst x t s).inter (PIP.Expr.subst x t t_1)
• PIP.Expr.subst x t PIP.Expr.empty = PIP.Expr.empty
• PIP.Expr.subst x t PIP.Expr.top = PIP.Expr.top
• PIP.Expr.subst x t (PIP.Expr.atom r w ts) = PIP.Expr.atom r (PIP.Expr.subst x t w) fun (i : Fin n) => PIP.Expr.subst x t (ts i)
• PIP.Expr.subst x t (s.eq t_1) = (PIP.Expr.subst x t s).eq (PIP.Expr.subst x t t_1)
• PIP.Expr.subst x t (s.subset t_1) = (PIP.Expr.subst x t s).subset (PIP.Expr.subst x t t_1)
• PIP.Expr.subst x t (s.mem t_1) = (PIP.Expr.subst x t s).mem (PIP.Expr.subst x t t_1)
• PIP.Expr.subst x t t_1.sg = (PIP.Expr.subst x t t_1).sg
• PIP.Expr.subst x t t_1.pl = (PIP.Expr.subst x t t_1).pl
• PIP.Expr.subst x t φ.neg = (PIP.Expr.subst x t φ).neg
• PIP.Expr.subst x t (φ.conj ψ) = (PIP.Expr.subst x t φ).conj (PIP.Expr.subst x t ψ)
• PIP.Expr.subst x t (PIP.Expr.exists_ x_3 φ) = PIP.Expr.exists_ x_3 (if x_3 = x then φ else PIP.Expr.subst x t φ)
• PIP.Expr.subst x t (PIP.Expr.labelDef X φ) = PIP.Expr.labelDef X (PIP.Expr.subst x t φ)
• PIP.Expr.subst x t (PIP.Expr.label X) = PIP.Expr.label X
• PIP.Expr.subst x t (e.presup ψ) = (PIP.Expr.subst x t e).presup (PIP.Expr.subst x t ψ)

Expressions without presuppositions

def PIP.Expr.PresupFree {V : Type u} {L : Type v} {P : ℕ → Type w} {k : Kind} : Expr V L P k → Prop

An expression with no presupposition operator and no label use.

Equations

• (PIP.Expr.var x_2).PresupFree = True
• (PIP.Expr.bvar x_2).PresupFree = True
• (PIP.Expr.abs x_2 φ).PresupFree = φ.PresupFree
• (PIP.Expr.sigma x_2 φ).PresupFree = φ.PresupFree
• (s.inter t).PresupFree = (s.PresupFree ∧ t.PresupFree)
• PIP.Expr.empty.PresupFree = True
• PIP.Expr.top.PresupFree = True
• (PIP.Expr.atom r w ts).PresupFree = (w.PresupFree ∧ ∀ (i : Fin n), i ∈ List.finRange n → (ts i).PresupFree)
• (s.eq t).PresupFree = (s.PresupFree ∧ t.PresupFree)
• (s.subset t).PresupFree = (s.PresupFree ∧ t.PresupFree)
• (s.mem t).PresupFree = (s.PresupFree ∧ t.PresupFree)
• t.sg.PresupFree = t.PresupFree
• t.pl.PresupFree = t.PresupFree
• φ.neg.PresupFree = φ.PresupFree
• (φ.conj ψ).PresupFree = (φ.PresupFree ∧ ψ.PresupFree)
• (PIP.Expr.exists_ x_2 φ).PresupFree = φ.PresupFree
• (PIP.Expr.labelDef X φ).PresupFree = φ.PresupFree
• (PIP.Expr.label X).PresupFree = False
• (e.presup ψ).PresupFree = False

def PIP.Expr.decPresupFree {V : Type u} {L : Type v} {P : ℕ → Type w} {k : Kind} (e : Expr V L P k) : Decidable e.PresupFree

Decidability of Expr.PresupFree.

Equations

• (PIP.Expr.var x_2).decPresupFree = isTrue trivial
• (PIP.Expr.bvar x_2).decPresupFree = isTrue trivial
• (PIP.Expr.abs x_2 φ).decPresupFree = φ.decPresupFree
• (PIP.Expr.sigma x_2 φ).decPresupFree = φ.decPresupFree
• (s.inter t).decPresupFree = instDecidableAnd
• PIP.Expr.empty.decPresupFree = isTrue trivial
• PIP.Expr.top.decPresupFree = isTrue trivial
• (PIP.Expr.atom r w ts).decPresupFree = instDecidableAnd
• (s.eq t).decPresupFree = instDecidableAnd
• (s.subset t).decPresupFree = instDecidableAnd
• (s.mem t).decPresupFree = instDecidableAnd
• t.sg.decPresupFree = t.decPresupFree
• t.pl.decPresupFree = t.decPresupFree
• φ.neg.decPresupFree = φ.decPresupFree
• (φ.conj ψ).decPresupFree = instDecidableAnd
• (PIP.Expr.exists_ x_2 φ).decPresupFree = φ.decPresupFree
• (PIP.Expr.labelDef X φ).decPresupFree = φ.decPresupFree
• (PIP.Expr.label X).decPresupFree = isFalse ⋯
• (e.presup ψ).decPresupFree = isFalse ⋯

@[instance_reducible]

instance PIP.instDecidablePresupFree {V : Type u} {L : Type v} {P : ℕ → Type w} {k : Kind} (e : Expr V L P k) : Decidable e.PresupFree

Equations

• PIP.instDecidablePresupFree e = e.decPresupFree

Labels

def PIP.Expr.substLabels {V : Type u} {L : Type v} {P : ℕ → Type w} (A : L → Option (Formula V L P)) {k : Kind} : Expr V L P k → Expr V L P k

Replace every label use by its definition under the assignment A, leaving undefined labels in place.

Equations

• PIP.Expr.substLabels A (PIP.Expr.var x_2) = PIP.Expr.var x_2
• PIP.Expr.substLabels A (PIP.Expr.bvar x_2) = PIP.Expr.bvar x_2
• PIP.Expr.substLabels A (PIP.Expr.abs x_2 φ) = PIP.Expr.abs x_2 (PIP.Expr.substLabels A φ)
• PIP.Expr.substLabels A (PIP.Expr.sigma x_2 φ) = PIP.Expr.sigma x_2 (PIP.Expr.substLabels A φ)
• PIP.Expr.substLabels A (s.inter t) = (PIP.Expr.substLabels A s).inter (PIP.Expr.substLabels A t)
• PIP.Expr.substLabels A PIP.Expr.empty = PIP.Expr.empty
• PIP.Expr.substLabels A PIP.Expr.top = PIP.Expr.top
• PIP.Expr.substLabels A (PIP.Expr.atom r w ts) = PIP.Expr.atom r (PIP.Expr.substLabels A w) fun (i : Fin n) => PIP.Expr.substLabels A (ts i)
• PIP.Expr.substLabels A (s.eq t) = (PIP.Expr.substLabels A s).eq (PIP.Expr.substLabels A t)
• PIP.Expr.substLabels A (s.subset t) = (PIP.Expr.substLabels A s).subset (PIP.Expr.substLabels A t)
• PIP.Expr.substLabels A (s.mem t) = (PIP.Expr.substLabels A s).mem (PIP.Expr.substLabels A t)
• PIP.Expr.substLabels A t.sg = (PIP.Expr.substLabels A t).sg
• PIP.Expr.substLabels A t.pl = (PIP.Expr.substLabels A t).pl
• PIP.Expr.substLabels A φ.neg = (PIP.Expr.substLabels A φ).neg
• PIP.Expr.substLabels A (φ.conj ψ) = (PIP.Expr.substLabels A φ).conj (PIP.Expr.substLabels A ψ)
• PIP.Expr.substLabels A (PIP.Expr.exists_ x_2 φ) = PIP.Expr.exists_ x_2 (PIP.Expr.substLabels A φ)
• PIP.Expr.substLabels A (PIP.Expr.labelDef X φ) = PIP.Expr.labelDef X (PIP.Expr.substLabels A φ)
• PIP.Expr.substLabels A (PIP.Expr.label X) = (A X).getD (PIP.Expr.label X)
• PIP.Expr.substLabels A (e.presup ψ) = (PIP.Expr.substLabels A e).presup (PIP.Expr.substLabels A ψ)

def PIP.Expr.defs {V : Type u} {L : Type v} {P : ℕ → Type w} {k : Kind} : Expr V L P k → List (L × Formula V L P)

The label definitions occurring in an expression.

Equations

• (PIP.Expr.var x_2).defs = []
• (PIP.Expr.bvar x_2).defs = []
• (PIP.Expr.abs x_2 φ).defs = φ.defs
• (PIP.Expr.sigma x_2 φ).defs = φ.defs
• (s.inter t).defs = s.defs ++ t.defs
• PIP.Expr.empty.defs = []
• PIP.Expr.top.defs = []
• (PIP.Expr.atom r w ts).defs = w.defs ++ List.flatMap (fun (i : Fin n) => (ts i).defs) (List.finRange n)
• (s.eq t).defs = s.defs ++ t.defs
• (s.subset t).defs = s.defs ++ t.defs
• (s.mem t).defs = s.defs ++ t.defs
• t.sg.defs = t.defs
• t.pl.defs = t.defs
• φ.neg.defs = φ.defs
• (φ.conj ψ).defs = φ.defs ++ ψ.defs
• (PIP.Expr.exists_ x_2 φ).defs = φ.defs
• (PIP.Expr.labelDef X φ).defs = (X, φ) :: φ.defs
• (PIP.Expr.label X).defs = []
• (e.presup ψ).defs = e.defs ++ ψ.defs

def PIP.assignment {V : Type u} {L : Type v} {P : ℕ → Type w} [DecidableEq L] : List (L × Formula V L P) → L → Option (Formula V L P)

The label assignment determined by a list of definitions: the first definition of each label.

Equations

• PIP.assignment [] x✝ = none
• PIP.assignment ((Y, ψ) :: A) x✝ = if Y = x✝ then some ψ else PIP.assignment A x✝

def PIP.Formula.expand {V : Type u} {L : Type v} {P : ℕ → Type w} [DecidableEq L] (A : List (L × Formula V L P)) (φ : Formula V L P) : Formula V L P

Expand a formula by a list of label definitions: one round of simultaneous substitution per definition, which resolves every non-circular chain of definitions whatever their order.

Equations

• PIP.Formula.expand A φ = List.foldl (fun (ψ : PIP.Formula V L P) (x : L × PIP.Formula V L P) => PIP.Expr.substLabels (PIP.assignment A) ψ) φ A

def PIP.Formula.expandSelf {V : Type u} {L : Type v} {P : ℕ → Type w} [DecidableEq L] (φ : Formula V L P) : Formula V L P

Expand a formula by its own label definitions.

Equations

• φ.expandSelf = PIP.Formula.expand (PIP.Expr.defs φ) φ

Eliminability

def PIP.Formula.closeList {V : Type u} {L : Type v} {P : ℕ → Type w} (xs : List V) (φ : Formula V L P) : Formula V L P

Existential closure over a list of variables, as syntax.

Equations

• PIP.Formula.closeList xs φ = List.foldr PIP.Expr.exists_ φ xs

def PIP.Expr.elim {V : Type u} {L : Type v} {P : ℕ → Type w} [DecidableEq V] {k : Kind} : Expr V L P k → Expr V L P k

Translation into predicate calculus with set abstraction: brackets and presuppositions are dropped, summation becomes abstraction over the closure of the other local variables, label definitions become ⊤.

Equations

• (PIP.Expr.var x_2).elim = PIP.Expr.var x_2
• (PIP.Expr.bvar x_2).elim = PIP.Expr.var x_2
• (PIP.Expr.abs x_2 φ).elim = PIP.Expr.abs x_2 φ.elim
• (PIP.Expr.sigma x_2 φ).elim = PIP.Expr.abs x_2 (PIP.Formula.closeList (List.filter (fun (x : V) => decide (x ≠ x_2)) φ.locals) φ.elim)
• (s.inter t).elim = s.elim.inter t.elim
• PIP.Expr.empty.elim = PIP.Expr.empty
• PIP.Expr.top.elim = PIP.Expr.top
• (PIP.Expr.atom r w ts).elim = PIP.Expr.atom r w.elim fun (i : Fin n) => (ts i).elim
• (s.eq t).elim = s.elim.eq t.elim
• (s.subset t).elim = s.elim.subset t.elim
• (s.mem t).elim = s.elim.mem t.elim
• t.sg.elim = t.elim.sg
• t.pl.elim = t.elim.pl
• φ.neg.elim = φ.elim.neg
• (φ.conj ψ).elim = φ.elim.conj ψ.elim
• (PIP.Expr.exists_ x_2 φ).elim = PIP.Expr.exists_ x_2 φ.elim
• (PIP.Expr.labelDef X φ).elim = PIP.Expr.top
• (PIP.Expr.label X).elim = PIP.Expr.label X
• (e.presup ψ).elim = e.elim