Predicate Logic with Anaphora: syntax

Syntax for Predicate Logic with Anaphora (PLA), the dynamic system originating in [Dek94] and consolidated in [Dek12]. PLA distinguishes variables x_i, bound by quantifiers, from pronouns p_i, anaphoric expressions resolved from discourse context; the distinction prevents variable clash and keeps composition clean.

Main definitions

• PLA.Term, PLA.Formula: terms (variables or pronouns) and formulas
• PLA.Formula.domain: the variables existentially bound in a formula, n(φ)
• PLA.Formula.range: the pronouns occurring in a formula, r(φ)
• PLA.Resolution, PLA.Formula.resolve: replacing pronouns with variables, φ^ρ

Main results

• PLA.Formula.resolve_preserves_domain: resolution preserves the domain
• PLA.Formula.resolve_no_pronouns: resolution eliminates all pronouns

@[reducible, inline]

abbrev PLA.VarIdx : Type

Variable index: identifies a variable x_i

Equations

• PLA.VarIdx = ℕ

@[reducible, inline]

abbrev PLA.PronIdx : Type

Pronoun index: identifies a pronoun p_i

Equations

• PLA.PronIdx = ℕ

inductive PLA.Term : Type

Term: either a variable or a pronoun

• var : VarIdx → Term
• pron : PronIdx → Term

def PLA.instDecidableEqTerm.decEq (x✝ x✝¹ : Term) : Decidable (x✝ = x✝¹)

Equations

• PLA.instDecidableEqTerm.decEq (PLA.Term.var a) (PLA.Term.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PLA.instDecidableEqTerm.decEq (PLA.Term.var a) (PLA.Term.pron a_1) = isFalse ⋯
• PLA.instDecidableEqTerm.decEq (PLA.Term.pron a) (PLA.Term.var a_1) = isFalse ⋯
• PLA.instDecidableEqTerm.decEq (PLA.Term.pron a) (PLA.Term.pron b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance PLA.instDecidableEqTerm : DecidableEq Term

Equations

• PLA.instDecidableEqTerm = PLA.instDecidableEqTerm.decEq

def PLA.instReprTerm.repr : Term → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PLA.instReprTerm : Repr Term

Equations

• PLA.instReprTerm = { reprPrec := PLA.instReprTerm.repr }

@[instance_reducible]

instance PLA.instHashableTerm : Hashable Term

Equations

• PLA.instHashableTerm = { hash := PLA.instHashableTerm.hash }

def PLA.instHashableTerm.hash : Term → UInt64

Equations

• PLA.instHashableTerm.hash (PLA.Term.var a) = mixHash 0 (hash a)
• PLA.instHashableTerm.hash (PLA.Term.pron a) = mixHash 1 (hash a)

def PLA.Term.pronouns : Term → Finset PronIdx

Pronouns in a term (singleton or empty)

Equations

• (PLA.Term.var a).pronouns = ∅
• (PLA.Term.pron a).pronouns = {a}

def PLA.Term.vars : Term → Finset VarIdx

Variables in a term

Equations

• (PLA.Term.var a).vars = {a}
• (PLA.Term.pron a).vars = ∅

def PLA.termsPronouns (ts : List Term) : Finset PronIdx

Pronouns in a list of terms via Finset.biUnion.

Equations

• PLA.termsPronouns ts = ts.toFinset.biUnion PLA.Term.pronouns

theorem PLA.mem_termsPronouns (ts : List Term) (i : PronIdx) : i ∈ termsPronouns ts ↔ ∃ t ∈ ts, i ∈ t.pronouns

inductive PLA.Formula : Type

PLA Formula

• atom : String → List Term → Formula
• neg : Formula → Formula
• conj : Formula → Formula → Formula
• exists_ : VarIdx → Formula → Formula

@[instance_reducible]

instance PLA.instReprFormula : Repr Formula

Equations

• PLA.instReprFormula = { reprPrec := PLA.instReprFormula.repr }

def PLA.instReprFormula.repr : Formula → ℕ → Std.Format

Equations

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

def PLA.Formula.«term_⋀_» : Lean.TrailingParserDescr

Equations

• PLA.Formula.«term_⋀_» = Lean.ParserDescr.trailingNode `PLA.Formula.«term_⋀_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋀ ") (Lean.ParserDescr.cat `term 35))

def PLA.Formula.«term∼_» : Lean.ParserDescr

Equations

• PLA.Formula.«term∼_» = Lean.ParserDescr.node `PLA.Formula.«term∼_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 40))

def PLA.Formula.disj (φ ψ : Formula) : Formula

Equations

• (φ ⋁ ψ) = (∼(∼φ ⋀ ∼ψ))

def PLA.Formula.«term_⋁_» : Lean.TrailingParserDescr

Equations

• PLA.Formula.«term_⋁_» = Lean.ParserDescr.trailingNode `PLA.Formula.«term_⋁_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋁ ") (Lean.ParserDescr.cat `term 30))

def PLA.Formula.impl (φ ψ : Formula) : Formula

Equations

• φ.impl ψ = (∼(φ ⋀ ∼ψ))

def PLA.Formula.«term_⟶_» : Lean.TrailingParserDescr

Equations

• PLA.Formula.«term_⟶_» = Lean.ParserDescr.trailingNode `PLA.Formula.«term_⟶_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟶ ") (Lean.ParserDescr.cat `term 25))

def PLA.Formula.forall_ (i : VarIdx) (φ : Formula) : Formula

Equations

• PLA.Formula.forall_ i φ = (∼PLA.Formula.exists_ i (∼φ))

def PLA.Formula.domain : Formula → Finset VarIdx

Domain: existentially bound variables

Equations

• (PLA.Formula.atom a a_1).domain = ∅
• (∼a).domain = a.domain
• (a ⋀ a_1).domain = a.domain ∪ a_1.domain
• (PLA.Formula.exists_ a a_1).domain = insert a a_1.domain

def PLA.Formula.range : Formula → Finset PronIdx

Range: pronouns in formula (using biUnion for atoms)

Equations

• (PLA.Formula.atom a a_1).range = PLA.termsPronouns a_1
• (∼a).range = a.range
• (a ⋀ a_1).range = a.range ∪ a_1.range
• (PLA.Formula.exists_ a a_1).range = a_1.range

def PLA.Formula.freeVars : Formula → Finset VarIdx

Free variables in formula

Equations

• (PLA.Formula.atom a a_1).freeVars = a_1.toFinset.biUnion PLA.Term.vars
• (∼a).freeVars = a.freeVars
• (a ⋀ a_1).freeVars = a.freeVars ∪ a_1.freeVars
• (PLA.Formula.exists_ a a_1).freeVars = a_1.freeVars.erase a

theorem PLA.Formula.range_atom (name : String) (ts : List Term) : (atom name ts).range = termsPronouns ts

theorem PLA.Formula.range_neg (φ : Formula) : (∼φ).range = φ.range

theorem PLA.Formula.range_conj (φ ψ : Formula) : (φ ⋀ ψ).range = φ.range ∪ ψ.range

theorem PLA.Formula.range_exists (i : VarIdx) (φ : Formula) : (exists_ i φ).range = φ.range

theorem PLA.Formula.pron_in_atom_range (name : String) (ts : List Term) (t : Term) (i : PronIdx) (ht : t ∈ ts) (hi : i ∈ t.pronouns) : i ∈ (atom name ts).range

If a pronoun appears in a term in the formula's argument list, it's in the range

theorem PLA.Formula.range_conj_left (φ ψ : Formula) : φ.range ⊆ (φ ⋀ ψ).range

Range is monotonic over conjunction

theorem PLA.Formula.range_conj_right (φ ψ : Formula) : ψ.range ⊆ (φ ⋀ ψ).range

@[reducible, inline]

abbrev PLA.Resolution : Type

Resolution: maps pronouns to variables

Equations

• PLA.Resolution = (PLA.PronIdx → PLA.VarIdx)

def PLA.Term.resolve (ρ : Resolution) : Term → Term

Apply resolution to a term

Equations

• PLA.Term.resolve ρ (PLA.Term.var a) = PLA.Term.var a
• PLA.Term.resolve ρ (PLA.Term.pron a) = PLA.Term.var (ρ a)

def PLA.Formula.resolve (ρ : Resolution) : Formula → Formula

Apply resolution to a formula

Equations

• PLA.Formula.resolve ρ (PLA.Formula.atom a a_1) = PLA.Formula.atom a (List.map (PLA.Term.resolve ρ) a_1)
• PLA.Formula.resolve ρ (∼a) = (∼PLA.Formula.resolve ρ a)
• PLA.Formula.resolve ρ (a ⋀ a_1) = (PLA.Formula.resolve ρ a ⋀ PLA.Formula.resolve ρ a_1)
• PLA.Formula.resolve ρ (PLA.Formula.exists_ a a_1) = PLA.Formula.exists_ a (PLA.Formula.resolve ρ a_1)

theorem PLA.Formula.resolve_preserves_domain (φ : Formula) (ρ : Resolution) : (resolve ρ φ).domain = φ.domain

Observation 2 ([Dek12] §2.1): Resolution preserves domain.

n(φ^ρ) = n(φ): resolving pronouns doesn't affect which variables are bound.

theorem PLA.Term.resolve_no_pronouns (t : Term) (ρ : Resolution) : (resolve ρ t).pronouns = ∅

Resolution removes all pronouns from a term

theorem PLA.Formula.resolve_no_pronouns (φ : Formula) (ρ : Resolution) : (resolve ρ φ).range = ∅

Observation 3 ([Dek12] §2.1): Resolution eliminates all pronouns.

r(φ^ρ) = ∅: after resolution, the formula contains no pronouns.