Peters-Kleene deployment

import Linglib.Logic.Trivalent.Deployment · namespace Trivalent

Peters-Kleene deployment applies a classical truth function to three-valued arguments one at a time, from left to right (George 2014 §3). A classical argument fills the next argument position. An undefined argument is repaired to either classical value, and the repair succeeds only if the two values leave the same function of the remaining arguments; otherwise the whole application is undefined. Each argument position is thus treated by the Strong Kleene principle with the earlier arguments fixed and the later ones still open, which is Krahmer's middle Kleene intuition made explicit.

Deploying the classical negation, conjunction, disjunction and material conditional gives exactly the connectives of Peters 1979, the Middle Kleene connectives meetMiddle and joinMiddle. As stipulated truth tables the Peters connectives do not meet the explanatory challenge of Schlenker 2008a, since nothing selects them among the trivalent extensions of the classical connectives. Deriving them by deployment does: the rule is uniform, so a connective's projection behaviour follows from its classical meaning and the order of its arguments.

Main definitions

Trivalent.reduceFirst: the reduction f/x of a truth function by a classical value (Definition 12).
Trivalent.pkReduce: the Peters-Kleene reduction f///X by a set of classical values (Definition 13).
Trivalent.deploy: the Peters-Kleene deployment f[x₁, …, xₙ] (Definition 15).
Trivalent.deploy₁, Trivalent.deploy₂: deployment of unary and binary truth functions.

Main results

Trivalent.deploy_cons_ofProp, Trivalent.deploy_cons_zero: deployment takes its arguments one at a time.
Trivalent.deploy_ofProp: on classical arguments, deployment is application (Remark 8).
Trivalent.deploy_eq_zero_of_reduceFirst_ne: an undefined argument in a position that matters makes the deployment undefined (generalising Remarks 9 and 10).
Trivalent.toFinset_deploy₁: unary deployment is the Strong Kleene lift.
Trivalent.deploy₂_ofProp_left, Trivalent.deploy₂_zero_left: binary deployment is unary deployment after its first argument.
Trivalent.deploy₁_not, Trivalent.deploy₂_and, Trivalent.deploy₂_or, Trivalent.deploy₂_imp, Trivalent.Connectives.middleKleene_eq_deploy: deployment of the classical connectives gives the Peters connectives (Proposition 3, whose cells include Remarks 11 and 12).

Implementation notes

An n-ary truth function is a function on Fin n → Bool, and a 0-ary one is identified with its value. A failed reduction is none rather than George's constant function to the failure value, which deployment then sends to 0. The repair set of a value (Definition 14) is SignType.toFinset. Choosing true or false as the member to reduce by is specific to Bool; repair sets of predicates over an infinite domain (George 2014 §4) will need George's existential formulation of Definition 13.

References

George 2014, Some Remarks on Certain Trivalent Accounts of Presupposition Projection
Peters 1979, A Truth-Conditional Formulation of Karttunen’s Account of Presupposition
Kleene 1952, Introduction to Metamathematics
Schlenker 2008a, Be Articulate: A Pragmatic Theory of Presupposition Projection

Declarations

The reduction f/x of an n + 1-ary truth function by a classical value fills its first argument position.

def reduceFirst L79–82

{n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (x : Bool) :

(Fin n → Bool) → Bool

reduceFirst f x ys = f (Fin.cons x ys)

Used by reduceFirst_apply, reduceFirst_unary, pkReduce, pkReduce_singleton, pkReduce_toFinset_zero, deploy_cons_ofProp, deploy_cons_zero, deploy_eq_zero_of_reduceFirst_ne

L84–85

L87–89

The Peters-Kleene reduction f///X is the reduction of f by any member of X when every member gives the same reduction, and fails otherwise. It reduces by true when X contains it and by false otherwise, which for a nonempty X is a member; Definition 13 requires X nonempty, and on ∅ the reduction is by false.

def pkReduce L91–99

{n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (X : Finset Bool) :

Option ((Fin n → Bool) → Bool)

pkReduce f X = if ∀ x ∈ X, ∀ y ∈ X, reduceFirst f x = reduceFirst f y then some (reduceFirst f (decide (true ∈ X))) else none

Built from

Used by pkReduce_singleton, pkReduce_toFinset_zero, deploy

L101–104

L106–109

The Peters-Kleene deployment f[x₁, …, xₙ] Peters-Kleene reduces f by the repair set of each argument in turn, following George's convention f[x₁, …, xₙ] = f[x₁]…[xₙ], and is undefined once a reduction fails.

def deploy L111–119

{n : ℕ} :

((Fin n → Bool) → Bool) → (Fin n → SignType) → SignType

deploy f x_3 = SignType.ofProp (f ![] = true)
deploy f x_3 = match pkReduce f (x_3 0).toFinset with | some g => deploy g (Fin.tail x_3) | none => 0

Built from

Used by deploy_cons_ofProp, deploy_cons_zero, deploy_ofProp, deploy_eq_zero_of_reduceFirst_ne, deploy₁, deploy₂

A classical first argument fills the first argument position.

theorem deploy_cons_ofProp L121–125

{n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (b : Bool) (x : Fin n → SignType) :

deploy f (Fin.cons (SignType.ofProp (b = true)) x) = deploy (reduceFirst f b) x

Built from ,

An undefined first argument is skipped if its position does not matter, and makes the deployment undefined otherwise.

theorem deploy_cons_zero L127–133

{n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (x : Fin n → SignType) :

deploy f (Fin.cons 0 x) = if reduceFirst f true = reduceFirst f false then deploy (reduceFirst f true) x else 0

Built from ,

On classical arguments, deployment is application (Remark 8).

theorem deploy_ofProp L135–143

{n : ℕ} (f : (Fin n → Bool) → Bool) (b : Fin n → Bool) :

(deploy f fun (i : Fin n) => SignType.ofProp (b i = true)) = SignType.ofProp (f b = true)

Built from

An undefined argument in a position whose value matters makes the deployment undefined, generalising Remarks 9 and 10.

theorem deploy_eq_zero_of_reduceFirst_ne L145–150

{n : ℕ} {f : (Fin (n + 1) → Bool) → Bool} (h : reduceFirst f true ≠ reduceFirst f false) {x : Fin (n + 1) → SignType} (hx : x 0 = 0) :

deploy f x = 0

Built from ,

Unary and binary deployment

The deployment of a unary truth function.

def deploy₁ L154–156

(f : Bool → Bool) (x : SignType) :

SignType

deploy₁ f x = deploy (fun (v : Fin (Nat.succ 0) → Bool) => f (v 0)) ![x]

Built from

Used by toFinset_deploy₁, deploy₂_ofProp_left, deploy₂_zero_left, deploy₁_not

The deployment of a binary truth function, its first argument first.

def deploy₂ L158–160

(f : Bool → Bool → Bool) (x y : SignType) :

SignType

deploy₂ f x y = deploy (fun (v : Fin (Nat.succ 0).succ → Bool) => f (v 0) (v 1)) ![x, y]

Built from

Used by deploy₂_ofProp_left, deploy₂_zero_left, deploy₂_and, deploy₂_or, deploy₂_imp, Connectives.middleKleene_eq_deploy

Unary deployment is the Strong Kleene lift: it leaves open the classical values f takes on the repair set of its argument.

theorem toFinset_deploy₁ L162–166

(f : Bool → Bool) (x : SignType) :

(deploy₁ f x).toFinset = Finset.image f x.toFinset

Built from

After a classical first argument, binary deployment is unary deployment.

theorem deploy₂_ofProp_left L168–171

(f : Bool → Bool → Bool) (b : Bool) (y : SignType) :

deploy₂ f (SignType.ofProp (b = true)) y = deploy₁ (f b) y

Built from ,

After an undefined first argument, binary deployment is unary deployment if the first position does not matter, and undefined otherwise.

theorem deploy₂_zero_left L173–177

(f : Bool → Bool → Bool) (y : SignType) :

deploy₂ f 0 y = if f true = f false then deploy₁ (f true) y else 0

Built from ,

The Peters connectives

Deploying classical negation gives Kleene's negation (Proposition 3).

@[simp] theorem deploy₁_not L181–183

(deploy₁ fun (x : Bool) => !x) = Neg.neg

Built from

Deploying classical conjunction gives Peters' conjunction (Proposition 3).

@[simp] theorem deploy₂_and L185–187

(deploy₂ fun (x1 x2 : Bool) => x1 && x2) = SignType.meetMiddle

Built from

Deploying classical disjunction gives Peters' disjunction (Proposition 3).

@[simp] theorem deploy₂_or L189–191

(deploy₂ fun (x1 x2 : Bool) => x1 || x2) = SignType.joinMiddle

Built from

Deploying the classical material conditional gives Peters' conditional (Proposition 3).

@[simp] theorem deploy₂_imp L193–195

(deploy₂ fun (a b : Bool) => !a || b) = fun (x y : SignType) => (-x).joinMiddle y

Built from

The Middle Kleene connectives are the Peters-Kleene deployments of the classical ones.

theorem Connectives.middleKleene_eq_deploy L197–201

middleKleene = { conj := deploy₂ fun (x1 x2 : Bool) => x1 && x2, disj := deploy₂ fun (x1 x2 : Bool) => x1 || x2, cond := deploy₂ fun (a b : Bool) => !a || b }

Built from