Possible Worlds Semantics for Second-Order Modal Logic

This is an attempt to define Second-Order Modal Logic in terms of possible worlds. The decision algorithm behind the web app http://somerby.net/mack/logic assumes that logical symbols have the meanings stated here.

There is not much in this document except definitions. I intend to write a complete paper on the subject someday. This paper would contain some evidence that these definitions are correct, a proof of decidability for a subset of symbolic that includes propositions, properties, and the necessity operator, and a decision algorithm for that subset. Also, since the meaning of the necessity operator given here is different from the meanings that it is normally given in modal predicate logic, the paper would also present definitions for necessity operators that capture these normal meanings that show the differences, show how they can be expressed in terms of the necessity operator used here, also show (what is already known) that predictate logics with these notions of necessity are not decideable. This would be a big project for me and I don’t know when I will get around to doing it, so I’ve decided I should at least share the definitions.

1 Symbols

These are definitions for some symbols that appear in the definitions:

$$𝒫(S):=\text{the power set of }S$$ (1)

$$\bigcup S:=\text{the union of all sets in }S$$ (2)

$$S^2:=S\times S:=\{(x,y):x\in S,y\in S\}$$ (3)

$$\lambda \text{(letters)}.\text{(expression)}:=\text{a function, where each letter is an argument to the function.}$$ (4)

$$\underset{m\in S}{\bigwedge }\varphi :=\varphi \text{ is true for each }m\text{ in }S$$ (5)

$$\mathbb{P}:=\text{the set of all possible worlds}$$ (6)

2 Meanings of Variables

$\varphi$ is a syntactically valid statement of Second-Order Logic or a syntactically valid true/false expression within a statement of Second-Order Logic.

$\psi$ is a syntactically valid statement of Second-Order Logic or a syntactically valid true/false expression within a statement of Second-Order Logic.

$f$ is a function which is defined as a set of ordered pairs. The first items in the pairs are the domain of the function – the inputs or arguments that function is defined for – and the second items in the pairs are the range of the function – the outputs or results of the function.

$w$ is a possible world.

$o$ is an object in a possible world.

$s$ is a symbol, usually a letter.

$S$ is a set of symbols.

$v$ is a function that, for a set of symbols (usually lowercase letters), maps each symbol to an object that exists in a possible world.

$n$ is a function that, for a set of possible words, maps each possible world to a set of symbols (usually lowercase letters) that are supposed to represent propositions that are true in that possible world.

$u$ is a function that, for a set of objects, maps each object to a set of symbols (usually uppercase letters) that are supposed to represent predicates that are true of that object.

$b$ is a function that, for a set of pairs of objects, maps each pair to a set of symbols (usually uppercase letters) that are supposed to represent relations that exist between the pair.

3 Possible Worlds Semantics

A possible world is just a set of objects – the objects that exist in that world. Whether or not an object in a possible world is a subset of another object does not enter into these definitions.

Possible worlds are assumed not to be empty:

$$\mathrm{\neg }\exists w,w\in \mathbb{P}\wedge w=\mathrm{\varnothing }$$ (7)

Transworld identity is assumed to be impossible:

$$\forall o,\forall w_1,\forall w_2,(w_1\in \mathbb{P}\wedge w_2\in \mathbb{P}\wedge o\in w_1\wedge w_1\ne w_2)\to o\notin w_2$$ (8)

A proposition symbol, or nullary predicate, is interpreted to be the set of possible world in which a proposition is true.

A property symbol, or unary predicate, is interpreted to be the set of objects which have a property.

A relation symbol, or binary predicate, is interpreted to be the set of pairs of objects which have a relation.

4 Translation

The definitions in Sections 5 through 8 are meant to be textual replacements that convert statements in conventional language of symbolic logic to statements about the set of possible worlds, $\mathbb{P}$, in the language of set theory. They are meant to be applied recursively to a statement, with parentheses added to the replacements to preserve order of operations. So, a definition of the form

$$\mathrm{\dots }\varphi \mathrm{\dots }:=definition$$ (9)

declares that, to translate “$\mathrm{\dots }\varphi \mathrm{\dots }$”, $\varphi$ should first be translated, then every instance of $\varphi$ in $definition$ should be replaced with the result of that translation, and then the resulting expression should be surrounded by parentheses.

5 Binding Symbols

A statement may have free symbols in it – symbols that are not bound by any quantifier. In both First-Order and Second-Order Logics, free symbols represent constants. In First-Order Logic, all propositions, predicates and relations are free. To decide the validity of a statement, it must be decided whether it is true for all possible meanings of the free symbols. The functions defined in this section are used to bind symbols in such a way that the statement is considered for all possible meanings of the symbol.

$$\text{free-v}(\varphi ):=\text{an ordered list of free variables in }\varphi$$ (10)

$$\text{free-n}(\varphi ):=\text{an ordered list of free nullary predicates in }\varphi$$ (11)

$$\text{free-u}(\varphi ):=\text{an ordered list of free unary predicates in }\varphi$$ (12)

$$\text{free-b}(\varphi ):=\text{an ordered list of free binary predicates in }\varphi$$ (13)

(14)

(15)

(16)

(17)

6 Boolean Definitions

These definitions translate statements of symbolic logic into Boolean (true/false) statements:

6.1 Necessity

A statement is necessarily true if and only if it is true in all possible worlds.

$$\mathrm{\square }\varphi :=\underset{w\in \mathbb{P}}{\bigwedge }\varphi$$ (18)

6.2 Universal Generalization

A universal generalization is true if and only if its predicate is true for all objects in the possible world that is assumed to be the current context.

$$\forall \text{x},\varphi :=\underset{\text{x}\in w}{\bigwedge }\varphi$$ (19)

6.3 Validity

A statement is valid if and only if it is true in all possible worlds for all possible assignments of objects in each possible world to constants, under all possible meanings for the free propositions, predicates and relations in the statement.

$$\text{valid}(\varphi ):=\text{bind-b}(\text{bind-n}(\text{bind-u}(\mathrm{\square }(\text{bind-v}(\varphi ))))$$ (20)

6.4 Propositions

A proposition is conflated with the set of possible worlds that it is true in. A proposition is true if and only if it includes the possible world that is assumed to be the current context.

$$\text{p}:=w\in \text{p}$$ (21)

$$\forall \text{p},\varphi :=\underset{\text{p}\in 𝒫(\mathbb{P})}{\bigwedge }\varphi$$ (22)

6.5 Properties

A property is conflated with the set of objects that have it. An object has a property if and only if it is a member the property.

$$\text{Px}:=\text{x}\in \text{P}$$ (23)

$$\forall \text{P},\varphi :=\underset{\text{P}\in 𝒫(\bigcup \mathbb{P})}{\bigwedge }\varphi$$ (24)

6.6 Relations

A relation is conflated with the set of ordered pairs of objects that have it. An ordered pair of objects has a relation if it is a member of the relation.

$$\text{Rxy}:=(\text{x},\text{y})\in \text{R}$$ (25)

$$\forall \text{R},\varphi :=\underset{\text{R}\in 𝒫({(\bigcup \mathbb{P})}^2)}{\bigwedge }\varphi$$ (26)

6.7 Other Operators

No special definition is needed for negation or conjunction. Because of (8), identity also does not need a special definition.

$$\text{x=y}:=\text{x}=\text{y}$$ (27)

$$\mathrm{\neg }\varphi :=\mathrm{\neg }\varphi$$ (28)

$$\varphi \wedge \psi :=\varphi \wedge \psi$$ (29)

Operators that can be defined in terms of the operators above, such as ‘$\exists$’, ‘$\vee$’ and ‘$\mathrm{◇}$’, are defined in the usual way.

7 Set Definitions

These definitions are based on the idea that the meaning of a statement is the set of possible worlds that it is true in. These definitions translate a statement of symbolic logic to an expression that identifies a set of possible worlds.

7.1 Truth

$\varphi$ is true when and where $\varphi$ includes the possible world that is assumed in the current context.

$$\text{true}(w,\varphi ):=w\in \varphi$$ (30)

7.2 Validity

$\varphi$ is valid if the result of binding all of its free variables and symbols is an expression that identifies a set that includes all possible worlds.

$$\text{valid}(\varphi ):=\text{bind-b}(\text{bind-n}(\text{bind-u}(\mathrm{\square }(\text{bind-v}(\varphi ))))=\mathbb{P}$$ (31)

7.3 Necessity

$\mathrm{\square }\varphi$ is the set of all possible worlds if $\varphi$ is the set of all possible worlds. Otherwise, it is the empty set.

(32)

alternatively

(33)

7.4 Universal Generalization

$\forall \text{x},\varphi$ is the set of possible worlds which are included in $\varphi$ no matter what object in the current world is assigned to the symbol ‘x’.

$$\forall \text{x},\varphi :=\bigcap _{\text{x}\in w}\varphi$$ (34)

7.5 Propositions

Since a proposition is a set of possible worlds, it needs no special definition.

A generalization of ‘p’ over $\varphi$ is the set of possible worlds which are included in $\varphi$ no matter what set of possible worlds is assumed for ‘p’.

$$\forall \text{p},\varphi :=\bigcap _{\text{p}\in 𝒫(\mathbb{P})}\varphi$$ (35)

7.6 Properties

If an object x has a property P, Px is defined as the set of all possible worlds. If it does not have property P, Px is defined as the empty set. This is because, in context, its truth or falsehood only depends on the object assigned to x and the property assigned to P and not the possible world assumed in the context.

(36)

$$\forall \text{P},\varphi :=\bigcap _{\text{P}\in 𝒫(\bigcup \mathbb{P})}\varphi$$ (37)

7.7 Relations

If a pair (x,y) in a relation R, Rxy is defined as the set of all possible worlds. If it is not in a relation R, Rxy is defined as the empty set. This is because, in context, its truth or falsehood only depends on the objects assigned to x and y and the relation assigned to R and not the possible world assumed in the context.

(38)

$$\forall \text{R},\varphi :=\bigcap _{\text{R}\in 𝒫({(\bigcup \mathbb{P})}^2)}\varphi$$ (39)

7.8 Conjunction

The conjunction of $\varphi$ and $\psi$ is their set intesection – the set of possible worlds which are contained in both $\varphi$ and $\psi$.

$$\varphi \wedge \psi :=\varphi \cap \psi$$ (40)

7.9 Negation

The negation of $\varphi$ is its set complement – the set of possible worlds that are not in $\varphi$.

$$\mathrm{\neg }\varphi :=\overline{\varphi }$$ (41)

7.10 Other Operators

Because of (8), identity does not need a special definition.

$$\text{x=y}:=\text{x}=\text{y}$$ (42)

Operators that can be defined in terms of the operators above, such as ‘$\exists$’, ‘$\vee$’ and ‘$\mathrm{◇}$’, are defined in the usual way.

8 Definitions for Decidability

My plan for a proof of decidability involves proving that certain generalizations over infinite sets of objects or infinite sets of sets of objects are logically equivalent to generalizations over finite sets of strings of symbols. To make this proof easier, I defined the logical operators as functions of the variables $w$, $v$, $n$, $u$ and $b$, which are described in section (2). In these definitions, mappings of things to strings of symbols are built up by “assigning” symbols to things, and “instantiating” variables with objects is achieved by building a mapping of variable symbols to objects.

8.1 Instantiation and Assignment

This function adds a symbol/object pair to a mapping of symbols to objects, associating the symbol with the object:

$$\text{instantiate}(v,s,o):=v\cup \{(s,o)\}$$ (43)

This function adds a symbol to the set of symbols associated with a thing $t$ in a mapping of things to symbols if $t$ belongs to a set of things $T$. If $t$ does not belong to $T$, the set of symbols associated with it is not changed:

$$\text{assign}(f,s,T):=\{(t,S\cup \{s\}):(t,S)\in f\wedge t\in T\}\cup \{(t,S):(t,S)\in f\wedge t\notin T\}$$ (44)

Alternatively,

$$\text{assign}(f,s,T):=\{p:\exists t,\exists S,(t,S)\in f\wedge (t\in T\to p=(t,S\cup \{s\}))\wedge (t\notin T\to p=(t,S))\}$$ (45)

Each kind of expression in Second-Order Logic is defined as a function of parameters $w$, $v$, $n$, $u$, $b$, which have the meanings described in Section 2 above. These parameters are the context of the expression; they provide the meaning of all of the predicates and variables in the expression.

8.2 Propositions

A proposition symbol “p” is true in context if it is in the set of symbols that are associated with the possible world $w$.

$$\text{“p”}:=\lambda wvnub.\text{‘p’}\in n(w)$$ (46)

8.3 Properties

A predication of a property P on an object x is true in context if it is in the set of symbols that are associated with the object that is associated with the symbol ‘x’ in context.

8.4 Relations

$$\text{“Px”}:=\lambda wvnub.\text{‘P’}\in u(v(\text{‘x’}))$$ (47)

A relation R between objects x and y is true in context if it is in the set of symbols that are associated with the pair of objects that are associated with symbols ‘x’ and ‘y’ in context.

$$\text{“Rxy”}:=\lambda wvnub.\text{‘R’}\in b(v(\text{‘x’}),v(\text{‘y’}))$$ (48)

8.5 Identity

x and y are identical if the symbols ‘x’ and ‘y’ are associated with the same object in context.

$$\text{“x=y”}:=\lambda wvnub.v(\text{‘x’})=v(\text{‘y’})$$ (49)

8.6 Negation

$\mathrm{\neg }\varphi$ is true if $\varphi$, in the same context, is false. $\varphi$ gets the same context as $\mathrm{\neg }\varphi$ because $\mathrm{\neg }\varphi$ passes its arguments to $\varphi$ unchanged.

$$\text{“}\mathrm{\neg }\varphi \text{”}:=\lambda wvnub.\mathrm{\neg }\varphi (w,v,n,u,b)$$ (50)

8.7 Conjunction

$\varphi \wedge \psi$ is true if both $\varphi$ and $\psi$ are false in the same context. $\varphi$ and $\psi$ get the same context as $\varphi \wedge \psi$ because $\varphi \wedge \psi$ passes its arguments to $\varphi$ and $\psi$ unchanged.

$$\text{“}\varphi \wedge \psi \text{”}:=\lambda wvnub.\varphi (w,v,n,u,b)\wedge \psi (w,v,n,u,b)$$ (51)

8.8 Necessity

$\varphi$ is necessarily true if it is true in every possible world. $\varphi$ does not always get the same context as $\mathrm{\square }\varphi$; it is considered in every possible world instead of just the current possible world. The assignment of objects to free variables in $\varphi$ does not change, nor do the objects change.

$$\text{“}\mathrm{\square }\varphi \text{”}:=\lambda w_{1}vnub.\underset{w_2\in \mathbb{P}}{\bigwedge }\varphi (w_2,v,n,u,b)$$ (52)

8.9 Universal Generalization

A universal generalization is true if and only if, for every object that is in the current possible world, $\varphi$ is true when instantiated with the object.

$$\text{“}\forall \text{x},\varphi \text{”}:=\lambda wvnub.\underset{o\in w}{\bigwedge }\varphi (w,\text{instantiate}(v,\text{‘x’},o),n,u,b)$$ (53)

8.10 Generalization over Propositions

A proposition is conflated with the set of possible worlds in which it is true. Consequently, a generalization over propositions is true if and only if, for every combination of possible worlds, $\varphi$ is true when, for each possible world in the combination, ‘p’ is added to the list of propositions which are true in it.

$$\text{“}\forall \text{p},\varphi \text{”}:=\lambda wvnub.\underset{P\in 𝒫(\mathbb{P})}{\bigwedge }\varphi (w,v,\text{assign}(n,\text{‘p’},P),u,b)$$ (54)

8.11 Generalization over Properties

A property is conflated with the set of objects that have it. Consequently, a generalization over properties is true if and only if, for every combination of objects, $\varphi$ is true when, for each object in the combination, ‘P’ is added to the list of properties that the object has.

$$\text{“}\forall \text{P},\varphi \text{”}:=\lambda wvnub.\underset{p\in 𝒫(\bigcup \mathbb{P})}{\bigwedge }\varphi (w,v,n,\text{assign}(u,\text{‘P’},p),b)$$ (55)

8.12 Generalization over Relations

A relation is conflated with the set of pairs of objects that have it. Consequently, a generalization over relations is true if and only if, for every combination of pairs of objects, $\varphi$ is true when, for each pair in the combination, ‘R’ is added to the list of relations that the pair has.

$$\text{“}\forall \text{R},\varphi \text{”}:=\lambda wvnub.\underset{r\in 𝒫({(\bigcup \mathbb{P})}^2)}{\bigwedge }\varphi (w,v,n,u,\text{assign}(b,\text{‘R’},r))$$ (56)

8.13 Other Operators

Operators that can be defined in terms of the operators above, such as ‘$\exists$’, ‘$\vee$’ and ‘$\mathrm{◇}$’, are defined in the usual way.

8.14 Validity

Validity is defined similarly to how it is defined in Section 6.3, but since the other definitions are functions, valid($\varphi$) is a function application (a function call) that passes initial mappings and an empty world to the function that is the result of binding all of the free symbols in $\varphi$.

$$\begin{array}{c}\hfill \text{valid}(\varphi ):=\text{bind-b}(\text{bind-n}(\text{bind-u}(\mathrm{\square }(\text{bind-v}(\varphi ))))\\ \hfill (\mathrm{\varnothing },\mathrm{\varnothing },\{(w,\mathrm{\varnothing }):w\in \mathbb{P}\},\{(o,\mathrm{\varnothing }):o\in \bigcup \mathbb{P}\},\{((a,b),\mathrm{\varnothing }):a\in \bigcup \mathbb{P}\wedge b\in \bigcup \mathbb{P}\}))\end{array}$$ (57)