Glossary

Glossary Definitions

Hover over bold terms to see their definitions.

Standard Language

A ***standard language*** $L$ is an austere first-order language consisting of:

• a (finite) vocabulary of primitive **predicates**,
• variables ranging over the domain,
• logical connectives ($\neg$, $\land$, $\lor$, $\to$, $\leftrightarrow$), quantifiers ($\forall$, $\exists$), and the identity **predicate** ($=$),
• interpreted objectually, with no individual constants or function symbols,
• a fixed axiomatization of classical first-order logic and the specific axioms of the theory regimented in $L$.

All notions of ***sentence***, ***proof***, ***theorem***, ***predicate***, ***equality predicate***, ***sentence isomorphism***, ***place***, ***role***, ***Pip***, ***Rip***, ***Qip***, and ***Qisl*** are relativized to a given **standard language** $L$.

Sentence

A ***sentence*** of a **standard language** $L$ is built inductively as follows:

• any primitive atomic formula of $L$ is a **sentence**;
• if $S$ is a **sentence**, then $\lnot S$ is a **sentence**;
• if $S$ and $T$ are **sentences**, then $(S \land T)$ is a **sentence**;
• if $S$ is a **sentence** and $x$ is a variable of $L$, then $\forall x\,S$ is a **sentence**.

Open Sentence

An ***open sentence*** of $L$ is a **sentence** that contains at least one free variable.

Closed Sentence

A ***closed sentence*** of $L$ is a **sentence** with no free variables. Given an **open sentence** $S$ with free variables $x_1,\dots,x_n$, its *closure* is $$ \forall S \;:=\; \forall x_1 \cdots \forall x_n\, S, $$ which is a **closed sentence**.

Proof

A ***proof*** in $L$ is a finite sequence of **sentences** $$ S_1, S_2, \dots, S_n $$ such that each $S_i$ is one of:

1. an axiom of $L$ or of the underlying logic;
2. of the form $\forall x\,S_j$ for some $j < i$ (*universal generalization*);
3. a **sentence** $T$ for which there is some $j < i$ and some **sentence** $S$ among $S_1,\dots,S_{i-1}$ such that $(S \Rightarrow T)$ also occurs among $S_1,\dots,S_{i-1}$ (*modus ponens*).

Theorem

A ***theorem*** of $L$ is a **sentence** that appears as the last member of some **proof** in $L$.

Sentence Equivalence

Two **sentences** $S$ and $T$ of $L$ are in ***sentence equivalence*** when the **closed sentence** $$ S \Leftrightarrow T $$ is a **theorem** of $L$.

Logical Equivalence

***Logical equivalence*** is the equivalence relation on **sentences** generated by **sentence equivalence**: $$ S \text{ and } T \text{ are logically equivalent} \quad\text{iff}\quad S \Leftrightarrow T \text{ is a theorem}. $$ In particular, **sentence equivalence** and **logical equivalence** coincide for **closed sentences**.

Sentence Isomorphism

Let $S$ and $T$ be **open sentences** of $L$. A ***sentence isomorphism*** from $T$ to $S$ is a one-to-one renaming of the free variables of $T$ by the free variables of $S$ that produces a new **sentence** $T'$ such that $$ S \Leftrightarrow T' $$ is a **theorem** of $L$. In this case we say that $S$ and $T$ are *isomorphic* **sentences**.

Isomorphism

Unless otherwise specified, ***isomorphism*** between **open sentences** means **sentence isomorphism**. **Isomorphism** between other objects (such as **places**) is always defined in terms of **sentence isomorphism**.

Place

A ***place*** is an ordered pair $$ \langle S, x\rangle $$ where $S$ is an **open sentence** of $L$ and $x$ is a free variable of $S$.

Place Isomorphism

Two **places** $$ \langle S, x\rangle,\qquad \langle T, y\rangle $$ are ***isomorphic places*** if there is a **sentence isomorphism** from $T$ to $S$ that sends the free variable $y$ to $x$.

Isomorphic Places

***Isomorphic places*** are **places** related by **place isomorphism**; this forms an equivalence relation on **places**.

Role

A ***role*** is an **isomorphism** class of **places** under **place isomorphism**. Equivalently, $$ \mathrm{Role}(S,x) $$ denotes the equivalence class of all **places** isomorphic to $\langle S,x\rangle$.

Predicate

A ***predicate*** of $L$ is an equivalence class of **open sentences** under **sentence isomorphism**. For any **open sentence** $S$, the **predicate** it represents is written $$ \mathrm{Pred}(S). $$

Equality Predicate

An ***equality predicate*** $E$ of $L$ is a binary **predicate** (i.e.\ a **predicate** represented by some **open sentence** $E(x,y)$ in two free variables) whose associated **open sentences** satisfy:

1. reflexivity: $\forall x\,E(x,x)$ is a **theorem**;
2. symmetry: $\forall x,y\,(E(x,y)\Rightarrow E(y,x))$ is a **theorem**;
3. transitivity: $\forall x,y,z\,((E(x,y)\land E(y,z))\Rightarrow E(x,z))$ is a **theorem**;
4. substitutivity: whenever $S$ and $S'$ are **sentences** that differ only by replacing a free occurrence of $x$ by $y$, then $$ \forall x,y\,(E(x,y)\Rightarrow (S \Leftrightarrow S')) $$ is a **theorem**.

We identify $E$ with its equivalence class of **open sentences** under **sentence isomorphism** and write $E(x=y)$ for the simple equality **sentence** asserting $E$ of $x$ and $y$.

Conjunction of Equalities

Given **equality predicates** $E$ and $F$ of $L$, their ***conjunction of equalities*** is the **predicate** $$ EF := \mathrm{Pred}\bigl(E(x=y)\land F(x=y)\bigr). $$ The simple equality **sentences** of $EF$ are written $EF(x=y)$ and are regarded as primitive (``simple in $EF$'') in **place** of the compound **sentence** $E(x=y)\land F(x=y)$.

Equality Logic

***Equality logic*** is the algebra of **equality predicates** of $L$ under:

• the binary operation of **conjunction of equalities** $(E,F)\mapsto EF$;
• the identity relation $E = F$ of **equality predicates** (i.e.\ **sentence**-**isomorphism** of their simple equality **sentences**).

Refinement

Let $E$ and $F$ be **equality predicates** of $L$. The ***refinement*** relation $$ E \Rightarrow F $$ (read: ``$E$ refines $F$'') is defined by $$ E \Rightarrow F \quad\text{iff}\quad EF = E $$ as **equality predicates**. Equivalently, using **sentence equivalence**: $$ E \Rightarrow F \quad\Longleftrightarrow\quad \forall x,y\,( E(x=y) \Rightarrow F(x=y) ) $$ is a **theorem** of $L$. In this sense, $E$ is a *finer* identity than $F$.

Pip

Let $S$ be an **open sentence** of $L$ with free variables $x,y,z,\dots$. Let $w$ be a new variable not occurring in $S$, and let $S'$ be the **open sentence** obtained from $S$ by replacing all free occurrences of $x$ by $w$. Define the **sentence** $$ E(x=w) \;:=\; \forall y,z,\dots\, (S \Leftrightarrow S'). $$ The ***place** identity **predicate*** of $x$ in $S$ is the **equality predicate** $$ \mathrm{Pip}(x) := \mathrm{Pred}\bigl(E(x=w)\bigr). $$

Rip

Let $r$ be a **role**, i.e.\ an **isomorphism** class of **places**. Choose any **place** $\langle S,x\rangle$ whose **role** is $r$. The ***role** identity **predicate*** of $r$ is defined as $$ \mathrm{Rip}(r) := \mathrm{Pip}(x) $$ for any representative $\langle S,x\rangle$ of $r$. This is well-defined because **isomorphic places** yield the same **place** identity **predicate**.

Qip

Let $P$ be a **predicate** of $L$ and let $\{r_1,\dots,r_n\}$ be the set of **roles** of $P$. The *Quine identity **predicate*** of $P$ is the **equality predicate** $$ \mathrm{Qip}(P) := \mathrm{Rip}(r_1)\,\mathrm{Rip}(r_2)\cdots \mathrm{Rip}(r_n), $$ i.e.\ the conjunction of all **role** identity **predicates** for the **roles** of $P$.

Qisl

Let $L$ be a **standard language** and let $\{P_1,\dots,P_m\}$ be the **predicates** of $L$. The *Quine identity of $L$* is the **equality predicate** $$ \mathrm{Qisl}(L) := \mathrm{Qip}(P_1)\,\mathrm{Qip}(P_2)\cdots \mathrm{Qip}(P_m), $$ i.e.\ the conjunction of all Quine identity **predicates** of the **predicates** of $L$.

Cardinality

Let $E$ be an **equality predicate** of $L$. To say that the ***cardinality*** of $E$ is $n$ means that the following two **sentences** are **theorems** of $L$:

1. There exist $n$ pairwise $E$-unequal entities: $$ \exists x_1,\dots,x_n.\;\bigwedge_{1\le iAmong any $n+1$ entities, at least two are $E$-equal: $$ \forall x_1,\dots,x_{n+1}.\;\bigvee_{1\le i If such an $n$ exists, $E$ is *finite*; otherwise $E$ is *infinite*.

Presentation

A ***presentation*** is a **standard language** $L$ considered together with its Quine identity $\mathrm{Qisl}(L)$ and its position among other **standard languages** $L'$ whose Quine identities $\mathrm{Qisl}(L')$ may or may not share a common **refinement** with $\mathrm{Qisl}(L)$. **Presentations** are related via the **refinement** relation between their associated **equality predicates**.

Local Language

A ***local language*** can thus be viewed both syntactically (as a system of **sentences**, **predicates**, and **proofs**) and structurally (via its Quine identity $\mathrm{Qisl}(L)$ and the **presentations** it participates in).

Relative Identity

Let $L$ be a **local language** and let $x$ be an element that acts as a *discriminator* in some **presentation** of $L$. A ***relative identity*** for $x$ is an **equality predicate** $$ E_x(y=z) $$ of $L$ such that:

• $E_x$ is an **equality predicate** in the sense above;
• $E_x$ is determined by the **roles** and co-**roles** of $y$ and $z$ in the relations of $L$ selected or induced by $x$;
• the identity of $y$ and $z$ is always read ``relative to $x$'', written $x(y=z)$.

Thus ***relative identity*** is identity defined not absolutely, but via the Quine-type construction restricted to the **predicates** and **presentations** determined by a particular discriminator $x$.