Many-Sorted First Order Logic with Equality (FOL) II : Syntax

Posted on August 3, 2016August 4, 2016 by berenbeim

Continuing where we have left off, we have an acceptable signature category whose objects are triples $\Sigma = (S,F,P)$ and whose morphisms are $\varphi=(\varphi^{st},\varphi^{op},\varphi^{rl})$ . We now make the step from (potentially vacuous) symbols to syntactically well-formed strings of symbols.

Classical Model Theoretic Approach To Syntax

First, we will rather informally describe a kernel signature consisting of the classical logical symbols:

a countably infinite set $V$ of logical variables $v_i$ , and parentheses (,) ;
four binary operations $\land, \lor, \rightarrow$ and $\leftrightarrow$ which we’ll always interpret as and, or, implies, and if and only if respectively;
one unary relation $\lnot$ , which we will always interpret as the Boolean connective of strong negation and a binary relation symbol = denoting equality
the quantifiers $\forall, \exists$ (read as “for all” and “exists” respectively)

Furthermore, for arbitrary P,Q and formula $\varphi (v)$ with free variable v, the following identities hold

$\lnot\lnot P \equiv P$
$( P\land Q ) \equiv \lnot ( \lnot P \lor \lnot Q )$
$( P \rightarrow Q ) \equiv ( \lnot P \lor Q )$
$( P \leftrightarrow Q) \equiv ((P\rightarrow Q) \land (Q\rightarrow P))$
$\forall v \varphi(v) \equiv \lnot \exists v \lnot \varphi(v)$

With these identities, we see that it we can fully recover classical logic with $\lnot, \lor$ and classical first order logic if we use $\exists$ or $\forall$ (there are other alternative choices, but classical strong negation and disjunction and a single quantifier will suffice when engaged in proofs on the induction of formula complexity in the next post).

Some readers should already be raising questions about this description — there will be a future post exploring the proof system of first order logic in which these relationships will be properly explained. For now, the reader should take as a given that all first order languages studied in classic model theory will contain this signature with the rules given above combined with the other signatures introduced in the last post; first order languages are in one-to-one correspondences with the signatures given last time modulo the kernel signature above.

In the traditional model theoretic approach to $\mathbf{FOL}$ we inductively construct sentences from formula, formula from atomic formula, and atomic formula from terms.

For instance, in a singly sorted first order model theory, this inductive process is handled as follows:

Now, we will start with an arbitrary language $\mathcal{L}=(\mathcal{F},\mathcal{P},v)$ which we may equivalently consider to be the triple $(\mathcal{F},\mathcal{R},\mathcal{C})$ , where $\mathcal{C}$ is a set of constant symbols, $\mathcal{R}$ is the same thing as P (i.e. a set of relation symbols) such that for all $R\in \mathcal{R}$ there is a positive integer $n_R$ denoting the arity of the relation symbol R,and $\mathcal{F}$ is the set of function symbols such that each $f\in \mathcal{F}$ has a positive integer $n_f$ denoting its arity.

Given $\mathcal{L}$ , we inductively form $\mathcal{T}$ as the smallest set such that

for all $c\in \mathcal{C}$ , $c\in \mathcal{T}$ ;
for each $v_i\in V, v_i\in \mathcal{T}$ ;
if $t_1,\hdots, t_{n_f}\in \mathcal{T}$ and $f\in \mathcal{F}$ , then $f(t_1,\hdots, t_{n_f})\in \mathcal{T}$ .

Notice that necessarily the set of terms has cardinality $\ge \aleph_0$ given that we are assuming a countably infinite number of logical variable symbols as terms in our arbitrary language (even one where $\mathcal{L}$ is empty save for the kernel of logical symbols).

Now that we have our set of terms, we define the set of atomic formula $\mathcal{A}$ over $\mathcal{T}$ as the set consisting of:

$(t_1=t_2)\in \mathcal{A}$ where $t_1, t_2\in \mathcal{T}$ ;
for $R\in \mathcal{R}$ and $t_1,\hdots, t_{n_R}\in \mathcal{T}$ , $R(t_1,\hdots, t_{n_R})\in \mathcal{A}$ .

Then, given $\mathcal{A}$ , we define the set of $\mathcal{L}$ -formula $\mathcal{W}$ to be the smallest set containing $\mathcal{A}$ such that

if $\phi \in \mathcal{W}$ then $\lnot \phi\in \mathcal{W}$ ;
if $\phi,\psi$ are formula in $\mathcal{W}$ , then $(\phi\land \psi)$ and $(\phi\lor \psi)$ are in $\mathcal{W}$ ;
if $\phi \in \mathcal{W}$ , then $\exists v_i \phi$ and $\forall v_i \phi$ are in $\mathcal{W}$ .

Finally, given $\mathcal{W}$ , we define a sentence to be some formula $\phi$ such that every logical variable appearing in $\phi$ is bound by a quantifier. For instance, given $\phi_1 := \forall v_0(v_0= v_1)$ and $\phi_2:= \forall v_0\exists v_1(v_0=v_1)$ , we would say that $\phi_1$ is a formula with a free variable $v_1$ , while $\phi_2$ is a sentence, as both logical variables are bound.

It is crucial to note that so far we’ve only described how to construct syntactically well-formed statements. The truth of these statements thus far is that we can say they are elements in the sets $\mathcal{T}, \mathcal{A},\mathcal{V}$ , and not that the statements that they express are true-in-themselves.

The Functorial Approach To The Syntax of FOL

Now, we switch our focus back to the institution theoretic point of view.

First, recall that we in order to have an institution, we must have a covariant functor $\mathtt{Sen}:\textsc{Sig}\to \textsc{Set}$ . An arbitrary functor $\mathtt{F}:\textsc{C}\to\textsc{D}$ is a map between categories $\textsc{C},\textsc{D}$ consisting of

$|\mathtt{F}|: |\textsc{C}|\to |\textsc{D}|$ ;
for all , such that
1. $\mathtt{F}(1_X)=1_{\mathtt{F}(X)}$ ;
2. $\mathtt{F}(g\circ f)= \mathtt{F}(g)\circ \mathtt{F}(f)$

So what we must now do is define such a map $\mathtt{Sen}$ . Given our syntactical category of signatures $\Sigma=(S,F,P)$ , we want to first take $\Sigma$ to a set whose elements will be called the sentences over the signature.

Towards that end, given an arbitrary signature $\Sigma$ , we first define the set of $F$ -terms $T_F$ inductively over the words from $S^*$ using the operation symbols $\sigma \in F_{s_1\hdots s_n\to s}$ and F-terms $t_1,\hdots, t_n$ of sorts $s_1, \hdots s_n$ to form an F-term $t:= \sigma(t_1,\hdots, t_n)$ of sort $s$ . We denote by $(T_F)_s$ the subset of terms of sort $s$ and by $(T_F)_w$ , where $w= s_1s_2\hdots s_n$ , the cartesian product of terms $(T_F)_{s_1}\times (T_F)_{s_2}\times \cdots \times (T_F)_{s_n}$ .

We now define the set of atoms $A_P$ as the set consisting of

equations $(t = t^\prime)$ for F-terms $t,t^\prime$ of the same sort $s$ , ;
relational atoms $\pi(t_1,\hdots, t_n)$ formed from $\pi \in P_w$ and $(t_1,\hdots, t_n)\in (T_F)_w$ .

Finally, we define the set of $\Sigma$ -sentences $W_\Sigma$ as the least set containing the (quantifier-free) atoms that is closed under Boolean connectives and quantification, i.e. $W_\Sigma\supset A_P$ such that

For $\rho_1,\rho_2\in W_\Sigma$ , $(\rho_1\land \rho_2), (\rho_2\lor \rho_2),(\lnot \rho_i), (\rho_i\rightarrow \rho_j), (\rho_i\leftrightarrow \rho_j)\in W_\Sigma$ ;
For arbitrary quantifier $Q$, and any finite set $X$ of variables of sort S, with variable x of sort s denoted by $x : s$ , can be added to $\Sigma$ as new constants such that the $\Sigma=(S,F,P)$ sentence $Qx(\rho)$ for all $\Sigma^\prime =(S, F\coprod X,P)$ -sentences $\rho$ ; that is $Qx(\rho)\in W_\Sigma$ .

We see that for any arbitrary signature, we have that $|\mathtt{Sen}(\Sigma)|=W_\Sigma\in |\textsc{Sets}|$ .

We now turn our attention to defining this functor with respect to the morphisms of $\textsc{Sig}$ by inductively defining $\mathtt{Sen}(\varphi):\mathtt{Sen}(\Sigma)\to\mathtt{Sen}(\Sigma^\prime)$ on the structures of sentences. Each $\mathtt{Sen}_{\Sigma,\Sigma^\prime}$ is called a sentence translation, and the induction occurs by applying $\varphi$ to replace the symbols of $\Sigma$ with the symbols of $\Sigma^\prime$ as follows:

For terms, we have a function $\varphi^{tm}\in \textsc{Sets}(T_F,T_{F^\prime})$ by $\varphi^{tm}(\sigma(t_1,\hdots, t_n))=\varphi^{op}(\sigma)(\varphi^{tm}(t_1),\hdots, \varphi^{tm}(t_n))$
$(\mathtt{Sen}(\varphi))(t=t^\prime)= (\varphi^{tm}(t)=\varphi^{tm}(t^\prime))$ ;
$(\mathtt{Sen}(\varphi))(\pi(t_1,\hdots,t_n))=(\varphi^{rl}(\pi))(\varphi^{tm}(t_1),\hdots,\varphi^{tm}(t_n))$ ;
for Boolean connectives $C$ , $(\mathtt{Sen}(\varphi))(C(\rho_1,\rho_2))=C( (\mathtt{Sen}(\varphi))(\rho_1),(\mathtt{Sen}(\varphi)) (\rho_2))$ –in the case of negation, we just use $\rho_1$ ;
For all finite sets X of variables of sort s, and all $(S,F\coprod X, P)$ -sentences $\rho$ , $(\mathtt{Sen}(\varphi))(\forall X(\rho))=\forall X^\varphi (\mathtt{Sen}(\varphi^\prime(\rho))$ –where we denote by $X^\varphi:=\{(x: \varphi^{st}(s)\mid (x: s)\in X\}$ and the canonical extension of $\varphi$ denoted by $\varphi^\prime: (S,F\coprod X,P)\to (S^\prime, F^\prime\coprod X^\varphi,P^\prime).$

The readers of this blog are encouraged to check that this indeed is just set-valued function from $W_\Sigma$ to $W_{\Sigma^\prime}$ . We see that this satisfies the definition of a functor as

$\mathtt{Sen}(1_\Sigma)=1_{W_\Sigma}=1_{\mathtt{Sen}(\Sigma)}$ ;
With $\varphi; \varphi^\prime$ denoting the application of the signature map $\varphi:\Sigma\to \Sigma^\prime$ then the application of the signature map $\varphi^\prime:\Sigma^\prime \to \Sigma^{\prime\prime}$ . We finally prove this is a functor by induction on arbitrary sentences $\rho\in W_\Sigma$ . So that $(\mathtt{Sen}(\varphi; \varphi\prime))(\rho) = (\mathtt{Sen}(\varphi^prime))\circ (\mathtt{Sen}(\varphi))(\rho)$ at the level of sets.

In the latter case, we start the induction first on terms, noting that $(\varphi^{\prime}\circ \varphi^{tm})(\sigma(t_1,\hdots, t_n))=((\varphi^{\prime,op}\circ\varphi^{op})(\sigma))((\varphi^{\prime,tm}\circ \varphi^{tm})(t_1),\hdots,(\varphi^{\prime,tm}\circ \varphi^{tm})(t_n))$ . We then start induction on sentences proper by noting in the case of equality, $(\mathtt{Sen}(\varphi;\varphi^\prime))(t=t^\prime)=(\varphi^{\prime,tm}\circ\varphi^{tm}(t)=\varphi^{\prime,tm}\circ\varphi^{tm}(t))$ . We then proceed to our relational atoms, Boolean connectives and quantification in a like manner.

Many-sorted First Order Logic with Equality (FOL) I : Signatures

Posted on August 2, 2016August 3, 2016 by berenbeim

For a mathematics blog whose raison d’être is the exploration of institution theory, we should hope that the logic we’ve come to associate with mathematics is expressible as an institution. Luckily, it is (as we shall see in the next series of posts).

First, recall that an institution $\mathcal{I}$ is a tuple $\langle\textsc{Sig}^I, \mathtt{Sen}^I, \mathtt{Mod}^I,\models^I \rangle$ .

In order to verify that $\mathbf{FOL}$ forms an institution, we will need to make sure that a tuple which one would recognize as the classical formulation of First-order logic exists. We will organize the next few posts around the four S's:

Signatures
Syntax
Semantics
Satisfaction

Signatures

For the rest of this post, we will examine Signatures by first constructing an appropriate signature category $\textsc{Sig}$ , and then we will compare this notion of signature to the notion of first order signatures one can find in Chang-Keisler or Marker.

Recall that from one pov a 1-category $\textsc{C}$ consists of the following:

a class of objects that we will heretofore denote by $|\textsc{C}|$ — although one commonly finds this denoted by $\mbox{ob } \textsc{C}$ in the literature;
for all $X,Y\in |\textsc{C}|$ , a class of arrows (or morphisms) denoted by $\textsc{C}(X,Y)$ — although one commonly finds this class in the literature denoted by $\mbox{Hom}_{\textsc{C}}(X,Y)$ ;
for all , a binary operation such that:
1. $\exists 1_X\in \textsc{C}(X,X)$ such that for any $f\in \textsc{C}(X,Y), g\in \textsc{C}(Z,X)$ , $1_x\circ g=g$ and $f\circ 1_X=f$ i.e. every object of $X$ is in a 1-1 correspondence with an identity arrow on X;
2. for all $f\in \textsc{C}(X,Y)$ and $g\in\textsc{C}(Y,Z), g\circ f \in \textsc{C}(X,Z)$

(At times we will find it more sensible to denote composition of two arrows by $f; g$ in lieu of the more common mathematical right-to-left notation of composition so that we can think of f being applied first, then g– in this case, we’re thinking of ; composition as $;: \textsc{C}(X,Y)\to(\textsc{C}(Y,Z)\to \textsc{C}(X,Z))$ .)

We will take for granted the existence of the category of sets, $\textsc{Sets}$ , for the time being (posts are planned on alternate and more general definitions of category with an eye towards foundations). We now define a category $\textsc{Sig}$ whose objects are triples $\Sigma=(S,F,P)$ where:

$S$ is a (possibly empty) set of sort symbols;
$F:=\{F_{w\to s}\mid w\in S^*, s\in S\}$ is a family of (possibly empty) sets of S-sorted operation symbols, where $F_{w\to s}$ denotes the set of operations of w-arity and sort s. For example, $F_{\to s}$ denotes the set of constants of sort s, while $F_{sss\to s}$ is the set of operations $s\times s\times s\to s$ ;
$P:=\{P_w\mid w\in S^*\}$ is a family of (possibly empty) sets of S-sorted relation symbols where $P_w$ denotes the set of relations of w-arity

(Notice that in the Kleene closure of the set of sorts S, we have an empty word, and so we very well might have a non-empty set of relations with empty arity. Can you think of a non-sorted set? Any one will do.)

Now we need to make sure we have a definition of a signature morphism $\varphi\in \textsc{Sig}( \Sigma,\Sigma^\prime)$ which satisfies the axioms of category theory. Towards that end we define $\varphi\in\textsc{Sig}^I((S,F,P),(S^\prime,F^\prime,P^\prime))$ to be a triple $(\varphi^{st},\varphi^{op}, \varphi^{rl})$ consisting of the following maps:

a function $\varphi^{st}\in \textsc{Sets}(S, S^\prime)$ ;
a family of functions $\varphi^{op}:=\{\varphi^{op}_{w\to s}\in \textsc{Sets}(F_{w\to s}, F^\prime_{\varphi^{st}(w)\to \varphi^{st}(w^\prime)})| w\in S^*,s\in S\}$ , which consists of functions between the sets of operation symbols;
a family of functions $\varphi^{rl}:=\{ \varphi^{rl}_w\in\textsc{Sets}( P_w, P^\prime_{\varphi^{st}(w)}) | s\in S^* \}$ consisting of functions between the sets of relation symbols.

Given that we have identity maps in the category of sets, we find that we have identity maps between each signature by the existence of the identity map $1_S\in \textsc{Sets}(S,S)$ and the existence of identity maps between the families of functions $\varphi^{op}$ and $\varphi^{rl}$ . Similarly, we find that $\varphi^{op};\psi^{op}=\{(\psi\circ\varphi)_{w\to s}^{op}\in\textsc{Sets}(F_{w\to s},F^{\prime\prime}_{\psi^{st}(\varphi^{st}(w)\to \psi^{st}(\varphi^{st}(s))})\}_{S^*\times S}$ , and $\varphi^{rl};\psi^{rl}=\{ (\psi\circ\varphi)^{rl}_w\in \textsc{Sets}(P_w,P_{\varphi^{st}(\psi^{st}(w))}^{\prime\prime} ) \}_{S^*}$ .

In the classical approach to many-sorted first order logic, the signature $\Sigma$ fixes an alphabet of non-logical symbols. That is, a classical signature is simply meant to capture some temporary placeholder for an idea that is to be elaborated upon later– the elements in the signature have no intrinsic meaning. They’re simply there.

So it is no wonder that a many-sorted signature is simply the tuple $\Sigma=(S, F, P, v)$ where $S$ denotes the set of sorts symbols, $F$ denotes a set of function symbols, $P$ denotes the set of predicate symbols, and $v$ is a function assigning our function, predicate, and variable symbols to the appropriate string of sort symbols in $S^*$ . So, for instance, a function symbol $f$ in a two-sorted logic (say the sorts are string and int denoted s and i) is identified as a binary operation when $v(f)$ is a word of length 3 with characters consisting of the two sort symbols, say $latex v(f)=iss$, which we then read as

operation “f” takes a pair belonging to int * string to string

while for any n-ary predicate $U$ , $v(U)$ is assigned to a word of length $n$ , so a binary relation symbol like $\le$ is one that is defined by $v(\le)$ being assigned sort ii or ss (or is or si in our two sorted example since the symbol $\le$ need not have the standard meaning we commonly assign it). We recover our notion of constants by letting $v(f)$ be a single sorted value, as before.

Readers still uncertain about the equivalence of these two formulations of abstract signatures are encouraged to try and recover the latter definition from the institution-theoretic definition (hint: the sorting function v does much of the heavy lifting).

Recovering single-sorted first order logic ( $\mathbf{FOL}^1$ ) and propositional logic ( $\mathbf{PL}$ )

While the notion of sub-institution will have to wait for a future post, one can define an institution of (single-sorted) first order logic by considering the subcategory of signature categories where $S$ is a singleton. In this case, the name of the sort simply does not matter, as different choices of S will give rise to isomorphic institutions, and so we may denote the objects of this category as pairs (F,P), where F and P retain their earlier definitions.

Notice that because our choice of singleton sort set S does not matter, the arities of functions and predicate symbols becomesidentified with natural numbers instead of words. It is in this setting that one finds classical model theory, and thus, much of mathematics.

Finally, we recover traditional propositional logic by restricting our attention to the signatures with an empty set of sort symbols, so that signatures only consists of sets (of zero arity relation symbols), whence the signature category is simply the category of sets itself!

What Do I Mean By Real Clear Ideas?

Posted on July 9, 2016August 3, 2016 by berenbeim

Motivations For This Blog

I would be unscrupulous if I were to obscure some of my motivations for this blog and its organization and presentation. While I had intended to inaugurate this blog with a lengthy post giving a brief genealogy of the concept of clear and distinct ideas covering the various problems with what we might expect from any theory of knowledge, I am also loathe to post extremely lengthy posts covering philosophical history on what is primarily intended to be a blog exploring real-world applications of formal logic. Indeed, discussing how Very Smart People over the centuries have misapprehended what mathematics is does little to actually give any reader a real clear idea of what this blog is about, let alone of what a real clear idea ought to look like in practice.

Why This Blog

So the overrarching motivation for this blog is derived from following question:

Given arbitrary requirements & specifications, is there a formal basis for systematically developing correct programs with verified refinement steps?

While this is the point of formal specification theory in computer science, I believe it is not too hard to rework this question so it can comfortably be asked by anyone (philosophers included!):

How can I defeasibly verify the(formal) intelligibility of what I want a computer to do?

While this is not a great account of formal specification theory, as it does not begin to describe the immense challenges faced by software engineers (let alone the uncountable quibbles of philosophers), it is an informal description that I can conceive of at this time which touches upon the notion of real clear ideas.

Without further circumlocution, I’d like to posit that a real clear idea is a fragment of natural language (idea) that is formally intelligible (clear), and one for which there is at least one consistent program (real). Of course, what is meant by fragment of natural language, formally intelligible, and consistent program has also left unstated; it is the goal of this blog to provide abductive accounts of these notions.

So while these descriptions may not be sufficient for “truly understanding” what Descartes, Leibniz, et al. may have meant when they were writing about ideas, I’d like to encourage readers of this blog (particularly those who really only will be reading any future posts principally concerned with intellectual history) to maintain some principle of charity with my presentation style; please try to keep in mind the broader historical contexts that I am trying to invoke.

How RCI Will Be Organized and Presented

This blog will primarily be broken down into the following three topics: Applications, Foundations, and Observations. Applications will ideally be broken down into two subjects: actual programs and pure mathematics. Foundations has three subjects (which are really interdefinable): the subjects are the Category theory, Set theory, and Type theory necessary for a theory of computation. Finally, Observations will consist of commentary on subjects distinct from the previous two topics; many of these observations will be philosophical, although I’ll gladly take requests.

How To Begin Approaching Real Clear Ideas: Institution Theory

While I intend to cover the development of Institution theory by Burstall and Goguen elsewhere, a very brief introduction is in order:

An institution $\mathcal{I}$ is the tuple $I:=\langle \textsc{Sig}^I, \mathtt{Sen}^I, \mathtt{Mod}^I,\models^I \rangle$ where:

$\textsc{Sig}^I$ is category whose objects are referred to as signatures;
$\mathtt{Sen}^I: \textsc{Sig}^I\to \textsc{Sets}$ is a covariant functor such that every signature $\Sigma$ is taken to a set whose elements are referred to as sentences over signature $\Sigma$ ;
$\mathtt{Mod}^I: (\textsc{Sig}^I)^{op} \to \textsc{Cat}$ is a contravariant functor taking signatures $\Sigma$ to a category $\textsc{C}_\Sigma$ whose objects are called $\Sigma$ –models and whose arrows are $\Sigma$ -(model) homomorphisms;
$\models^I$ is a family of relations $\models_\Sigma\subseteq |\mathtt{Mod}^I(\Sigma)|\times \mathtt{Sen}^I(\Sigma)$ indexed by $|\mathtt{Sig}^I|$ such that for each $\varphi\in \textsc{Sig}^I(\Sigma,\Sigma^\prime), s \in \mathtt{Sen}^I(\Sigma), \& M^\prime\in |\mathtt{Mod}^I(\Sigma^\prime)|$

$\mathtt{Mod}^I(\varphi)(M^\prime)\models_\Sigma s \equiv M^\prime\models_{\Sigma^\prime} \mathtt{Sen}^I(\varphi)(s)$

We refer to this last condition as the satisfaction condition, with the relation $\models_\Sigma$ being referred to as $\Sigma$ –satisfaction. For those familiar with Tarski’s semantic definition of Truth, the punchline of this satisfaction condition is that (semantic) Truth is invariant under changes of notation and extension of context.