Sorted logic

Syntax of sorted logic

Let %$S$% be a set of sorts. Instead of one set of variables, we have one set for each sort. Each constant symbol has a sort. Instead of having a number %$n$% of places, each predicate symbol has a list %$s_{1},\dotsc ,s_n$% of sorts. The first two clauses in the definition of a formula become

1. A variable or a constant symbol followed by = followed by a variable or a constant symbol is a formula if the variable or constant symbol on the left is of the same sort as that of the variable or constant symbol on the right.
2. A relation symbol from %$\mathcal L$% followed by a list of variables and constant symbols from %$\mathcal L$% such that the %$i$%th item on the list is of the %$i$%th sort in the list of sorts associated with the relation symbol is a formula.

Semantics of sorted logic

A structure now has one nonempty domain for each sort such that all the domains are disjoint, and each constant and relation symbol must be of the appropriate (list of) sorts. An assignment must assign an object in the domain of sort %$s$% to each variable of sort %$s$%.The quantifier clauses in the definition of satisfaction now read:

If %$\phi$% is %$(\forall\nu\psi)$%, where %$\nu$% is of sort %$s$%, then %$\mathfrak{A}\vDash\phi [s]$% if for every assignment %$r$% that agrees with %$s$% on every variable other than %$\nu$%, %$\mathfrak{A}\vDash\psi [r]$%, or, equivalently, if for every %$a$% in %$A_{s}$%, the domain of sort %$s$%, %$\mathfrak{A}\vDash\psi [s(\nu /a)]$%.

If %$\phi$% is %$(\exists\nu\psi)$%, where %$\nu$% is of sort %$s$%, then %$\mathfrak{A}\vDash\phi [s]$% if there is an assignment %$r$% that agrees with %$s$% on every variable other than %$\nu$% such that %$\mathfrak{A}\vDash\psi [r]$%, or, equivalently, if for there is an %$a$% in %$A_s$%, the domain of sort %$s$%, such that %$\mathfrak{A}\vDash\psi [s(\nu /a)]$%.

Sorting out sorted logic

If %$\mathfrak A$% is a sorted structure, let %$\mathfrak{A}^{*}$% be the unsorted structure with domain the union of the domains of %$\mathfrak A$% and with a new predicate symbol %$P_s$% in the language for each sort of %$\mathfrak A$%. Let * be a function that takes each sorted variable, constant symbol, or relation symbol to a distinct unsorted one. In addition, make * be such that every unsorted variable is the * of some sorted variable. If %$s$% is an assignment for %$\mathfrak A$%, let %$s ^{*}$% be the assignment for %$\mathfrak{A}^{-}$% that assigns %$\nu ^{*}$% %$a$% if %$s(\nu)=a$%.

If %$\theta$% is a formula in the language of %$\mathfrak A$%, define a formula %$\theta^*$% in the language of %$\mathfrak{A}^{-}$% as follows:

1. If %$\theta$% is %$s=t$%, then %$\theta^*$% is %$s^{*}=t^{*}$%.
2. If %$\theta$% is %$Rt_{1}\dotsm t_{n}$%, then %$\theta^*$% is %$Rt_{1}^{*}\dotsm t_{n}^{*}$%.
3. If %$\theta$% is %$(\phi\land\psi )$%, %$(\phi\lor\psi )$%, %$(\phi\rightarrow\psi )$%, %$(\phi\leftrightarrow\psi )$%, or %$(\lnot\phi )$%, then %$\theta^*$% is,respectively, %$(\phi^{*}\land\psi^{*} )$%, %$(\phi^{*}\lor\psi ^{*})$%, %$(\phi^{*}\rightarrow\psi ^{*})$%, %$(\phi^{*}\leftrightarrow\psi ^{*})$%, or %$(\lnot\phi ^{*})$%
4. If %$\theta$% is %$\forall\nu\phi$% or %$\exists\nu\phi$%, where %$\nu$% is of sort %$s$% , then %$\theta^*$% is, respectively, %$\forall\nu^{*}(P_{s}\nu^{*}\rightarrow\phi^{*})$% or %$\exists\nu^{*}(P_{s}\nu^{*}\land\phi^{*})$%.

It is tedious but elementary to prove that for every sorted structure %$\mathfrak A$%, formula %$\phi$% in the language of %$\mathfrak A$%, and assignment %$s$% for %$\mathfrak A$%, that

%$\mathfrak{A}\models\phi [s]$% if and only if%$\mathfrak{A}^{*}\models\phi ^{*}[s^{*}]$%

Second-order logic

Syntax of second-order logic

Add to our list of symbols infinitely many %$n$%-placed predicate variables for each natural number %$n$%.

Add to the definition of formula:

If %$X$% is an %$n$%-placed predicate variable, then %$Xt_{1}\dotsm t_{n}$% is a formula, where each %$t_{i}$% is either a constant symbol or an ordinary, first-order variable.

If %$X$% is an %$n$%-placed predicate variable and %$\phi$% is a formula, then %$\forall X\phi$% and %$\exists X\phi$% are formulas.

Nothe that, though I didn't make it explicit, the syntax of second-order logic is just that of a sorted first-order logic.

Semantics of second-order logic

An assignment for a structure %$\mathfrak A$% is a function that takes each first-order variable to a member of %$A$% as before and that takes each %$n$%-placed predicate variable to a set of %$n$%-tuples of members of %$A$%. If %$s$% is an assignment for %$\mathfrak A$%, %$X$% is an %$n$%-placed predicate variable, and %$\mathbold R$% is a set of %$n$%-tuples of members of %$A$%, then %$s(x/\mathbold{R})$% is the assignment that assigns %$\mathbold R$% to %$X$%, and otherwise agrees with %$s$%.

Add the following clauses to the definition of satisfaction:

If %$\phi$% is %$Xt_{1}\dotsm t_{n}$%, where each %$t_{i}$% is either a constant symbol or an ordinary, first-order variable, then %$\mathfrak{A}\models\phi$% if %$\langle t_{1}^{\mathfrak{A}[s]},\dotsc ,t_{n}^{\mathfrak{A}[s]}\rangle\in s(X)$%.

If %$\phi$% is %$(\forall X\psi)$%, where %$X$% has %$n$% places, then %$\mathfrak{A}\vDash\phi [s]$% if for every assignment %$r$% that agrees with %$s$% on every variable other than %$X$%, %$\mathfrak{A}\vDash\psi [r]$%, or, equivalently, if for every %$\mathbold{R}\subseteq A^{n}$%, %$\mathfrak{A}\vDash\psi [s(X /\mathbold{R})]$%.

If %$\phi$% is %$(\exists X\psi)$%, where %$X$% has %$n$% places, then %$\mathfrak{A}\vDash\phi [s]$% if there is an assignment %$r$% that agrees with %$s$% on every variable other than %$X$% such that %$\mathfrak{A}\vDash\psi [r]$%, or, equivalently, if there is %$\mathbold{R}\subseteq A^{n}$% such that %$\mathfrak{A}\vDash\psi [s(X /\mathbold{R})]$%.

Plural quantifiers

The logic with plural quantification is just like second order logic restricted to only 1-placed predicate variables. It is cute to use %$xx$% instead of %$X$% and to write %$x\prec xx$% instead of %$Xx$%. Since the value of an assignment on %$xx$% is a set, and we don't want that, we let the value be some things in the domain (those in the set), instead.

The clauses in the definition of satisfaction are mathematically identical to the ones for second-order logic, but one can make them look different by rendering them thus:

IIf %$\phi$% is %$t\prec xx$%, where %$t$% is either a constant symbol or an ordinary, first-order variable, then %$\mathfrak{A}\models\phi$% if %$t^{\mathfrak{A}[s]}$% is among the %$s(xx)$%.

If %$\phi$% is %$(\forall xx\psi)$%, then %$\mathfrak{A}\vDash\phi [s]$% if for every assignment %$r$% that agrees with %$s$% on every variable other than %$xx$%, %$\mathfrak{A}\vDash\psi [r]$%, or, equivalently, if there are some things %$\mathbold R$% in %$A$% such that %$\mathfrak{A}\vDash\psi [s(xx /\mathbold{R})]$%.

If %$\phi$% is %$(\exists xx\psi)$%, then %$\mathfrak{A}\vDash\phi [s]$% if there is an assignment %$r$% that agrees with %$s$% on every variable other than %$xx$% such that %$\mathfrak{A}\vDash\psi [r]$%, or, equivalently, if there are some things %$\mathbold{R}$% in %$A$% such that %$\mathfrak{A}\vDash\psi [s(xx /\mathbold{R})]$%.

Modal logic

Quantified modal logic is a mess, and so I won't do it here, but, in quantified modal logic, the formulas would be those of first- or second-order logic with modal operators added, and each possible world would be a structure, first- or second-order, as defined above.

Syntax of modal logic

Let %$\mathcal L$% be a set of sentence letters, henceforth fixed. Each member of %$\mathcal L$% is a sentence of modal logic and, if %$\phi$% and %$\psi$% are sentences of modal logic, then so are %$(\phi\land\psi )$%, %$(\phi\lor\psi )$%, %$(\phi\rightarrow\psi )$%, %$(\phi\leftrightarrow\psi )$%, %$(\lnot\phi )$%, %$(\square\phi )$%, and %$(\lozenge\phi )$%.

Semantics of modal logic

A possible world %$A$% is a subset of %$\mathcal L$%, the set of sentence letters true at the world. A modal frame %$\mathfrak M$% is a set of possible worlds with a binary relation %$\rho$% on them called the accessibility relation. It is usual to require that every world be accessible from itself, that is, that the accessibiltiy relation be reflexive, but nothing in the mathematical formalism requires it.

A sentence %$\theta$% is true at a world %$\mathfrak w$% in a frame %$\mathfrak M$% if

1. %$\theta$% is a sentence letter and %$\theta\in\mathfrak w$%.
2. %$\phi$% is %$(\phi\land\psi )$%, %$(\phi\lor\psi )$%, %$(\phi\rightarrow\psi )$%, %$(\phi\leftrightarrow\psi )$%, or %$(\lnot\phi )$%, and, respectively, %$\phi$% and %$\psi$% are both true at %$\mathfrak w$%, at least one of them is true at %$\mathfrak w$%, %$\phi$% is not true at %$\mathfrak w$% or %$\psi$% is true at %$\mathfrak w$%, %$\phi$% and %$\psi$% are either both true or both false at %$\mathfrak w$%, or %$\phi$% is not true at %$\mathfrak w$%.
3. %$\phi$% is %$(\square\phi )$%, and %$\phi$% is true at every world accessible from %$\mathfrak w$%.
4. %$\phi$% is %$(\lozenge\phi )$%, and %$\phi$% is true at some world accessible from %$\mathfrak w$%.

A sentence %$\theta$% is true in a frame %$\mathfrak M$% if it is true at every world in %$\mathfrak M$%.

-- ShaughanLavine - 04 May 2009