DRAFT

Existential variables and nominal terms in first-order logic proof-search

Claus-Peter Wirth, Murdoch J. Gabbay

Abstract [mjg to do] Keywords: [mjg to do]

Contents

1  Introduction  2
2  Nominal terms  2
2.1 Basic Notions and Notation . . . . . . . . . . . . . . . . . . . . . . . . . 2
2.2 Atoms and Permission Sets . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.3 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.4 Atom Substitutions and Terms . . . . . . . . . . . . . . . . . . . . . . . 3
2.5 Formulas and Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2.6 Variable Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.7 Extending Atom and Variable Substitutions to Terms . . . . . . . . . . 5
2.8 Permutations and α-Equivalence . . . . . . . . . . . . . . . . . . . . . . 6
2.9 Further Elementary Lemmas . . . . . . . . . . . . . . . . . . . . . . . . 7
3 Semantics 10
3.1 Pre-Structures, Evaluation, and Structures . . . . . . . . . . . . . . . . 10
3.2 Interface Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
3.3 Choice-Conditions, Compatibility, and C-Validity . . . . . . . . . . . . 14
3.4 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
4 Proof-search 17
4.1 γ-Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
4.2 δ^{−}-Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
4.3 δ^{ε}-Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
4.4 δ^{+}-Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5  Background on nominal sets  24
6  Nominal models for simple type theory  25
6.1 Nominal λ-model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

Preprint submitted to Elsevier January 18, 2012

DRAFT

7  [mjg] stuff  27
7.1 Soundness for β-conversion . . . . . . . . . . . . . . . . . . . . . . . . . 28
8  [mjg stuff]  28

1. Introduction

2. Nominal terms

2.1. Basic Notions and Notation

‘N’ denotes the set of natural numbers and ‘≺’ the ordering on N. Let N_{+} := { n ∈ N | 0 ≠ n }. ‘Z’ denotes the set of integers: Z := {0, −1, 1, −2, 2, …}. We use ‘⊎’ for the union of disjoint classes and ‘id’ for the identity function. For classes R, A, and B we define:

dom(R) := {a | ∃b. (a, b) ∈ R}  domain
A↿R := {(a, b) ∈ R | a ∈ A}  (domain-) restriction toA
⟨A⟩R := {b | ∃a ∈ A. (a, b) ∈ R} image ofA, i.e. ⟨A⟩R = ran(_{A}↿R)

And the dual ones:

ran(R) := {b | ∃a. (a, b) ∈ R}  range
R↾_{B} := {(a, b) ∈ R | b ∈ B }  range-restriction to B
R⟨B⟩ := {a | ∃b ∈ B. (a, b) ∈ R} reverse-image ofB, i.e. R⟨B⟩ = dom(R↾_{B})

Furthermore, we use ‘∅’ to denote the empty set as well as the empty function. Functions are (right-) unique relations and the meaning of ‘f∘g’ is extensionally given by (f∘g)(x) = g(f(x)). The class of total functions from A to B is denoted as A → B. The class of (possibly) partial functions from A to B is denoted as A ⇝ B. Both → and ⇝ associate to the right, i.e. A ⇝ B → C reads A ⇝ (B → C).

Let R be a binary relation. R is said to be a relation on A if dom(R) ∪ ran(R) ⊆ A. R isirreflexive if id ∩ R = ∅. It is A-reflexive if _{A}↿id ⊆ R. Speaking of a reflexive relation we refer to the largest A that is appropriate in the local context, and referring to this A we write R^{0} to ambiguously denote _{A}↿id. With R^{1} := R, and R^{n+1} := R^{n}∘R for n ∈ N_{+}, R^{m} denotes the m-step relation for R. The transitive closure of R is R^{+} := ⋃_{n∈N_{+}} R^{n}. The reflexive & transitive closure of R is R^{∗} := ⋃_{n∈N} R^{n}. A relation R (on A) is well-foundedif any non-empty class B (⊆A) has an R-minimal element, i.e. ∃a ∈ B. ¬∃a′ ∈ B. a′R a.

Definition 2.1 (Partial Generalized Choice Function). f is a partial generalized choice function on A if f is a function with f : A ⇝ ⋃ A and ∀x ∈ dom(f). ((x = ∅) ∨ (f(x) ∈ x)).

DRAFT

2.2. Atoms and Permission Sets 2.3. Types Definition 2.2. Fix a set of base types τ.

Let types α be inductively defined as follows:

α ::= o | τ | α → α

2.4. Atom Substitutions and Terms Definition 2.3. For each type α, let us fix a disjoint countably infinite set of atoms 𝔸_{α}, and an arbitrary bijection f_{α} between Z and 𝔸_{α}. Write

𝔸α^{<} = {f_{α}(i) | i < 0} 𝔸α^{>} = {f_{α}(i) | i ≥ 0}.

Finally, write

𝔸^{<} = ⋃_{α} 𝔸α^{<}  𝔸^{>} = ⋃_{α} 𝔸α^{>}  𝔸 = ⋃_{α} 𝔸_{α}

a, b, c, … will range over distinct atoms (we call this the permutative convention).

A permission set has the form (𝔸^{<} ∪ A) \ B where A ⊆ 𝔸^{>} and B ⊆ 𝔸^{<} are finite (and a permission set may be finitely represented by the pair (A, B)). S, T, and U will range over permissions sets.

The use of 𝔸^{<} and 𝔸^{>} ensures that permission sets are infinite and also co-infinite (i.e. their complement is also infinite).

Definition 2.4. For each permission set S and type α fix a disjoint countably infinite set of (level 2) variables 𝕍_{α,S}. Set 𝕍 := ⋃_{α,S} 𝕍_{α,S}. X, Y, Z will range over distinct variables. We write pmss(X) for the permission set of X and type(X) for the type of X.

Definition 2.5. Fix a set of constants, to each of which is associated a type. f, g, h will range over distinct constants; we write type(f) for the type of f.

We assume the following distinguished constants:

⊥, ⊤ : o  ¬ : o → o  ∧, ⇒ : o → o → o  ∀_{α}, ∃_{α} : (α → o) → o

DRAFT

Definition 2.6 (Terms T , Types, Atom Substitutions). Let atom substitutions (or level 1 substitutions) and typed terms be inductively defined as follows:

An atom substitution is a total function from 𝔸 to terms of the same type, which maps a to a for all but finitely many atoms.

Define typed terms, such that r : α reads “term r has type α”, as follows:

{type(f) = α \atop f : α}  {type(a) = α \atop a : α}

{r_{1} : α_{2} → α_{1} r_{2} : α_{2} \atop r_{1}r_{2} : α_{1}}  {a : α r : β \atop [a]r : α → β}

type(X) = α, σ is an atom substitution

σ·X : α

r is a term if r : α for some α. Let T denote the set of all terms.

Notation 2.7. We write [a_{1}↦t_{1}, …, a_{n}↦t_{n}] for the substitution σ on variables given by σ := { ⟨ a_{i} , t_{i} ⟩ | i ∈ {1, …, n} } ∪_{𝔸\{a_{1},...,a_{n}}}↿id.

Notation 2.8. r_{1}r_{2} associates to the left, so that r_{1}r_{2}r_{3} reads (r_{1}r_{2})r_{3}.

[mjg give example terms]

σ will range over atom substitutions.

2.5. Formulas and Sequents Definition 2.9 (Formulas, Sequents). r is a formula if r : o. A sequent is a list of formulas (with disjunctive interpretation).

Definition 2.10 (fa,fv). Let T range over sets of terms. Define the operators fa (“free atoms of”), and fv (“free variables of”) by:

fa(f) = ∅  fv(f) = ∅
fa(r_{1}r_{2}) = ⋃_{i∈{1,2}} ; fa(r_{i})  fv(r_{1}r_{2}) = ⋃_{i∈{1,2}} ; fv(r_{i})
fa(a) = {a}  fv(a) = ∅
fa([b]r) = fa(r) \ {b}  fv([b]r) = fv(r)
fa(σ·X) = ⋃_{a∈pmss(X)} ; fa(σ(a))  fv(σ·X) = {X} ∪ ⋃_{a∈pmss(X)} fv(σ(a))
fa(T) = ⋃_{t∈T} fa(t)  fv(T) = ⋃_{t∈T} fv(t)

Be aware that Z ∈ fv(r) does not mean that Z (or _{𝔸}↿id·Z) is a subterm of r. [mjg cp: I don’t understand this comment or the example] For example, Z ∈ fv(r) does not imply fa(_{𝔸}↿id·Z) ⊆ fa(r); to wit take r = [a↦b]·Z with a ∈ pmss(Z); then a ∈ fa(_{𝔸}↿id·Z), but a ∉ fa(r).

DRAFT

2.6. Variable Substitutions Definition 2.11. A variable substitution (or level 2 substitution) is a function θ from variablesto terms which maps X to _{𝔸}↿id·X for all but finitely many variables, and is such that fa(θ(X)) ⊆ fa(_{𝔸}↿id·X) for all X (note that fa(_{𝔸}↿id·X) = pmss(X)).

θ will range over variable substitutions.

2.7. Extending Atom and Variable Substitutions to Terms Definition 2.12. Define nontriv(σ) and fa(σ) and nontriv(θ) by

nontriv(σ) = {a | σ(a) ≠ a}  nontriv(θ) = { X | θ(X) ≠ _{𝔸}↿id·X }
fa(σ)

=

⋃ a∈nontriv(σ)

({a} ∪ fa(σ(a)))

Remark 2.13. Note that a term σ·X, i.e. a variable X with a delayed atom substitution σ, does not have to satisfy nontriv(σ) ⊆ pmss(X), but we could require this because we are not interested in σ·X beside (_{pmss(X)}↿σ)·X. Note that these possibly different terms will be α-equivalent according to Definition 2.17.

Definition 2.14. We extend any atom substitution σ and any variable substitution θ to functions σ^{T} and θ^{T} from terms to terms as given in the following box. Note that we write rσ as a shorthand for σ^{T}(r), and also rθ as a shorthand for θ^{T}(r).

fσ = f  fθ = f
(r_{1}r_{2})σ = (r_{1}σ)(r_{2}σ)  (r_{1}r_{2})θ = (r_{1}θ)(r_{2}θ)
aσ = σ(a)  aθ = a
([b]r)σ = [b](rσ) with proviso b ∉ fa(σ)  ([b]r)θ = [b](rθ)
(σ′·X)σ = (σ′ ∘ σ^{T})·X  (σ′·X)θ = (θ(X))(σ′ ∘ θ^{T})

[mjg cp: why is substitution written postfix in the boxed fiture, but prefix on a moderated variable?] Note that in the right-hand side of the last equation of the left column of the above box, (σ′ ∘ σ^{T}) is the atom substitution that maps a to (σ′(a))σ. Similarly, in the right column, (σ′ ∘ θ^{T}) is the atom substitution that maps a to (σ′(a))θ. The reason why we had better not be sloppy and simply write σ instead of σ^{T} is that, for instance in the last example, we must make clear that (θ(X))(σ ∘ θ^{T}) is (σ ∘ θ^{T})^{T} (θ(X)) and not the in general different (σ^{T} ∘ θ^{T})(θ(X)); to see the difference, take σ := _{𝔸}↿id, then σ^{T} ∘ θ^{T} = _{T} ↿id ∘ θ^{T} = θ^{T}, but (σ ∘ θ^{T})^{T} = (_{𝔸}↿id)^{T} = _{T} ↿id. For more convincing examples of the need for notational explicitness here, see the proof of Lemma 2.23.

DRAFT

2.8. Permutations and α-Equivalence

To overcome the partiality of σ^{T} with b ∈ fa(σ) on [b]r according to Definition 2.14, and to identify the terms with different structure but identical meaning discussed in Remark 2.13, we will quotient terms according to the equivalence of Definition 2.17.

[mjg cp: perhaps better to quotient first and then define substitution action? By appealing to nominal abstract syntax, this can be done completely rigorously.]

Definition 2.15. A permutation π is an atom substitution that is a bijection on 𝔸. Write ℙ for the set of permutations.

Notation 2.16. We use the following notation:

• Given a, b ∈ 𝔸_{α}, let a swapping (a b) be the atom substitution [a↦b, b↦a], i.e. the permutation that maps a to b, b to a, and all other c to themselves.

• Write_{𝔸}↿id for the identity permutation, so_{𝔸}↿id(a) = a always.

• Write π^{-1} for inverse, so π ∘ π^{-1} = _{𝔸}↿id.

Definition 2.17. Call a relation R on terms a congruence when it is an equivalence relation and:

• If r R r′ and s R s′ then rs R r′s′.

• If r R r′ and [a]r R [a]r′.

• σ(a) R σ′(a) for every a ∈ pmss(X) implies σ·X R σ′·X.

Then α-equivalence r = s is the least congruence such that a, b ∉ fa(r) implies r(a b) = r. Henceforth, we quotient terms by α-equivalence.

Lemma 2.18. • [a]r = [b]s if and only if b ∉ fa(r) and r(b a) = s. [mjg cp: I would be in

favour of writing this r · (b a), not r(b a).]

• [a]r = [b]s if and only if r(c a) = s(c a) for fresh c (so c ∉ fa(r)∪fa(s)).

Proof. By elementary calculations.

DRAFT

2.9. Further Elementary Lemmas Lemma 2.19. For a term r and an atom substitution σ we have:

1. fa(rσ) = fa(⟨fa(r)⟩σ).

2. fv(rσ) = fv(r) ∪ fv(⟨fa(r)⟩σ).

2.9.1. Proof of Lemma 2.19

By structural induction on r. \underline{r = a:} fa(aσ) = fa(\{aσ\}) = fa(⟨\{a\}⟩σ) = fa(⟨fa(a)⟩σ).

fv(aσ) = fv({aσ}) = ∅ ∪ fv(⟨{a}⟩σ) = fv(a) ∪ fv(⟨fa(a)⟩σ). \underline{r = σ′·X:} fa((σ′·X)σ) = fa((σ′ ∘ σ^{T})·X) = ⋃_{a∈pmss(X)} fa((σ′ ∘ σ^{T})(a))

= ⋃_{a∈pmss(X)} fa((σ′(a))σ) = ⋃_{a∈pmss(X)} fa(⟨fa(σ′(a))⟩σ)

= fa(⋃_{a∈pmss(X)} ⟨fa(σ′(a))⟩σ) = fa(⟨⋃_{a∈pmss(X)} fa(σ′(a))⟩σ) = fa(⟨fa(σ′·X)⟩σ). fv((σ′·X)σ) = fv((σ′ ∘ σ^{T})·X) = {X} ∪ ⋃_{a∈pmss(X)} fv((σ′ ∘ σ^{T})(a)) = {X} ∪ ⋃_{a∈pmss(X)} fv((σ′(a))σ) = {X} ∪ ⋃_{a∈pmss(X)} (fv(σ′(a)) ∪ fv(⟨fa(σ′(a))⟩σ)) = {X} ∪ ⋃_{a∈pmss(X)} fv(σ′(a)) ∪ ⋃_{a∈pmss(X)} fv(⟨fa(σ′(a))⟩σ) = fv(σ′·X) ∪ fv(⟨⋃_{a∈pmss(X)} fa(σ′(a))⟩σ) = fv(σ′·X) ∪ fv(⟨fa(σ′·X)⟩σ). \underline{r = f:} fa(fσ) = fa(f) = ∅ = fa(∅) = fa(⟨∅⟩σ) = fa(⟨fa(f)⟩σ).

fv(fσ) = fv(f) = fv(f) ∪ ∅ = fv(f) ∪ fv(⟨∅⟩σ) = fv(f) ∪ fv(⟨fa(f)⟩σ). \underline{r = r′_{1}r′_{2}:} fa((r′_{1}r′_{2})σ) = fa((r′_{1}σ)(r′_{2}σ)) = fa(r′_{1}σ)∪fa(r′_{2}σ) = fa(⟨fa(r′_{1})⟩σ)∪fa(⟨fa(r′_{2})⟩σ)

= fa(⟨fa(r′_{1})⟩σ ∪ ⟨fa(r′_{2})⟩σ) = fa(⟨fa(r′_{1}) ∪ fa(r′_{2})⟩σ) = fa(⟨fa(r′_{1}r′_{2})⟩σ).

fv((r′_{1}r′_{2})σ) = fv((r′_{1}σ)(r′_{2}σ)) = ⋃_{i∈{1,2}} fv(r′_{i}σ) = ⋃_{i∈{1,2}} (fv(r′_{i}) ∪ fv(⟨fa(r′_{i})⟩σ)) = ⋃_{i∈{1,2}} fv(r′_{i}) ∪ ⋃_{i∈{1,2}} fv(⟨fa(r′_{i})⟩σ) = fv(r′_{1}r′_{2}) ∪ fv(⟨⋃_{i∈{1,2}} fa(r′_{i})⟩σ) = fv(r′_{1}r′_{2}) ∪ fv(⟨fa(r′_{1}r′_{2})⟩σ). \underline{r = [b]r′, w.l.o.g. b ∉ fa(σ):} fa(([b]r′)σ) = fa([b](r′σ)) = fa(r′σ) \ \{b\}

= fa(⟨fa(r′)⟩σ) \ {b} = fa(⟨fa(r′) \ {b}⟩σ) = fa(⟨fa([b]r′)⟩σ).

fv(([b]r′)σ) = fv([b](r′σ)) = fv(r′σ) = fv(r′) ∪ fv(⟨fa(r′)⟩σ) = fv(r′) ∪ fv(⟨fa(r′) \ {b}⟩σ) = fv([b]r′) ∪ fv(⟨fa([b]r′)⟩σ). \underline{\underline{Q.e.d. (Lemma 2.19)}}

Lemma 2.20. For a term r and a variable substitution θ we have:

1. fa(rθ) ⊆ fa(r).

2. fv(rθ) ⊆ fv(⟨fv(r)⟩θ).

2.9.2. Proof of Lemma 2.20

By structural induction on r. \underline{r = a:} fa(aθ) = fa(a).

fv(aθ) = fv(a) = ∅ = fa(∅) = fa(⟨∅⟩θ) = fv(⟨fv(a)⟩θ). \underline{r = σ·X:} According to Lemma 2.19(in the second steps), because of fa(θ(X)) ⊆ pmss(X)

(in the third steps), and by induction hypothesis (in the sixth steps), we have:

fa((σ·X)θ) = fa((θ(X))(σ ∘ θ^{T})) = fa(⟨fa(θ(X))⟩(σ ∘ θ^{T})) ⊆ fa(⟨pmss(X)⟩(σ ∘ θ^{T})) = ⋃_{a∈pmss(X)} fa((σ ∘ θ^{T})(a)) = ⋃_{a∈pmss(X)} fa((σ(a))θ) ⊆ ⋃_{a∈pmss(X)} fa(σ(a)) = ⋃_{a∈pmss(X)} fa(σ(a)) = fa(σ·X). fv((σ·X)θ) = fv((θ(X))(σ ∘ θ^{T})) = fv(θ(X)) ∪ fv(⟨fa(θ(X))⟩(σ ∘ θ^{T})) ⊆ fv(θ(X)) ∪ fv(⟨pmss(X)⟩(σ ∘ θ^{T})) = fv({θ(X)}) ∪ ⋃_{a∈pmss(X)} fv((σ ∘ θ^{T})(a))

DRAFT

= fv(⟨{X}⟩θ) ∪ ⋃_{a∈pmss(X)} fv((σ(a))θ) ⊆ fv(⟨{X}⟩θ) ∪ ⋃_{a∈pmss(X)} fv(⟨fv(σ(a))⟩θ) = fv(⟨{X} ∪ ⋃_{a∈pmss(X)} fv(σ(a))⟩θ) = fv(⟨fv(σ·X)⟩θ). \underline{r = f:} fa(fθ) = fa(f).

fv(fθ) = fv(f) = ∅ = fv(∅) = fv(⟨∅⟩θ) = fv(⟨fv(f)⟩θ). \underline{r = r′_{1}r′_{2}:} fa((r′_{1}r′_{2})θ) = fa((r′_{1}θ)(r′_{2}θ)) = ⋃_{i∈\{1,2\}} fa(r′_{i}θ) ⊆ ⋃_{i∈\{1,2\}} fa(r′_{i}) = fa(r′_{1}r′_{2}).

fv((r′_{1}r′_{2})θ) = fv((r′_{1}θ)(r′_{2}θ)) = ⋃_{i∈{1,2}} fv(r′_{i}θ) ⊆ ⋃_{i∈{1,2}} fv(⟨fv(r′_{i})⟩θ)

= fv(⟨⋃_{i∈{1,2}} fv(r′_{i})⟩θ) = fv(⟨fv(r′_{1}r′_{2})⟩θ). \underline{r = [b]r′, w.l.o.g. b ∉ fa(σ):} fa(([b]r′)θ) = fa([b](r′θ)) = fa(r′θ) \ \{b\} ⊆ fa(r′) \ \{b\}

= fa([b]r′).

fv(([b]r′)θ) = fv([b](r′θ)) = fv(r′θ) ⊆ fv(⟨fv(r′)⟩θ) = fv(⟨fv([b]r′)⟩θ).

Q.e.d. (Lemma 2.20)

Lemma 2.21. If a ∈ fa(t[a↦t′]), then a ∈ fa(t′).

2.9.3. Proof of Lemma 2.21

If a ∈ fa(t[a↦t′]), then, by Lemma 2.19, a ∈ fa(⟨fa(t)⟩[a↦t′]) ⊆ (fa(t)\{a}) ∪ fa(t′), thus a ∈ fa(t′). \underline{\underline{Q.e.d. (Lemma 2.21)}}

Lemma 2.22. σ^{′T} ∘ σ^{T} = (σ′ ∘ σ^{T})^{T}.

2.9.4. Proof of Lemma 2.22

It suffices to show (rσ′)σ = r(σ′ ∘ σ^{T}) by structural induction on r. \underline{r = a:} (aσ′)σ = (σ′(a))σ = (σ′ ∘ σ^{T})(a) = a(σ′ ∘ σ^{T}). \underline{r = σ′′·X:} By induction hypothesis we have ((σ′′(a))σ′)σ = (σ′′(a))(σ′ ∘ σ^{T}) for all

a ∈ nontriv(σ′′). And for a ∈ 𝔸\nontriv(σ′′), this holds as well because of

((σ′′(a))σ′)σ = (aσ′)σ = (σ′(a))σ = (σ′ ∘ σ^{T})(a) = a(σ′ ∘ σ^{T}) = (σ′′(a))(σ′ ∘ σ^{T}). This means that, for all a ∈ 𝔸, we have (σ′′ ∘ σ^{′T} ∘ σ^{T})(a) = (σ′′ ∘ (σ′ ∘ σ^{T})^{T})(a).

Thus, we have ((σ′′·X)σ′)σ = ((σ′′ ∘ σ^{′T})·X)σ = (σ′′ ∘ σ^{′T} ∘ σ^{T})·X = (σ′′ ∘ (σ′ ∘ σ^{T})^{T})·X = (σ′′·X)(σ′ ∘ σ^{T}). \underline{r = f:} (fσ′)σ = fσ = f = f(σ′ ∘ σ^{T}). \underline{r = r′_{1}r′_{2}:} ((r_{1}r_{2})σ′)σ = ((r_{1}σ′)(r_{2}σ′))σ = ((r_{1}σ′)σ)((r_{2}σ′)σ)

= (r_{1}(σ′ ∘ σ^{T}))(r_{2}(σ′ ∘ σ^{T})) = (r_{1}r_{2})(σ′ ∘ σ^{T}).

\underline{r = [b]r′, w.l.o.g. b ∉ fa(σ) ∪ fa(σ′) ∪ fa(σ′ ∘ σ^{T}):} (([b]r′)σ′)σ = ([b](r′σ′))σ

= [b]((r′σ′)σ) = [b](r′(σ′ ∘ σ^{T}))

= ([b]r′)(σ′ ∘ σ^{T}). \underline{\underline{Q.e.d. (Lemma 2.22)}}

DRAFT

Lemma 2.23. (rσ)θ = (rθ)(σ ∘ θ^{T}).

2.9.5. Proof of Lemma 2.23

By structural induction on r. \underline{r = a:} (aσ)θ = (σ(a))θ = (σ ∘ θ^{T})(a) = a(σ ∘ θ^{T}) = (aθ)(σ ∘ θ^{T}). \underline{r = σ′·X:} By induction hypothesis we have ((σ′(a))σ)θ = ((σ′(a))θ)(σ ∘ θ^{T}) for all

a ∈ nontriv(σ′). And for a ∈ 𝔸\nontriv(σ′) this holds as well because

of ((σ′(a))σ)θ = (aσ)θ = (σ(a))θ = (σ ∘ θ^{T})(a) = a(σ ∘ θ^{T}) = (aθ)(σ ∘ θ^{T}) = ((σ′(a))θ)(σ ∘ θ^{T}).

This means that, for all a ∈ 𝔸, we have (σ′ ∘ σ^{T} ∘ θ^{T})(a) = ((σ′(a))σ)θ = ((σ′(a))θ)(σ ∘ θ^{T}) = (σ′ ∘ θ^{T} ∘ (σ ∘ θ^{T})^{T})(a); i.e. σ′ ∘ σ^{T} ∘ θ^{T} = σ′ ∘ θ^{T} ∘ (σ ∘ θ^{T})^{T}; i.e.

(σ′ ∘ σ^{T} ∘ θ^{T})^{T} = ( σ′ ∘ θ^{T} ∘ (σ ∘ θ^{T})^{T} )^{T} = (σ′ ∘ θ^{T})^{T} ∘ (σ ∘ θ^{T})^{T} by Lemma 2.22.

Thus, we have ((σ′·X)σ)θ = ((σ′ ∘ σ^{T})·X)θ = (θ(X))(σ′ ∘ σ^{T} ∘ θ^{T}) = (σ′ ∘ σ^{T} ∘ θ^{T})^{T} (θ(X)) = ((σ′ ∘ θ^{T})^{T} ∘ (σ ∘ θ^{T})^{T})(θ(X)) = ((θ(X))(σ′ ∘ θ^{T}))(σ ∘ θ^{T}) = ((σ′·X)θ)(σ ∘ θ^{T}). \underline{r = f:} (fσ)θ = fθ = f = f(σ ∘ θ^{T}) = (fθ)(σ ∘ θ^{T}). \underline{r = r′_{1}r′_{2}:} ((r_{1}r_{2})σ)θ = ((r_{1}σ)(r_{2}σ))θ = ((r_{1}σ)θ)((r_{2}σ)θ)

= ((r_{1}θ)(σ ∘ θ^{T}))((r_{2}θ)(σ ∘ θ^{T})) = ((r_{1}θ)(r_{2}θ))(σ ∘ θ^{T}) = ((r_{1}r_{2})θ)(σ ∘ θ^{T}).

\underline{r = [b]r′, w.l.o.g. b ∉ fa(σ) ∪ fa(σ ∘ θ^{T}):} (([b]r′)σ)θ = ([b](r′σ))θ = [b]((r′σ)θ)

= [b]((r′θ)(σ ∘ θ^{T})) = ([b](r′θ))(σ ∘ θ^{T})

= (([b]r′)θ)(σ ∘ θ^{T}). \underline{\underline{Q.e.d. (Lemma 2.23)}}

Lemma 2.24. (rπ)θ = (rθ)π.

2.9.6. Proof of Lemma 2.24

According to Lemma 2.23, we have (rπ)θ = (rθ)(π ∘ θ^{T}) = (rθ)π.

Q.e.d. (Lemma 2.24)

Lemma 2.25. If σ(a) = σ′(a) for all a ∈ fa(r), then rσ = rσ′.

DRAFT

3. Semantics

3.1. Pre-Structures, Evaluation, and Structures

Let S range over pre-structures of the fixed signature given by the set of constants and their types. So S provides some non-empty set as the universe (or “carrier”) (for each type).

More precisely, we assume that every pre-structure S is not only defined on the constants, but is defined also on the symbol U (for universe) such that, for each type α, the universe for the type α is denoted by S(U)_{α} and we have

S(U)_{α} ≠ ∅,
S(U)_{o} = {TRUE, FALSE},
S(U)_{α→β} ⊆ S(U)_{α} → S(U)_{β},

and, for every f : α,

S(f) ∈ S(U)_{α}.

Moreover, every pre-structure is required to be defined also on the symbol C (for choice) such that, for each type α, S(C)_{α} is a partial generalized choice function for the power set of S(U)_{α}. Note that this does not put special restrictions on the existence of prestructures, because we can always take S(C)_{α} as the empty function.

For A ⊆ 𝔸, we denote the set of total S-valuations of A (i.e. functions mapping atoms to objects of the universe of S (respecting types)) with

A → S,

and the set of (possibly) partial S-valuations of A with

A ⇝ S.

Definition 3.1 (S-Semantical Valuation). Let S be a pre-structure. ζ is an S-semantical valuation if

ζ : 𝕍 → (𝔸 ⇝ S) ⇝ S

and, for all X ∈ 𝕍:

ζ(X) : (pmss(X) → S) → S,

such that the type α of X is respected by the value of ζ(X)(τ) in the sense that, for all τ : pmss(X) → S, we have ζ(X)(τ) ∈ S(U)_{α}.

We need the technical means to turn an S-semantical valuation ζ together with an S-valuation τ of the atoms into an S-valuation ϵ(ζ)(τ) of the variables:

Definition 3.2 (ϵ). We define the function

ϵ : (𝕍 → (𝔸 ⇝ S) ⇝ S) → (𝔸 → S) → 𝕍 ⇝ S

for

ζ : 𝕍 → (𝔸 ⇝ S) ⇝ S, τ : 𝔸 → S, X ∈ 𝕍

by

ϵ(ζ)(τ)(X) := ζ(X)(_{pmss(X)}↿τ).

DRAFT

Definition 3.3 (eval). Let S range over pre-structures. Let ζ range over S-semantical valuations. Let τ : 𝔸 → S. Let T range over the truth values TRUE and FALSE. Let f range over elements of S(U)_{α} → S(U)_{β}. Let A_{i} range over formulas. Let G range over sets of sequents. eval(S)(ζ)(τ)(a) = τ(a). eval(S)(ζ)(τ)(σ·X) = ϵ(ζ)(σ ∘ eval(S)(ζ)(τ))(X). eval(S)(ζ)(τ)(f) = S(f). eval(S)(ζ)(τ)(r_{1}r_{2}) = eval(S)(ζ)(τ)(r_{1})(eval(S)(ζ)(τ)(r_{2})). eval(S)(ζ)(τ)([a_{α}]r) is the function that maps every element s ∈ S(U)_{α} to

eval(S)(ζ)(_{𝔸\{a}}↿τ ⊎ {a↦s})(r).

eval(S)(ζ)(τ)(A_{1}, …, A_{n}) =

\{ \begin{matrix}TRUE & if there is an i ∈ \{1, …, n\} such that eval(S)(ζ)(τ)(A_{i}) = TRUE \\ FALSE & otherwise \end{matrix} \} .

eval(S)(ζ)(τ)(G) =

\{ \begin{matrix}FALSE & if there is an Γ ∈ G such that eval(S)(ζ)(τ)(Γ) = FALSE \\ TRUE & otherwise \end{matrix} \} .

eval(S)(ζ)(τ)(⊥) = FALSE. eval(S)(ζ)(τ)(¬)(TRUE) = FALSE. eval(S)(ζ)(τ)(¬)(FALSE) = TRUE. eval(S)(ζ)(τ)(∧)(TRUE)(T) = T. eval(S)(ζ)(τ)(∧)(FALSE)(T) = FALSE. eval(S)(ζ)(τ)(⇒)(TRUE)(T) = T. eval(S)(ζ)(τ)(⇒)(FALSE)(T) = TRUE.

eval(S)(ζ)(τ)(∀_{α})(f) = \{ \begin{matrix}FALSE & if there is an s ∈ S(U)_{α} such that f(s) = FALSE \\ TRUE & otherwise \end{matrix} \}.

eval(S)(ζ)(τ)(∃_{α})(f) = \{ \begin{matrix}TRUE & if there is an s ∈ S(U)_{α} such that f(s) = TRUE \\ FALSE & otherwise \end{matrix} \}.

As abstraction may result in functions that are not contained in the pre-structure S, we need the following definition:

Definition 3.4 (Structure). A pre-structure S is a structure if for each S-semantical valuation ζ, for each τ : 𝔸 → S, and for each term t : α, we have eval(S)(ζ)(τ)(t) ∈ S(U)_{α}. From now on, let S range over structures only.

DRAFT

3.2. Interface Lemmas

The following “lemmas” are the minimal preconditions for the correctness of our inference rules of Section 4. This is the reason why they typically state a proposition that is more restrictive than its valid straightforward generalization. Moreover, they use to occur in logic textbooks.

Corollary 3.5 (Explicitness Lemma). The value of the evaluation of a term t : α, depends only on the valuation of those variables and atoms that actually have free occurrences in t; i.e., if _{fa(t)}↿τ = _{fa(t)}↿τ′ and _{fv(t)}↿ζ = _{fv(t)}↿ζ′, then:

eval(S)(ζ)(τ)(t) = eval(S)(ζ′)(τ′)(t).

Corollary 3.6 (Valuation Lemma). The evaluation function treats application terms consisting of symbols from 𝔸 and 𝕍 straightforwardly in the sense that for every terms t_{0} : α_{0}, …, t_{l−1} : α_{l−1}, t′ : α_{0} → ⋯ → α_{l−1} → α_{l} for some types α_{0}, …, α_{l−1}, α_{l}, and where each of t_{0}, …, t_{l−1}, t′ is either a variable or an atom, we have:

eval(S)(ζ)(τ)(t′ t_{0} ⋯ t_{l−1}) = eval(S)(ζ)(τ)(t′)(eval(S)(ζ)(τ)(t_{0})) ⋯ (eval(S)(ζ)(τ)(t_{l−1})).

Of special relevance are the following cases for l = 0:

eval(S)(ζ)(τ)(a) = τ(a).

Lemma 3.7 (Substitution [Value] Lemma). Let σ be a variable substitution. For every term t : α, we have:

eval(S)(ζ)(τ)(tσ) = eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(t).

3.2.1. Proof of Lemma 3.7 By structural induction on t. \underline{\underline{t = a:}}

eval(S)(ζ)(τ)(aσ) = eval(S)(ζ)(τ)(σ(a))
= (σ ∘ eval(S)(ζ)(τ))(a)
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(a)

\underline{\underline{t = σ′·X:}} By induction hypothesis we have for a ∈ nontriv(σ′):

eval(S)(ζ)(τ)((σ′(a))σ) = eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(σ′(a)).

But this holds for a ∈ 𝔸\nontriv(σ′) as well:

eval(S)(ζ)(τ)((σ′(a))σ) = eval(S)(ζ)(τ)(aσ)
= eval(S)(ζ)(τ)(σ(a))
= (σ ∘ eval(S)(ζ)(τ))(a)
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(a)
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(σ′(a)).

This means that σ′ ∘ σ^{T} ∘ eval(S)(ζ)(τ) = σ′ ∘ eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ)). Thus, we have

eval(S)(ζ)(τ)((σ′·X)σ) = eval(S)(ζ)(τ)((σ′ ∘ σ^{T})·X)
= ϵ(ζ)(σ′ ∘ σ^{T} ∘ eval(S)(ζ)(τ))(X)
= ϵ(ζ)(σ′ ∘ eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ)))(X)
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(σ′·X)

DRAFT

\underline{\underline{t = f:}}

eval(S)(ζ)(τ)(fσ) = eval(S)(ζ)(τ)(f)
= S(f)
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(f)

\underline{\underline{t = r_{1}r_{2}:}} eval(S)(ζ)(τ)((r_{1}r_{2})σ)

= eval(S)(ζ)(τ)((r_{1}σ)(r_{2}σ))
= eval(S)(ζ)(τ)(r_{1}σ)(eval(S)(ζ)(τ)(r_{2}σ))
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(r_{1})(eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(r_{2}))
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))(r_{1}r_{2})

\underline{\underline{t = [b]r, w.l.o.g. b ∉ fa(σ):}} Assume b : α. Let s ∈ S(U)_{α}. Set τ′_{s} := _{𝔸\\{b\}}↿τ ⊎ \{b↦s\}.

Set τ′′_{s} := _{𝔸\{b}}↿(σ ∘ eval(S)(ζ)(τ)) ⊎ {b↦s}.

\underline{Claim 1:} σ ∘ eval(S)(ζ)(τ′_{s}) = τ′′_{s}. \underline{Proof of Claim 1:} We have

(σ ∘ eval(S)(ζ)(τ′_{s}))(b) = eval(S)(ζ)(τ′_{s})(b) = τ′_{s}(b) = s = τ′′_{s}(b),

where the first equation holds because of b ∉ fa(σ). Moreover, for a ∈ nontriv(σ), we have a ≠ b, and thus

(σ ∘ eval(S)(ζ)(τ′_{s}))(a) = eval(S)(ζ)(τ′_{s})(σ(a)) = eval(S)(ζ)(τ)(σ(a)) = τ′′_{s}(a),

where the one but last equation holds by the Explicitness Lemma because of b ∉ fa(σ). Finally, for a ∉ nontriv(σ) ∪ {b}, we have (σ ∘ eval(S)(ζ)(τ′_{s}))(a) = eval(S)(ζ)(τ′_{s})(a) = τ′_{s}(a) = τ(a) = eval(S)(ζ)(τ)(a) = (σ ∘ eval(S)(ζ)(τ))(a) = τ′′_{s}(a). \underline{Q.e.d. (Claim 1)}

eval(S)(ζ)(τ)(([b]r)σ)

= eval(S)(ζ)(τ)([b](rσ))
= “the function that maps every element s ∈ S(U)_{α} to eval(S)(ζ)(τ′_{s})(rσ).”
= “the function that maps every element s ∈ S(U)_{α} to eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ′_{s}))(r).”
= “the function that maps every element s ∈ S(U)_{α} to eval(S)(ζ)(τ′′_{s})(r).”
= eval(S)(ζ)(σ ∘ eval(S)(ζ)(τ))([b]r),

where the one but last equation holds because of Claim 1. \underline{\underline{Q.e.d. (Lemma 3.7)}}

Corollary 3.8 (∀-Lemma). The following two are logically equivalent:

• eval(S)(ζ)(τ)(∀[a]A) = TRUE,

• eval(S)(ζ)(χ ⊎_{𝔸\{a}}↿τ)(A) = TRUE for every χ : {a} → S

Corollary 3.9 (∃-Lemma). The following two are logically equivalent:

• eval(S)(ζ)(τ)(∃[a]A) = TRUE,

• eval(S)(ζ)(χ ⊎_{𝔸\{a}}↿τ)(A) = TRUE for some χ : {a} → S

Corollary 3.10 (¬-Lemma). The following two are logically equivalent:

• eval(S ⊎ δ)(A) = TRUE

• eval(S ⊎ δ)(¬A) = FALSE

DRAFT

3.3. Choice-Conditions, Compatibility, and C-Validity Definition 3.11 (Choice-Condition, Return Type). C is a choice-condition if C is a partial function from variables into the set of (higherorder) ε-terms such that, for every Y ∈ dom(C), the following items hold for some types α_{0}, …, α_{l}:

1. The value C(Y) is of the form

[c_{0}] … [c_{l−1}]ε[c_{l}]B

for some formula B, and

for some mutually distinct atoms c_{0}, …, c_{l} ∈ 𝔸 with c_{0} : α_{0}, …, c_{l} : α_{l}, and for some additional constant ε_{α_{l}} : (α_{l} → o) → α_{l}, which is not interpreted by our structures and is only to be used in choice-conditions at the indicated place.

2. Y : α_{0} → ⋯ → α_{l−1} → α_{l}.

3. c_{l} ∉ fa(_{𝔸}↿id·Y) and fa(C(Y)) ⊆ fa(_{𝔸}↿id·Y).

4. fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·Y) for all Z ∈ fv(C(Y)).

In the situation described, α_{l} is the return type of C(Y). β is a return type of C if there is a Z ∈ dom(C) such that β is the return type of C(Z).

Definition 3.12 (Compatibility). Let C be a choice-condition. Let S be a structure. ζ is S-compatible with C if the following items hold:

1. ζ is an S-semantical valuation.

2. For every Y ∈ dom(C) with C(Y) = [c_{0}] … [c_{l−1}]ε[c_{l}]B for some formula B, and for every τ : 𝔸 → S :

If  eval(S)(ζ)(τ)(B) = TRUE
then eval(S)(ζ)(τ)(B[c_{l} ↦ (_{𝔸}↿id·Y)(c_{0}) ⋯ (c_{l−1})]) = TRUE as well.

Definition 3.13 (C-validity, K). Let C be a choice-condition. Let G be a set of sequents. Let S be a structure. G is C-valid in S if G is ⟨ ζ , S ⟩-valid for some ζ that is S-compatible with C. G is ⟨ ζ , S ⟩-valid if eval(S)(ζ)(τ)(G) = TRUE for every τ : 𝔸 → S. Validity in a class of structures is understood as validity in each of the structures of that class. If we omit the reference to a special structure we mean validity in some fixed class K of structures, such as the class of all structures or the class of Herbrand structures over the given signature.

DRAFT

3.4. Reduction Definition 3.14 (Reduction). Let C be a choice-condition. Let G_{0} and G_{1} be sets of sequents. Let S be a structure. G_{0} C-reduces to G_{1} in S if for every ζ that is S-compatible with C:

If G_{1} is ⟨ ζ , S ⟩-valid, then G_{0} is ⟨ ζ , S ⟩-valid as well.

Definition 3.15 (Extended Extension). C′ is an extended extension of C if

• C is a choice-condition,

• C′ is a choice-condition,

• C ⊆ C′.

Corollary 3.16. Let C′ be an extended extension of C. If ζ is S-compatible with C′, then ζ is S-compatible with C.

Definition 3.17 (Extended θ-Update). Let C be a choice-condition and let θ be a variable substitution. The extended θ-update C′ of C is given as follows:

C′ := { ⟨ X , tθ ⟩ | ⟨ X , t ⟩ ∈ C and X ∉ nontriv(θ) }.

Definition 3.18 (Q_{C}). Q_{C} is the function that maps every Z ∈ dom(C) with C(Z) = [c_{0}] ⋯ [c_{l−1}]ε[c_{l}]B (for some atoms c_{0}, …, c_{l} and some formula B) to the single-formula sequent

∀[c_{0}] ⋯ [c_{l−1}]( ∃[c_{l}]B ⇒ B[c_{l} ↦ Z(c_{0}) ⋯ (c_{l−1})] )

and is otherwise undefined.

Theorem 3.19 (Reduction). Let C be a choice-condition. Let G_{0}, G_{1}, G_{2}, and G_{3} be sets of sequents. Let S be a structure.

1. (Validity) \begin{matrix}If G_{0} C-reduces to G_{1} in S and G_{1} is C-valid in S, \\ then G_{0} is C-valid in S, too. \end{matrix}

2. (Reflexivity) In case of G_{0} ⊆ G_{1}: G_{0} C-reduces to G_{1} in S.

3. (Transitivity) \begin{matrix}If G_{0} C-reduces to G_{1} in S \\ and G_{1} C-reduces to G_{2} in S, \\ then G_{0} C-reduces to G_{2} in S. \end{matrix}

4. (Additivity) \begin{matrix}If G_{0} C-reduces to G_{2} in S \\ and G_{1} C-reduces to G_{3} in S, \\ then G_{0} ∪ G_{1} C-reduces to G_{2} ∪ G_{3} in S. \end{matrix}

5. (Monotonicity) For C′ being an extended extension of C:

(a) If G_{0} is C′-valid in S, then G_{0} is also C-valid in S.

(b) If G_{0} C-reduces to G_{1} in S, then G_{0} also C′-reduces to G_{1} in S.

DRAFT

6. (Instantiation) \begin{matrix}Let θ be a variable substitution. \\ Let C′′ be the extended θ-update of C. \\ Set M := nontriv(θ) ∩ dom(C). \\ Set O := M ∩ \{ Z ∈ 𝕍 | ∃Y ∈ fv(G_{0}, G_{1}). fa(Z) ⊆ fa(Y) \}. \\ Set O′ := dom(C) ∩ \{ X ∈ 𝕍 | ∃Y ∈ M\O. fa(Y) ⊆ fa(X) \}. \\ Assume that for every Y ∈ O′ and for every return type α of C(Y), \\ there is a generalized choice function \\ on the power-set of the universe of S for the type α. \end{matrix}

(a) If G_{0}θ ∪ (⟨O⟩Q_{C})θ is C′-valid in S, then G_{0} is C-valid in S.

(b) If G_{0} C-reduces to G_{1} in S, then G_{0}θ C′-reduces to G_{1}θ ∪ (⟨O⟩Q_{C})θ in S.

3.4.1. Proof of Theorem 3.15

Items 1 to 4 are trivial consequences of the definitions of C-reduction, C-validity, and of truth of a set of sequents under the evaluation function; whereas the the validity of Items 1 to 4 does not depend on the the concrete evaluation of a sequent or its parts. \underline{\underline{(5a):}} Assume that G_{0} is C′-valid in S. Then there is some ζ that is S-compatible with C′

such that G_{0} is ⟨ ζ , S ⟩-valid. By Corollary 3.16, ζ is S-compatible with C as well. Thus, G_{0} is C-valid in S. \underline{\underline{(5b):}} Suppose that ζ is S-compatible with C′ and that G_{1} is ⟨ ζ , S ⟩-valid. By Corol-

lary 3.16, ζ is S-compatible with C as well. Thus, under the assumption that G_{0} C-reduces to G_{1} in S, also G_{0} is ⟨ ζ , S ⟩-valid, as was to be shown. \underline{\underline{(6):}}

DRAFT

4. Proof-search

Let A, B range over formulas. Let Γ, Δ, Θ range over sequents.

As we want to use the following rules for reductive proof search, we have inverted the rules such that passing the line (or bar) means reduction instead of consequence (as in standard presentation). This means that the essential function of our rules is that the sequent on top of the bar is a consequence of the sequences below it.

In this paper, however, all rules will actually be strong equivalence transformations in the following sense, which we describe semantically here: For the given choicecondition C, and for every structure S of the given signature, the singleton set of sequences above the line and the the set of sequences below the line mutually C-reduce to each other.

Moreover, this strong kind of equivalence will be invariant under substitution of variables.

4.1. γ-Rule

For proof search, the term t in the following rule will typically be a fresh variable having all atoms that are currently in use in its permission set.

Γ ∃[a]A Δ ; \overline{γ(t)(∃)} ; A[a↦t] Γ ∃[a]A Δ  Γ ¬∀[a]A Δ ; \overline{γ(t)(∀)(¬)} ; ¬A[a↦t] Γ ¬∀[a]A Δ

Note that the principal formula of the upper sequent is repeated in the lower sequent for two reasons:

1. For the above mentioned strong equivalence, the lower sequent must remain valid even if we pick a wrong term t.

2. For first-order completeness we may need different terms t closing different branches (γ-multiplicity).

4.2. δ^{−}-Rules

Note that the principal formula of the upper sequent of the following rule is deleted in the lower sequent.

The following rules come with proviso that a ∉ fa(Γ, Δ):

Γ ∀[a]A Δ ; \overline{δ^{−}(a)(∀)} ; A Γ Δ  Γ ¬∃[a]A Δ ; \overline{δ^{−}(a)(∃)(¬)} ; ¬A Γ Δ

DRAFT

4.3. δ^{ε}-Rules

The following rules are nothing but a variant of Hilbert’s formulas (ε_{2}) and (ε_{1}) for eliminating the universal and the existential quantifiers.

Γ ∀[a]A Δ ; \overline{δ^{ε}(a)(∀)} ; A[a↦ε[a]¬A] Γ Δ  Γ ¬∃[a]A Δ ; \overline{δ^{ε}(a)(∃)(¬)} ; ¬A[a↦ε[a]A] Γ Δ

Note that the δ^{ε}-rules are not part of our inference system, but server only for motivation of the δ^{+}-rules

4.4. δ^{+}-Rule

The bad thing about δ^{ε}-rule is that the huge introduced ε-term is hardly any help in proof search. Therefore, in the following δ^{+}-rule, this term is replaced with its abstraction_{𝔸}↿id·X. For the soundness (direction of the strong equivalence property mentioned above) of the δ^{+}-rule, we have to put X ↦ ε[a]¬A as an entry into our choicecondition.^{1} By this trick, we can restrict the occurrences of the ε to the choice-condition. The entry in the choice-condition will restrict future substitutions of X to satisfy Hilbert’s formula (ε_{0}).

The following rules come with proviso that X and a have the same type; X ∉ dom(C) for our global choice-condition C; a ∉ fa(_{𝔸}↿id·X); fa(A)\{a} ⊆ fa(_{𝔸}↿id·X); and fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·X) for every Z ∈ fv(A):

Γ ∀[a]A Δ
\overline{δ^{+}(_{𝔸}↿id·X)(∀)}

A[a ↦ _{𝔸}↿id·X] Γ Δ

Γ ¬∃[a]A Δ
\overline{δ^{+}(_{𝔸}↿id·X)(∃)(¬)}
¬A[a ↦ _{𝔸}↿id·X] Γ Δ

Moreover, if we perform such a δ^{+}(_{𝔸}↿id·X)(∀)-step, we set C(X) := ε[a]¬A; similarly, we set C(X) := ε[a]A in case of a δ^{+}(_{𝔸}↿id·X)(∃)(¬)-step.

The proviso “fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·X)” has the following function: We have to block the substitution Z↦_{𝔸}↿id·X, because this would destroy the correctness of the rule.^{2} We express this here with the proper inclusion of fa(_{𝔸}↿id·Z) in fa(_{𝔸}↿id·X). See Example 4.1.

1We do not have the possibility omit the entry into the choice-condition by adding

(_{𝔸}↿id·X = ε[a]¬A) Γ ∀[a]A Δ as a second lower sequent to the δ^{+}-rule because this destroys safeness and first-order completeness.

2The substitution X↦_{𝔸}↿id·Z is not a problem, however, provided that ∀[a]A ⇒ A[a↦Z] holds.

DRAFT

Example 4.1. The formula ∃[b]∀[a](b = a) is not generally valid. We can start a proof attempt as follows:

γ(_{𝔸}↿id·Z)-step: ( ∀[a](b = a) )[b ↦ _{𝔸}↿id·Z], ∃[b]∀[a](b = a)

Under the condition of a ∉ fa(_{𝔸}↿id·Z), this reads as follows:

∀[a](_{𝔸}↿id·Z = a), ∃[b]∀[a](b = a)

δ^{+}(_{𝔸}↿id·X)-step: (_{𝔸}↿id·Z = _{𝔸}↿id·X), ∃[b]∀[a](b = a) Now, if the variable Z could be replaced with_{𝔸}↿id·X by substitution, we would get the tautology (_{𝔸}↿id·Z = _{𝔸}↿id·Z), i.e. we would have proved an invalid formula. To prevent this, the δ^{+}(_{𝔸}↿id·X)-step has the proviso fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·X).

DRAFT

Example 4.2. For an initially empty choice-condition C := ∅, let us try to prove Plato’s Principle:^{3} ∃[a](∃[b](pb) ⇒ (pa)) A γ(_{𝔸}↿id·Y)-step applied to Plato’s Principle results in:

∃[b](pb) ⇒ (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa))

α-step: ¬∃[b](pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa)) δ^{−}(b)-step with proviso that b ∉ fa(_{𝔸}↿id·Y):

¬(pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa))

γ(_{𝔸}↿id·Y′)-step:

∃[b](pb) ⇒ (p(_{𝔸}↿id·Y′)), ¬(pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa))

α-step: ¬∃[b](pb), (p(_{𝔸}↿id·Y′)), ¬(pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa)) Now we can apply the substitution Y′↦b to the whole proof tree. Afterwards the proof tree is closed with a tautology of the form Γ, A, Δ, ¬A, Θ, and so we have proved Plato’s Principle. Note that we were not able to close the tree before via Y ↦b, because the δ^{−}-step introduced b ∉ fa(_{𝔸}↿id·Y).

Now, to show how liberalization of the δ-rule works, we could continue the previous proof after the first α-step with a δ^{+}-step instead of the δ^{−}-step. Let us do something stronger instead. Let us ask for a solution (similar to a Prolog query) to Plato’s Principle by starting with the logically equivalent, but proof-technically harder input theorem ∃[b](pb) ⇒ (p_{𝔸}↿id·Y), which is a subsequent of our second sequent of the previous proof. From a proof of this formula we will get a proof of Plato’s Principle simply by adding the formula ∃[a](∃[b](pb) ⇒ (pa)) to the end of each of its sequents and adding the original γ-step to the added root ∃[a](∃[b](pb) ⇒ (pa)) of the new proof tree. All in all, the first proof, consisting of the steps γ(_{𝔸}↿id·Y), α, δ^{−}(b), γ(b), α, which is the shortest one possible with the δ^{−}-rules as the only δ-rules, will then be shortened to γ(_{𝔸}↿id·X), α, δ^{+}(_{𝔸}↿id·X).^{4} Here comes the announced proof of the new input formula ∃[b](pb) ⇒ (p(_{𝔸}↿id·Y)) α-step: ¬∃[b](pb), (p(_{𝔸}↿id·Y)) δ^{+}(_{𝔸}↿id·X)-step with proviso of b ∉ fa(_{𝔸}↿id·X) and p ∈ fa(_{𝔸}↿id·X), and with choice-condition C(X) := ε[b](pb): ¬(p(_{𝔸}↿id·X)), (p(_{𝔸}↿id·Y)) After application of the substitution Y ↦_{𝔸}↿id·X, we get a closed proof tree for the now instantiated input theorem ∃[b](pb) ⇒ (p(_{𝔸}↿id·X)). Moreover, by looking at the current choice-condition, the user gets the information that ε[b](pb) is a solution for X.

Summing up, with the substitution Y′↦b executed globally, the first proof reads in full: ∃[a](∃[b](pb) ⇒ (pa)) γ(_{𝔸}↿id·Y)-step: ∃[b](pb) ⇒ (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa)) α-step: ¬∃[b](pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa)) δ^{−}(b)-step with proviso that b ∉ fa(_{𝔸}↿id·Y):

¬(pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa))

γ(b)-step: ∃[b](pb) ⇒ (pb), ¬(pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa)) α-step: ¬∃[b](pb), (pb), ¬(pb), (p(_{𝔸}↿id·Y)), ∃[a](∃[b](pb) ⇒ (pa))

3Plato’s Principle is equivalent in intuitionistic logic to each of Hilbert’s formulas (ε_{0}) and (ε_{1}) and to Hilbert’s ε-formula.

4In general, shortest proofs of some families of formulas (indexed by natural numbers) are shortened exponentially and even non-elementary by replacing the δ^{−}-rules with the δ^{+}-rules. Moreover, the δ^{+}-rules help humans to give proof hints to semi-automated proof procedures.

DRAFT

Moreover, with the substitution Y ↦_{𝔸}↿id·X executed globally, the second proof reads in full: ∃[a](∃[b](pb) ⇒ (pa)) γ(_{𝔸}↿id·X)-step: ∃[b](pb) ⇒ (p(_{𝔸}↿id·X)), ∃[a](∃[b](pb) ⇒ (pa)) α-step: ¬∃[b](pb), (p(_{𝔸}↿id·X)), ∃[a](∃[b](pb) ⇒ (pa)) δ^{+}(_{𝔸}↿id·X)-step: ¬(p(_{𝔸}↿id·X)), (p(_{𝔸}↿id·X)), ∃[a](∃[b](pb) ⇒ (pa))

Theorem 4.3. Let C be a choice-condition. Let S be a structure. Let us consider any of the γ-, δ^{−}-, and δ^{+}-rules of this section. Let G_{0} and G_{1} be the sets of the sequent above and of the sequents below the bar of that rule, respectively. Let C′′ be the singleton set of the pair by which the considered rule extends the choice-condition (applies only to the δ^{+}-rules) or the empty set otherwise. Let us set C′ := C ∪ C′′, Then C′ is an extended extension of C; moreover, the considered inference rule is sound, safe, and solution-preserving in the sense that G_{0} and G_{1} mutually C′-reduce to each other in S.

4.4.1. Proof of Theorem 4.3

To illustrate our techniques, we only treat the first rule of each kind; the other rules can be treated most similar. In the situation described in the theorem, it suffices to show that C′ is a choice-condition (because the other properties of an extended extension are trivial), and that, for every S-semantical valuation ζ that is S-compatible with C′, the sets G_{0} and G_{1} of the upper and lower sequents of the inference rule are equivalent w.r.t. their ⟨ ζ , S ⟩-validity. \underline{\underline{γ-rule:}} In this case we have C′ = C. Thus, C′ is a choice-condition by assumption of

the theorem. Moreover, for every S-valuation τ : 𝔸 → S, the values of

{Γ ∃[a]A Π} and {A[a↦t] Γ ∃[a]A Π}

under eval(S)(ζ)(τ) are indeed the same:

If the left one is TRUE, then so is the right one, because the former sequent is a sub-sequent of the latter.

For the other direction, assume that eval(S)(ζ)(τ)(A[a↦t]) = TRUE. Thus, by the Substitution [Value] Lemma (second equation) and the Valuation Lemma for l = 0 (third equation):

TRUE = eval(S)(ζ)(τ)(A[a↦t])
= eval(S)(ζ)([a↦t] ∘ eval(S)(ζ)(τ))(A)
= eval(S)(ζ)({a ↦ eval(S)(ζ)(τ)(t)} ⊎_{𝔸\{a}}↿τ)(A)

Thus, by the backward direction of the ∃-Lemma, ∃[a]A evaluates to TRUE under eval(S)(ζ)(τ). Thus, so does the left sequent. \underline{\underline{Q.e.d. (γ-rule)}} \underline{\underline{δ^{−}-rule:}} In this case we have C′ = C. Thus, C′ is a choice-condition by assumption of

the theorem. Moreover, in this case, we have a ∉ fa(Γ, Δ). Let α be the type

of a.

Now, for the soundness direction, it suffices to show the contrapositive, namely to assume that there is an S-valuation τ : 𝔸 → S such that

eval(S)(ζ)(τ)(Γ ∀[a]A Π) = FALSE,

DRAFT

and to show that there is an S-valuation τ′ : 𝔸 → S such that eval(S)(ζ)(τ′)(A Γ Π) = FALSE. This follows directly from Claims 2 and 4 below. \underline{Claim 2:} eval(S)(ζ)(τ′)(Γ Π) = FALSE for all τ′ : 𝔸 → S with _{𝔸\\{a\}}↿τ′ = _{𝔸\\{a\}}↿τ. \underline{Proof of Claim 2:} Under the above assumption, we have eval(S)(ζ)(τ)(Γ Π) = FALSE. Thus, Claim 2 holds by the Explicitness Lemma because of a ∉ fa(Γ, Δ).

Q.e.d. (Claim 2)

\underline{Claim 4:} There is a τ′ : 𝔸 → S with _{𝔸\\{a\}}↿τ′ = _{𝔸\\{a\}}↿τ, such that eval(S)(ζ)(τ′)(A) = FALSE. \underline{Proof of Claim 4:} Under the above assumption, we also have eval(S)(ζ)(τ)(∀[a]A) = FALSE. By the backward direction of the ∀-Lemma, this means that there is some s ∈ S(U)_{α} such that, for τ′ := {a↦s} ⊎ _{𝔸\{a}}↿τ, we have eval(S)(ζ)(τ′)(A) = FALSE.

Q.e.d. (Claim 4)

Now, for the safeness direction of the proof, let us assume that for some S-valuation τ : 𝔸 → S we have

eval(S)(ζ)(τ)(Γ ∀[a]A Π) = TRUE.

It suffices to show eval(S)(ζ)(τ)(Γ A Π) = TRUE. This is obviously the case if eval(S)(ζ)(τ)(Γ Π) = TRUE. Otherwise, we have eval(S)(ζ)(τ)(∀[a]A) = TRUE, in which case we get eval(S)(ζ)(τ)(A) = TRUE by the forward direction of the ∀-Lemma.

\underline{\underline{Q.e.d. (δ^{−}-rule)}}

\underline{\underline{δ^{+}-rule:}} In this case, we have that X and a have the same type; X ∉ dom(C) for

our global choice-condition C; a ∉ fa(_{𝔸}↿id·X); fa(A)\{a} ⊆ fa(_{𝔸}↿id·X); and fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·X) for every Z ∈ fv(A). Moreover, we have C′ = C ∪ {⟨ X , ε[a]¬A ⟩}. \underline{Claim 7:} C′ is a choice-condition. \underline{Proof of Claim 7:} As X ∈ 𝕍 \ dom(C), we know that C′ is a partial function on 𝕍 just as C. Moreover, for Y ∈ dom(C′), we either have Y ∈ dom(C) and then the requirements of Definition 3.11 are satisfied by assumption of the theorem, or else we have Y = X, in which case we have to verify the following:

1. The value C(Y) is of the form

[c_{0}] … [c_{l−1}]ε[c_{l}]B

for some formula B, and

for some mutually distinct atoms c_{0}, …, c_{l} ∈ 𝔸 with c_{0} : α_{0}, …, c_{l} : α_{l}

2. Y : α_{0} → ⋯ → α_{l−1} → α_{l}.

3. c_{l} ∉ fa(_{𝔸}↿id·Y) and fa(C(Y)) ⊆ fa(_{𝔸}↿id·Y).

4. fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·Y) for all Z ∈ fv(C(Y)).

So we take l := 0, c_{0} := a, B := ¬A. Moreover, we take α_{0} to be the common type of X and a. Then Items 1 and 2 are immediately satisfied. And for Item 3 we just have to note that here we have C(Y) = ε[a]¬A, and thus c_{l} = c_{0} = a ∉ fa(_{𝔸}↿id·X) = fa(_{𝔸}↿id·Y) and fa(C(Y)) = fa(A)\{a} ⊆ fa(_{𝔸}↿id·X) = fa(_{𝔸}↿id·Y). Finally, for Item 4, in case of Z ∈ fv(C(Y)), we have Z ∈ fv(A), and thus fa(_{𝔸}↿id·Z) ⊊ fa(_{𝔸}↿id·X) = fa(_{𝔸}↿id·Y).

Q.e.d. (Claim 7)

DRAFT

Now, for ζ being an S-semantical valuation that is S-compatible with C′, and for τ : 𝔸 → S, it suffices to show that

eval(S)(ζ)(τ)(Γ ∀[a]A Δ) = TRUE

iff

eval(S)(ζ)(τ)(Γ A[a ↦ _{𝔸}↿id·X] Δ) = TRUE.

For the soundness direction, suppose that the latter is the case. If eval(S)(ζ)(τ)(Γ Δ) = TRUE, then eval(S)(ζ)(τ)(Γ ∀[a]A Δ) = TRUE, as was to be shown. Otherwise, we have eval(S)(ζ)(τ)(A[a ↦ _{𝔸}↿id·X]) = TRUE, and thus eval(S)(ζ)(τ)(¬A[a ↦ _{𝔸}↿id·X]) = FALSE by the ¬-Lemma. By Lemma 2.21, we have a ∈ fa(A[a ↦ _{𝔸}↿id·X]) only if a ∈ fa(_{𝔸}↿id·X), which is not the case. Thus, by the Explicitness Lemma, for all τ′ : 𝔸 → S with _{𝔸\{a}}↿τ = _{𝔸\{a}}↿τ′, we have eval(S)(ζ)(τ′)(¬A[a ↦ _{𝔸}↿id·X]) = FALSE. As ζ is S-compatible with C′, we have eval(S)(ζ)(τ′)(¬A) = FALSE because of C′(X) = ε[a]¬A. Thus, eval(S)(ζ)(τ′)(A) = TRUE by the ¬-Lemma. Thus, eval(S)(ζ)(τ)(∀[a]A) = TRUE by the ∀-Lemma. Thus, eval(S)(ζ)(τ)(Γ ∀[a]A Δ) = TRUE, as was to be shown.

For the safeness direction of the proof, assume that eval(S)(ζ)(τ)(Γ ∀[a]A Π) = TRUE. It suffices to show eval(S)(ζ)(τ)(Γ A[a ↦ _{𝔸}↿id·X] Π) = TRUE. This is obviously the case if eval(S)(ζ)(τ)(Γ Π) = TRUE. Otherwise, we have eval(S)(ζ)(τ)(∀[a]A) = TRUE and it suffices to show eval(S)(ζ)(τ)(A[a ↦ _{𝔸}↿id·X]) = TRUE. By the Substitution [Value] Lemma, it suffices to show eval(S)(ζ)([a ↦ _{𝔸}↿id·X] ∘ eval(S)(ζ)(τ))(A) = TRUE, but this is the case by the forward direction of the ∀-Lemma because, for b ∈ 𝔸\{a}, we have ([a ↦ _{𝔸}↿id·X] ∘ eval(S)(ζ)(τ))(b) = eval(S)(ζ)(τ)(b) = τ(b) because of the Valuation Lemma for l = 0. \underline{\underline{Q.e.d. (δ^{+}-rule)}}

Q.e.d. (Theorem 4.3)

DRAFT

5. Background on nominal sets

Definition 5.1. The cumulative hierarchy of ZFA sets U is the least fixedpoint U = 𝔸 ∪ powerset(U). This can be constructed by starting from atoms and transfinitely adding all subsets (a construction going back to Neumann [? ]).

Definition 5.2. Given a, b ∈ 𝔸 write (a b) for the swapping bijection on atoms mapping a to b, b to a, and any other c ∈ 𝔸 \ {a, b} to c.

If π is a bijection on atoms define nontriv(π) = {a | π(a) ≠ a}.

Write ℙ for the group of bijections (finitely) generated by swappings, and call these bijections permutations.

Write π ∘ π′ for the composition of first π and then π′ (so (π ∘ π′)(a) = π′(π(a))). Write id for the identity permutation (so id(a) = a always).

Lemma 5.3. A bijection π on atoms is a permutation if and only if nontriv(π) = {a | π(a) ≠ a} is finite.

Definition 5.4. Give U a permutation action π·x inductively defined by π·a = π(a) for a ∈ 𝔸, and π·X = {π·x | x ∈ X} for X ∈ U \ 𝔸.

If A ⊆ 𝔸 write fix(A) = {π ∈ ℙ | ∀a∈A.π(a) = a}.

Say that A ⊆ 𝔸 supports x ∈ U when ∀π∈fix(A).π·x = x.

Definition 5.5. Call an element x ∈ U finitely-supported when it has a unique least finite supporting set supp(x). Write a#x for a ∉ supp(x) and read this as ‘a is fresh for x’.

Lemma 5.6 ([? ? ]). If x ∈ U has a finite supporting set A, then supp(x) exists.

Our reasoning can be formalised in first-order logic, enriched with the axioms of Zermelo-Fraenkel set theory with atoms (ZFA). This is just a formal way of stating that we have assumed atoms and sets and we reason about them mathematically, but stating it in terms of formal logic lets us express an important observation, that our reasoning is symmetric under permutation:

Theorem 5.7. If \overline{x} denotes a list x_{1}, …, x_{n}, write π·\overline{x} for π·x_{1}, …, π·x_{n}. Suppose Φ(\overline{x}) is a ZFA predicate on variables included in \overline{x}. Then we have equivariance [? , Section 4]:^{5} Φ(\overline{x}) ⇔ Φ(π·\overline{x}).

We will appeal to equivariance repeatedly to quickly yet rigorously rename atoms, usually while retaining an inductive hypothesis. See for instance Lemma 7.2.^{6}

Definition 5.8. Say that X ∈ U \ 𝔸 has the trivial action when supp(x) = ∅ for every x ∈ X (equivalently: when π·x = x for every x ∈ X and permutation π).

Definition 5.9. If X, Y ∈ U \𝔸 then a function(-set) from X to Y is a subset of X ×Y such that ∀x∈X.∃y∈Y.(x, y) ∈ f and ∀x, y, y′.((x, y) ∈ f ∧ (x, y′) ∈ f) ⇒ y = y′. Write X→Y for the set of all functions from X to Y. Write X ⇒ Y for the set of all functions from X to Y with finite support.

Remark 5.10. The permutation action from Definition 5.4 gives f ∈ X→Y the conjugation permutation action specified by π·(f(x)) = (π·f)(π·x).

5\overline{x} must contain all the variables mentioned in the predicate. It is not the case that a = a if and only if a = b—but it is the case that a = b if and only if b = a.

6This technique was used in pencil-and-paper mathematics instead of long inductive proofs, e.g. in [? ].

DRAFT

Lemma 5.11. If X and Y in U \ 𝔸 have the trivial permutation action (Definition 5.8), then so does X→Y, and X→Y = X ⇒ Y. (If underlying sets have empty support then so do functions between them.)

6. Nominal models for simple type theory

6.1. Nominal λ-model Definition 6.1. An interpretation ℐ consists of an assignment for each type ϕ of a nominal set ⟦ϕ⟧^{ℐ} together with the following data:

1. For every a:ϕ [mjg atoms have inherent types] an element a^{ℐ} ∈ ⟦ϕ⟧^{ℐ}.

2. For every constant f an equivariant element f^{ℐ} ∈ ⟦type(f)⟧^{ℐ}.

3. If x ∈ ⟦α⟧^{ℐ}, an element [a_{α}]x ∈ ⟦α→β⟧^{ℐ}.

4. For x ∈ ⟦α→β⟧^{ℐ} and y ∈ ⟦α⟧^{ℐ}, an element x • y ∈ ⟦β⟧^{ℐ}.

ℐ must be equivariant in the sense that:

\begin{matrix}π·a^{ℐ} = & (π(a))^{ℐ} & π·f^{ℐ} = & f^{ℐ} \\ π·[a]x = & [π(a)]π·x & π·(x • y) = & (π·x) • (π·y) \end{matrix}

We write x[a↦y] as sugar for ([a]x) • y. Be aware that this is not necessary real substitution! In addition, ℐ must satisfy the following equalities:

(Suba)  a^{ℐ}[a↦x]  = x
(Sub#)  a#z ⇒ z[a↦x]  = z
(SubApp)  (z′ • z)[a↦x] = (z′[a↦x]) • (z[a↦x])
(Subλ)  c#x ⇒ ([c]z)[a↦x] = [c](z[a↦x])
(SubId)  z[a↦a^{ℐ}]  = z

Definition 6.2. A (level 1) substitution σ is a total function on atoms such that:

• dom(σ) = {a | σ(a) ≠ a} is finite.

• If a : ϕ then a ∈ ⟦ϕ⟧^{ℐ}.

If dom(σ) = {a_{1}, …, a_{n}} and σ(a_{i}) = x_{i} for 1≤i≤n then we may write σ as [a_{i}↦x_{i}]_{1}^{n}.

Definition 6.3. Suppose x ∈ ⟦ϕ⟧^{ℐ}. Specify x·[a_{i}↦x_{i}]_{1}^{n} by

x·[a_{i}↦x_{i}]_{1}^{n} = (((c_{1} a_{1}) ∘ ⋯ ∘ (c_{n} a_{n}))·x)[c_{1}↦x_{1}] … [c_{n}↦x_{n}]

for fresh c_{1}, …, c_{n} (so c_{i} ∉ supp(x) ∪ ⋃_{i} supp(x_{i}) for 1 ≤ i ≤ n).

Remark 6.4. The equalities (Suba) to (SubId) in Definition 6.1only give us substitution for one atom at a time. It is easy to extend this to a simultaneous substitution [a_{i}↦x_{i}]_{1}^{n}, but there is a catch; it might be that a_{i} ∈ supp(x_{j}). So in Definition 6.3 we ‘rename atoms fresh’ first, and then substitute for these atoms one at a time. Certain detailed but routine verifications are necessary to make sure this works and is well-defined (depends neither on the fresh choice of c_{i}, nor on the order in which the substitutions are then carried out). The relevant maths is described in [? , Section 6].

DRAFT

Definition 6.5. Call σ closing for x ∈ ⟦ϕ⟧^{ℐ} when supp(x·σ) = ∅.

Call an interpretation ℐ extensional when if x·σ = x′·σ for all closing substitutions for x and x′, then x = x′.

Definition 6.6. Call an interpretation ℐ Boolean when ⊤^{ℐ} ≠ ⊥^{ℐ} and

{x ∈ ⟦o⟧_{∅}^{ℐ} | supp(x) = ∅} = {⊤^{ℐ}, ⊥^{ℐ}}.

If ℐ is Boolean then ⟦o⟧^{ℐ} has a lattice structure, defined by if x, y ∈ ⟦o⟧^{ℐ} then x ≤ y when for every σ:

• If x·σ = ⊤^{ℐ} then y·σ = ⊤^{ℐ}.

• If x·σ = ⊥^{ℐ} then y·σ ∈ {⊥^{ℐ}, ⊤^{ℐ}}. [mjg ??]

Definition 6.7. Call ℐ a model when it is Boolean and extensional, and furthermore the distinguished constants from Definition 2.5 have distinguished behaviour as follows:

• ∧^{ℐ} • ⊤^{ℐ} • ⊤^{ℐ} = ⊤^{ℐ} and ∧^{ℐ} • ⊤^{ℐ} • ⊥^{ℐ} = ⊥^{ℐ} … and so on.

• ∨^{ℐ} • ⊤^{ℐ} • ⊤^{ℐ} = ⊤^{ℐ} and ∨^{ℐ} • ⊤^{ℐ} • ⊥^{ℐ} = ⊤^{ℐ} … and so on.

• ¬^{ℐ} • ⊤^{ℐ} = ⊥^{ℐ} and ¬^{ℐ} • ⊥^{ℐ} = ⊤^{ℐ}.

• Suppose x ∈ ⟦o⟧^{ℐ}. Then:

\begin{matrix}∀^{ℐ} • [a:ϕ]x = & ⋀\{x[a:ϕ↦y] | y ∈ ⟦ϕ⟧^{ℐ}\} \\ ∃^{ℐ} • [a:ϕ]x = & ⋁\{x[a:ϕ↦y] | y ∈ ⟦ϕ⟧^{ℐ}\} \end{matrix}  (1)

• Suppose f ∈ ⟦α→o⟧_{∅}^{ℐ}. Then if there exists x ∈ ⟦α⟧_{∅}^{ℐ} [mjg use this notation for empty support?] such that f • x = ⊤^{ℐ} then f(ε_{α}(f)) = ⊤^{ℐ}. [mjg x has empty support?]

Definition 6.8. A valuation ζ is a map on variables. Write Γ ⊢ ζ when ζ(X) ∈ ⟦type(X)⟧^{ℐ} for every variableX.

Definition 6.9. Suppose ℐ is a model. Suppose Γ ⊢ r : ϕ. Define an interpretation ⟦r⟧_{ζ}^{ℐ} ∈ ⟦ϕ⟧_{ζ}^{ℐ} and ⟦σ⟧_{ζ}^{ℐ} inductively by:

\begin{matrix}⟦a⟧_{ζ}^{ℐ} = & a^{ℐ} & ⟦f⟧_{ζ}^{ℐ} = & f^{ℐ} & ⟦X·σ⟧_{ζ}^{ℐ} = & ζ(X)·⟦σ⟧_{ζ}^{ℐ} \\ ⟦rs⟧_{ζ}^{ℐ} = & ⟦r⟧_{ζ}^{ℐ} • ⟦s⟧_{ζ}^{ℐ} & ⟦[a]r⟧_{ζ}^{ℐ} = & [a]⟦r⟧_{ζ}^{ℐ} & ⟦σ⟧_{ζ}^{ℐ}(a) = & ⟦σ(a)⟧_{ζ}^{ℐ} \end{matrix}

Lemma 6.10. 1. ⟦r[X↦s]⟧_{ζ}^{ℐ} = ⟦r⟧_{ζ[X↦⟦s⟧^{ℐ}_{ζ}]}^{ℐ}.

2. ⟦r[a↦s]⟧_{ζ}^{ℐ} = ⟦r⟧_{ζ}^{ℐ}[a↦⟦s⟧_{ζ}^{ℐ}].

[mjg to check]

Definition 6.11. A choice condition is an equality of the form X=ε(r) where fa(r) ⊆ fa(X) and X ∉ fv(r). If C is a set of choice conditions define ⟦C⟧_{ζ}^{ℐ} by:

• ⟦C⟧_{ζ}^{ℐ} = ⊤^{ℐ} when ζ(X) = ⟦ε(r)⟧_{ζ}^{ℐ} for every (X=ε(r)) ∈ C.

• ⟦C⟧_{ζ}^{ℐ} = ⊥^{ℐ} if ζ(X) ≠ ⟦ε(r)⟧_{ζ}^{ℐ} for some (X=ε(r)) ∈ C.

A sequent S is a list of formulae [mjg i.e. terms of type o]. A hypersequent H is a set of sequents. A problem is a pair (C, H) of a choice condition and a hypersequent.

Define an interpretation of problems as follows: [mjg work on this]

⟦(C, H)⟧^{ℐ} = ∃ζ.(⟦C⟧_{ζ}^{ℐ} ∧ ⋀_{S∈H} ⋁_{P ∈S}⟦P ⟧_{ζ}^{ℐ} = ⊤^{ℐ})

DRAFT

We need to verify soundness of the [mjg] rules:

Lemma 6.12 (Rule (γ)). Suppose Γ ⊢ A : o and Γ ⊢ ζ. Then:

• ⟦A[a↦t]⟧_{ζ}^{ℐ} ≤ ⟦∃a.A⟧_{ζ}^{ℐ}.

• ⟦A[a↦t]⟧_{ζ}^{ℐ} ≥ ⟦∀a.A⟧_{ζ}^{ℐ}.

Proof. By construction in equation (1).

Lemma 6.13. Suppose X ∉ fv(r). Then ⟦r[a↦X]⟧_{ζ}^{ℐ} = ⟦r⟧_{ζ}^{ℐ}[a↦ζ(X)].

Proof. By a routine induction on r. [mjg expand]

Lemma 6.14. (ϵ • f)·σ = ϵ • (f·σ).

As a corollary, if (f •(ϵ•f))·σ = ⊥^{ℐ} then (f·σ)•x = ⊥^{ℐ} for all closed x. [mjg put in types]

Lemma 6.15. Suppose Γ ⊢ A : o and Γ ⊢ ζ. Suppose X ∉ fv(A) and ζ(X) = ε(⟦[a:ϕ]¬A⟧_{ζ}^{ℐ}). Then

⟦A[a↦X]⟧_{ζ}^{ℐ} = ⟦∀a.A⟧_{ζ}^{ℐ}.

Proof. By extensionality (Definition 6.5) it suffices to show for each closing substitution σ that

⟦A[a↦X]⟧_{ζ}^{ℐ}·σ = ⟦∀a.A⟧_{ζ}^{ℐ}·σ.

Suppose σ is closing and by [mjg stuff] suppose that dom(σ) = fa(A)\{a}. There are two possibilities:

• The case that ⟦A[a↦X]⟧_{ζ}^{ℐ}·σ = ⊥^{ℐ}. Then

⟦∀ • [a:ϕ]A⟧_{ζ}^{ℐ}·σ ≤ ⟦A⟧_{ζ}^{ℐ}[a↦ζ(X)]·σ  Definition 6.7
= ⟦A[a↦ζ(X)]⟧_{ζ}^{ℐ}·σ  Lemma 6.10
= ⊥^{ℐ}  Assumption

• The case that ⟦A[a↦X]⟧_{ζ}^{ℐ}·σ = ⊤^{ℐ}. By assumption ζ(X) = ⟦ε([a:ϕ]¬A)⟧_{ζ}^{ℐ}. So suppose ⟦A[a↦X]⟧_{ζ}^{ℐ}·σ = ⊤^{ℐ}. By [mjg lemmas] ⟦A⟧_{ζ}^{ℐ}[a↦ζ(X)]·σ = ⊤^{ℐ}.

[mjg] it must be that there is no x ∈ ⟦ϕ⟧^{ℐ} such that supp(x) ⊆ pmss(X) and ⟦A[a↦X]⟧_{ζ[X↦x]}^{ℐ}·σ = ⊥^{ℐ} By [mjg something] supp(⟦A[a↦X]⟧_{ζ}^{ℐ}) ⊆ fa(A)\{a}. Also σ maps each b ∈ fa(A)\ {a} to something closed, so that [a↦x] ∘ σ = σ ∘ [a↦x·σ]. Therefore [mjg ?] ⟦∀ • [a:ϕ]A⟧_{ζ}^{ℐ}·σ = ⊤^{ℐ}.

[mjg] If z[a↦b] = z′ and b#z then ∀[a]z = ∀[b]z′?

7. [mjg] stuff

[mjg update with ζ] We now come to our first soundness theorem; if a term is typable then its denotation inhabits the denotation of its type:

Theorem 7.1 (First soundness theorem). If Γ ⊢ r : ϕ then ⟦r⟧_{Γ}^{ℐ} ∈ ⟦ϕ⟧_{Γ}^{ℐ}.

As a corollary using condition 5 of Definition 6.1, if Γ ⊢ r : ϕ then supp(⟦r⟧_{Γ}^{ℐ}) ⊆ fa(r).

DRAFT

Proof. By a straightforward induction on the derivation of Γ ⊢ r : ϕ:

• By the definition of model (Definition 6.1), if a : ϕ ∈ Γ then ⟦a⟧_{Γ}^{ℐ} = aϕ^{ℐ} ∈ ⟦ϕ⟧_{Γ}^{ℐ}, and ⟦C⟧_{Γ}^{ℐ} = C^{ℐ} ∈ ⟦type(C)⟧_{Γ}^{ℐ}.

• Suppose Γ, a:ϕ ⊢ r : ψ so that by (L) Γ ⊢ λa:ϕ.r : ϕ→ψ and by inductive hypothesis ⟦r⟧_{Γ,a:ϕ}^{ℐ} ∈ ⟦ψ⟧_{Γ}^{ℐ}. By assumpion ⟦λa:ϕ.r⟧_{Γ}^{ℐ} ∈ ⟦ϕ→ψ⟧_{Γ}^{ℐ}.

• If ⟦r⟧_{Γ}^{ℐ} ∈ ⟦ϕ→ψ⟧_{Γ}^{ℐ} and ⟦s⟧_{Γ}^{ℐ} ∈ ⟦ϕ⟧_{Γ}^{ℐ} then ⟦r⟧_{Γ}^{ℐ} • ⟦s⟧_{Γ}^{ℐ} ∈ ⟦ϕ⟧_{Γ}^{ℐ}.

7.1. Soundness for β-conversion Lemma 7.2. Suppose Γ, a:ϕ ⊢ r : ψ and Γ ⊢ s : ϕ, where a ∉ dom(Γ).

Then ⟦r[a↦s]⟧_{Γ}^{ℐ} = ⟦r⟧_{Γ,a:ϕ}^{ℐ}[a↦⟦s⟧_{Γ}^{ℐ}].

Proof. By a routine induction on the derivation of Γ, a:ϕ ⊢ r : ψ:

• The case of (V) for a. By (Suba) aϕ^{ℐ}[a↦⟦s⟧_{Γ}^{ℐ}] = ⟦s⟧_{Γ}^{ℐ}. Also a[a↦s] = s.

• The case of (V) for c:χ ∈ Γ. By (Sub#) cχ^{ℐ}[a↦⟦s⟧_{Γ}^{ℐ}] = cχ^{ℐ}. Also c[a↦s] = s.

• The case of (L) for λc:χ.r. Using equivariance (Theorem 5.7) suppose c ∉ dom(Γ)∪ supp(⟦s⟧_{Γ}^{ℐ}).^{7} The result follows using (Subλ).

• The case of (A) uses (SubApp).

Proposition 7.3 (The ξ rule). Suppose Γ, a:ϕ ⊢ r : ψ and Γ, a:ϕ ⊢ s : ψ.

If ⟦r⟧_{Γ,a:ϕ}^{ℐ} = ⟦s⟧_{Γ,a:ϕ}^{ℐ} then ⟦λa:ϕ.r⟧_{Γ}^{ℐ} = ⟦λa:ϕ.s⟧_{Γ}^{ℐ}.

Proof. Immediate since by Definition 6.9⟦λa:ϕ.r⟧_{Γ}^{ℐ} = [a:ϕ]⟦r⟧_{Γ,a:ϕ}^{ℐ}, and similarly for s.

Example 7.4. Proposition 7.3 does not hold in a valuation semantics. For instance, consider a (valuation-based) semantics with one base type τ with denotation {0, 1} (a twoelement set). Consider x and y and a valuation ρ mapping x and y both to 0. Then ⟦x⟧_{ρ} = 0 = ⟦y⟧_{ρ} but ⟦λx:τ.x⟧_{ρ} ≠ ⟦λx:τ.y⟧_{ρ}.

Corollary 7.5 (Second soundness theorem). If r =_{β} s (Defn. ??) and Γ ⊢ r : ϕ then ⟦r⟧_{Γ}^{ℐ} = ⟦s⟧_{Γ}^{ℐ}.

Proof. By some routine sets calculations, using Lemma 7.2 and Proposition 7.3.

8. [mjg stuff]

For the rest of this subsection fix a model ℐ.

Let us break down the design of Definition 6.1. Obviously names inhabit the denotation in a very direct and literal sense that aϕ^{ℐ} ∈ ⟦ϕ⟧_{Γ}^{ℐ}. The reader can think of a : ϕ as a constant which must be interpreted ‘as itself’ by aϕ^{ℐ}.

But aϕ^{ℐ} also behaves like a variable: It can be renamed by π·x, and bound by [a:ϕ]x, and it can also be substituted for. The rules (Suba) to (Subλ) do the job that valuations do in ‘normal’ models; they replace a name aϕ^{ℐ} by an(other) element of the model. The significant difference is that in standard models we pick a valuation and then form a

7In fact by Theorem 7.1 c ∉ supp(⟦s⟧_{Γ}^{ℐ}) follows from c ∉ dom(Γ). But that does not matter; we can just rename c ‘fresh’, without having to engage in detailed calculations about how fresh it is.

DRAFT

denotation; in nominal models we form a denotation and then—if we wish—substitute for the free variables.

The axioms (Suba) to (SubId) can be made formal in nominal algebra [? ]. These particular axioms are taken from [? ].^{8} Instead of (Sub#) we could take a weaker axiom b[a↦x] = b. Conversely, we could safely add (SubId) and thus exclude certain arguably pathological models. The language of Definition ?? is not expressive enough to detect these choices, but the language of Definition ??is (see Example ??).

Aside from the inclusion of names, our notion of model resembles Henkin models, which have an applicative structure in which abstractions have a well-defined interpretation [? ].

Just as is the case for Henkin models, Definition 6.1 specifies what a model must look like but does not build one. We do build a concrete model out of syntax as part of the completeness proof in Subsection ??.

The equivariance conditions are standard for nominal techniques; our models must be symmetric up to permuting atoms.

Finally, conditions 1 to 6 specify the structure of a model that makes it into a model of the λ-calculus, by interpreting names (as themselves), constants, λ-abstraction (as a function of the name a and the element x)^{9} and a Henkin-models style application.

8(Suba) to (SubId) soundly and completely characterise the syntactic model of substitution. In this paper we are also interested in non-syntactic models, so weaker axioms—and thus more models—are reasonable.

We chose the axioms above because they are closed, in the sense of [? ? ], which gives better computational properties (if we ever design an abstract machine using this semantics).

9So [a:ϕ]x need not be precisely equal to the Gabbay-Pitts atoms-abstraction [a]x from [? ].