-
Notifications
You must be signed in to change notification settings - Fork 238
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
initial checkin of style and first section files
- Loading branch information
Showing
13 changed files
with
865 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
\documentclass{memoir} | ||
|
||
\usepackage{subfiles} | ||
|
||
\usepackage{amsmath} | ||
\usepackage[greekformulas]{../open-logic} | ||
|
||
\begin{document} | ||
\subfile{sets-and-relations} | ||
\end{document} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,310 @@ | ||
\documentclass[misc]{subfiles} | ||
|
||
\begin{document} | ||
|
||
\section{Sets and Relations}\label{sec:Sets-and-Relations} | ||
|
||
|
||
\subsection{Sets}\label{ssec:Sets} | ||
|
||
Sets and relations are the fundamental building blocks from which | ||
we construct structures used to interpret logical languages. For instance, a model~$\Mod M$ | ||
for a first-order language consists of a set~$D$ (the ``domain'' | ||
or ``universe of discourse'') and relations on~$D$ for each predicate | ||
symbol in the language. For the semantics of modal logic, we will | ||
make extensive use of sets and relations; in particular, certain specific | ||
kinds of relations will play a prominent role. Hence, let's first | ||
review what sets and relations are. | ||
|
||
\begin{defn} | ||
A set is a collection of objects, considered independently of the | ||
way it is specified, of the order of its elements, or of their | ||
multiplicity. The objects making up the set are called \emph{elements} of | ||
the set. If $a$ is an element of a set $X$, we write $a \in X$ (otherwise, | ||
$a \notin X$). The set which has no elements is called the \emph{empty set} | ||
and denoted~$\emptyset$. | ||
\end{defn} | ||
|
||
\begin{ex} | ||
Whenever you have a bunch of objects, you can collect them together | ||
in a set. The set of Richard's siblings, for instance, is a set that | ||
contains one person, and we could write it as $S=\{\textrm{Ruth}\}$. | ||
In general, when we have some objects $a_{1}$, \dots{}, $a_{n}$, | ||
then the set consisting of exactly those objects is written $\{a_{1},\dots,a_{n}\}$. | ||
\end{ex} | ||
|
||
Frequently we'll specify a set by some property that its elements | ||
share---as we just did, for instance, by specifying $S$ as the set | ||
of Richard's siblings. We'll use the following shorthand notation | ||
for that: $\{x : \ldots x \ldots\}$ (pronounced ``the set of all | ||
$x$ such that $\ldots x\ldots$''), where the $\ldots x\ldots$ | ||
is the property that $x$ has to have in order to be counted among | ||
the elements of the set. In our example, we could have specified $S$ | ||
also as $S=\{x : x\text{ is a sibling of Richard}\}$. When we say | ||
that sets are independent of the way they are specified, we mean | ||
that the elements of a set are all that matters. For instance, it | ||
so happens that $\{\text{Nicole},\text{Jacob}\}$, $\{x : x\text{ is a niece or nephew of Richard}\}$ and | ||
$\{x :d x\text{ is a child of Ruth}\}$ are three ways of specifying | ||
one and the same set. Saying that sets are considered independently | ||
of the order of their elements and their multiplicity is a fancy way | ||
of saying that $\{\text{Nicole}, \text{Jacob}\}$ and $\{\text{Jacob},\text{Nicole}\}$ are | ||
two ways of specifying the same set; and that $\{\text{Nicole},\text{Jacob}\}$ | ||
and $\{\text{Jacob},\text{Nicole}, \text{Nicole}\}$ are two ways of | ||
specifying the same set. | ||
|
||
Mostly we'll be dealing with sets that have mathematical objects as | ||
members. You will remember the various sets of numbers: $\mathbb{N}$ | ||
is the set of \emph{natural} numbers $0$, $1$, $2$, $3$, \dots{}; | ||
$\mathbb{Z}$ the set of \emph{integers} \dots{}, $-3$, $-2$, | ||
$-1$, $0$, $1$, $2$, $3$, \dots{}; $\mathbb{Q}$ the set of | ||
\emph{rationals} ($\mathbb{Q}=\{p/q : p,q\in\mathbb{Z}\}$); and | ||
$\mathbb{R}$ the set of \emph{real} numbers. These are all \emph{infinite} | ||
sets, that is, they each have infinitely many elements. As it turns | ||
out, $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ have the same number | ||
of elements, while $\mathbb{R}$ has a whole bunch more---$\mathbb{N}$, | ||
$\mathbb{Z}$, $\mathbb{Q}$ are ``countably infinite'' whereas | ||
$\mathbb{R}$ is ``uncountable''. | ||
|
||
\begin{ex}\label{ex:strings} | ||
Another interesting set is the set $A^{*}$ of | ||
\emph{strings} over an alphabet $A$: any sequence of elements of | ||
$A$ is a string over $A$. We include the \emph{empty string $\Lambda$} | ||
among the strings over $A$, for every alphabet~$A$. For instance, | ||
if $A = \{0,1\}$, then | ||
\[ | ||
\mathbb{B}=A^{*}=\{\Lambda,0,1,00,01,10,11,000,001,010,011,100,101,110,111,0000,\ldots\}. | ||
\] | ||
If $x=x_{1}\ldots x_{n}\in A^{*}$ is a string consisting of $n$ | ||
``letters'' from $A$, then we say the \emph{length} of the string is~$n$ | ||
and write $\len(x)=n$. | ||
\end{ex} | ||
|
||
\begin{defn} | ||
A set $X$ is a \emph{subset} of a set $Y$, $X \subseteq Y$, iff every | ||
element of $X$ is also an element of $Y$. If $X\subseteq Y$ and | ||
$X\neq Y$, we say that $X$ is a \emph{proper subset} of $Y$ and | ||
write $X\subsetneq Y$. The set of all subsets of a set~$X$ is called | ||
the \emph{power set} of~$X$, and denoted~$\wp(X)$. | ||
\end{defn} | ||
|
||
\begin{ex} | ||
The empty set~$\emptyset$ is a subset of every set, and every set | ||
is a subset of itself. If $X$ is a finite set with $n$ elements, | ||
then there are $2^{n}$ subsets of~$X$. For instance, $X=\{1,2,3\}$has | ||
$2^{3}=8$ subsets, namely: | ||
\[ | ||
\wp(X)=\{\emptyset,\{1\},\{2\},\{3\},\{1,2\},\{1,3\},\{2,3\},\{1,2,3\}\}. | ||
\] | ||
Of our previous examples, we have $\mathbb{N}\subseteq\mathbb{Z}\subseteq\mathbb{Q}\subseteq\mathbb{R}$ | ||
(in fact, these are all proper subsets). If $A\subseteq B$, then | ||
also $A^{*}\subseteq B^{*}$ and $\wp(A) \subseteq \wp(B)$. | ||
\end{ex} | ||
|
||
\begin{defn} | ||
If $X$and $Y$ are sets, then the \emph{intersection} $X\cap Y$ | ||
of $X$ and $Y$ is the set of all elements of $X$ which are also | ||
elements of $Y$, i.e., $X\cap Y=\{x : x\in X\text{ and }x\in Y\}$. | ||
If $X$ and $Y$ have no elements in common, then $X \cap Y = \emptyset$,and | ||
we call $X$ and $Y$ \emph{disjoint.} The \emph{union}~$X \cup Y$ | ||
of $X$ and $Y$ is the set consisting of the elements of $X$ together | ||
with all the elements of $Y$, i.e., $X \cup Y=\{x : x\in X\text{ or }x\in Y\}$. | ||
The \emph{difference}~$X \setminus Y$ is the set of all elements | ||
of $X$ which are not also elements of $Y$, i.e., $X \setminus Y = \{x : x\in X\text{ and }x\notin Y\}$. | ||
\end{defn} | ||
|
||
It will ofent be necessary to describe the unions or intersections not just of two, but of many sets. Since sets are collections of arbitrary objects, we can form sets of sets. The power set of a set~$X$ is aset of sets, for instance, and its powerset is a set of sets of sets. | ||
|
||
\begin{defn} | ||
If $X$ is a set (of sets), then $\bigcap X = \{x : x \in Y \text{ for all } Y \in X\}$ and $\bigcup X = \{x : x \in Y \text{ for some } Y \in X\}$ are the intersection and union, respectively, of all sets in~$X$. | ||
\end{defn} | ||
|
||
If the elements of $X$ are indexed, e.g., $X = \{Y_0, Y_1, Y_2, \dots\}$, we will also write $\bigcap_{i=0}^\infty Y_i$ and $\bigcap_{i=0}^\infty Y_i$ for $\bigcap X$ and $\bigcup X$, respectively. Often infinite sets are constructed as the unions or intersections of an infinite sequence of sets, which may be nested ($Y_0 \subseteq Y_1 \subseteq Y_2 \subseteq \dots$). It will be important to remember in such cases that $x \in \bigcup_{i=0}^\infty$ iff $x \in Y_i$ for some~$i$. | ||
|
||
\subsection{Relations} | ||
|
||
Now that we've reviewed what sets are and seen some examples, you | ||
will no doubt remember some interesting relations between objects | ||
of some of these sets. For instance, numbers come with an \emph{order | ||
relation}~$<$ and from the theory of whole numbers the relation | ||
of \emph{divisibility without remainder} (usually written $n \mid m$) | ||
may be familar. There is also the relation \emph{is identical with} | ||
that every object bears to itself and to no other thing. But there | ||
are many more interesting relations that we'll encounter, and even | ||
more possible relations. Before we review them, we'll just point out | ||
that we can look at relations as a special sort of set. For this, | ||
we'll first need to define what a \emph{pair} is: if $a$ and $b$ | ||
are two objecta, we can combine them into the \emph{ordered pair}~$(a,b)$. | ||
Note that for ordered pairs the order \emph{does} matter, e.g, $(a,b)\neq(b,a)$ | ||
(in contrast to unordered pairs, i.e., 2-element sets, where $\{a,b\}=\{b,a\}$). | ||
|
||
\begin{defn} | ||
If $X$ and $Y$ are sets, then the \emph{Cartesian product} $X \times Y$ | ||
of $X$ and $Y$ is the set of all pairs $(a,b)$ with $a\in X$ and | ||
$b\in Y$. In particular, $X^{2}=X \times X$ is the set of all pairs | ||
from~$X$. | ||
\end{defn} | ||
|
||
Now consider a relation on a set, e.g., the $<$-relation on the set | ||
$\mathbb{N}$ of natural numbers, and consider the set of all pairs | ||
of numbers $(n,m)$ where $n<m$, i.e., | ||
\[ | ||
R=\{(n,m)\mid n,m\in\mathbb{N}\text{ and }n<m\}. | ||
\] | ||
Then there is a close connection between the a number $n$ being less | ||
than a number $m$ and the corresponding pair $(n,m)$ being a member | ||
of $R$, namely, $n<m$ if and only if $(n,m) \in R$. In a sense we | ||
can consider the set $R$ to \emph{be} the $<$-relation on the set | ||
$\mathbb{N}$. In the same way we can construct a subset of $\mathbb{N}^{2}$ for | ||
any relation between numbers. Conversely, given any set of pairs of | ||
numbers $S\subseteq\mathbb{N}^{2}$, there is a corresponding relation | ||
between numbers, namely, the relationship $n$ bears to $m$ if and | ||
only if $(n,m) \in S$. This justifies the following definition: | ||
|
||
\begin{defn} | ||
A \emph{binary relation} on a set $X$ is a subset of $X^{2}$. If | ||
$R\subseteq X^{2}$ is a binary relation on~$X$ and $x,y\in X$, | ||
we write $Rxy$ (or $xRy$) for $(x,y)\in R$. | ||
\end{defn} | ||
|
||
\begin{ex}label{ex:relations} | ||
The set $\mathbb{N}^{2}$of | ||
pairs of natural numbers can be listed in a 2-dimensional matrix like | ||
this: | ||
\[ | ||
\begin{array}{ccccc} | ||
\mathbf{(0,0)} & (0,1) & (0,2) & (0,3) & \ldots\\ | ||
(1,0) & \mathbf{(1,1)} & (1,2) & (1,3) & \ldots\\ | ||
(2,0) & (2,1) & \mathbf{(2,2)} & (2,3) & \ldots\\ | ||
(3,0) & (3,1) & (3,2) & \mathbf{(3,3)} & \ldots\\ | ||
\vdots & \vdots & \vdots & \vdots & \mathbf{\ddots} | ||
\end{array} | ||
\] | ||
The subset consisting of the pairs lying on the diagonal, $I=\{(0,0),(1,1),(2,2),\ldots\}$, | ||
is the \emph{identity relation on}~$\mathbb{N}$. (Since the identity | ||
relation is popular, let's define $I_{X}=\{(x,x) : x\in X\}$ for any | ||
set $X$.) The subset of all pairs lying above the diagonal, $L = \{(0,1),(0,2),\ldots,(1,2),(1,3),\ldots,(2,3),(2,4),\ldots\}$ is | ||
the \emph{less than} relation, i.e., $Lnm$ iff $n<m$. The subset | ||
of pairs below the diagonal, $G=\{(1,0),(2,0),(2,1),(3,0),(3,1),(3,2),\ldots\}$ | ||
is the \emph{greater than} relation, i.e., $Gnm$ iff $n>m$. The | ||
union of $L$ with $I$, $K=L\cup I$, is the \emph{less than or equal | ||
to} relation: $Kmn$ iff $n\le m$. Similarly, $H=G\cup I$ is the | ||
\emph{greater than or equal to relation.} $L$, $G$, $K$, and $H$ | ||
are special kinds of relations called \emph{orders}. $L$ and $G$ | ||
have the property that no number bears $L$ or $G$ to itself (i.e., | ||
for all $n$, neither $Lnn$ nor $Gnn$). Relations with this property | ||
are called \emph{antireflexive}, and, if they also happen to be orders, | ||
they are called \emph{strict orders.} | ||
|
||
Although orders and identity are important and natural relations, | ||
it should be emphasized that according to our definition \emph{any} | ||
subset of $X^{2}$ is a relation on~$X$, regardless of how unnatural | ||
or contrived it seems. In particular, $\emptyset$ is a relation on | ||
any set (the \emph{empty relation}, which no pair of elements bears), | ||
and $X^{2}$ itself is a relation on $X$ as well (the universal relation, which every | ||
pair bears). But also something like $E=\{(n,m) : d n>5\text{ or }m\times n\ge 34\}$ | ||
counts as a relation. | ||
\end{ex} | ||
|
||
\begin{defn} | ||
If $R$ is a relation, then the \emph{domain}~$\dom{R}$ is the set of all elements related by~$R$, i.e., $\dom{R} = \{a : \text{for some }b, Rab\}$. | ||
The \emph{range}~$\ran{R}$ is the set of all elements related to by~$R$, i.e., $\ran{R} = \{b : \text{for some }a, Rab\}$. | ||
\end{defn} | ||
|
||
\begin{defn} | ||
A relation $R$ over a set $X$ is called \emph{reflexive} if, for | ||
every $x\in X$, $Rxx$. A relation which has the property that whenever | ||
$Rxy$ and $Ryz$, then also $Rxz$, is called \emph{transitive}. | ||
$R$ is called \emph{anti-symmetric,} if, whenever both $Rxy$ and | ||
$Ryx$, then $x=y$ (or, in other words: if $x\neq y$ then either | ||
$\not Rxy$ or $\not Ryx$). Finally, $R$ is \emph{total} if for | ||
all $x,y\in X$, either $Rxy$ or $Ryx$. | ||
|
||
A relation which is both reflexive and transitive is called a \emph{preorder.} | ||
A preorder which is also anti-symmetric is called a \emph{partial | ||
order}. A partial order which is also total is called a \emph{total | ||
order} or \emph{linear order.} (If we want to emphasize that the order | ||
is reflexive, we add the adjective ``weak''---see below). | ||
\end{defn} | ||
|
||
\begin{ex} | ||
Every linear order is also a partial order, and every partial order | ||
is also a preorder, but the converses don't hold. For instance, the | ||
identity relation and the universal relation on~$X$ are preorders, but | ||
they are not partial orders, because they are not anti-symmetric (if | ||
$X$ has more than one element). For a somewhat less silly example, | ||
consider the \emph{no longer than} relation $\preccurlyeq$on~$\mathbb{B}$: | ||
$x\preccurlyeq y$ iff $\len(x)\le\len(y)$. This is a preorder, even | ||
a total preorder, but not a partial order. The relation of \emph{divisibility | ||
without remainder} gives us an example of a partial order which isn't | ||
a total order: for integers $n$, $m$, we say $n$ (evenly) divides | ||
$m$, in symbols: $n\mid m$, if there is some $k$ so that $m=kn$. | ||
On $\mathbb{N}$, this is a partial order, but not a linear order: | ||
for instance, $2\nmid3$ and also $3\nmid2$. Considered as a relation | ||
on $\mathbb{Z}$, divisibility is only a preorder since anti-symmetry | ||
fails: $1\mid-1$ and $-1\mid1$ but $1\neq-1$. Another important | ||
partial order is the relation $\subseteq$ on a set of sets. | ||
|
||
Notice that the examples $L$ and $G$ from \ref{ex:relations}, | ||
although we said there that they were called ``strict orders'' are | ||
not total orders even though they are total. But there is a close | ||
connection, as we will see momentarily. | ||
\end{ex} | ||
|
||
\begin{defn} | ||
A relation $R$ on $X$is called \emph{irreflexive} if, for all $x\in X$, | ||
$x\not Rx$. $R$ is called \emph{asymmetric} if for no pair $x,y\in X$ | ||
we have $xRy$ and $yRx$. A \emph{strict partial order} is a relation | ||
which is irreflexive, asymmetric, and transitive. A strict partial | ||
order which is also linear is called a \emph{strict linear order.} | ||
\end{defn} | ||
|
||
A strict partial order $R$ on $X$ can be turned into a weak partial | ||
order $R'$ by adding the identity relation on $X$. | ||
Conversely, starting from a weak partial order, one can get a strict | ||
partial order by removing~$I_{X}$ | ||
|
||
\begin{prop} | ||
Let $R$ be a relation on $X$ and $R'= R \cup I{}_{X}$. Then | ||
$R$ is a strict partial (linear) order on $X$ iff $R'$ is a weak | ||
partial (linear) order. Moreover, $xRy$ iff $xR'y$ for all $x\neq y$.\end{prop} | ||
|
||
\begin{ex} | ||
$\le$ is the weak linear order corresponding to the strict linear | ||
order $<$. $\subseteq$ is the weak partial order corresponding to | ||
the strict partial order $\subsetneq$. | ||
\end{ex} | ||
|
||
\begin{prob} | ||
Show that if $R$ is a weak partial order on $X$, then $R^{-} = R\setminus I_{X}$ | ||
is a strict partial order and $xRy$ iff $xR^{-}y$ for all $x\neq y$.\end{prob} | ||
|
||
\subsection{Operations on Relations} | ||
|
||
It is often useful to modify or combine relations. We've already used the union of relations above (which is just the union of two relations considered as sets of pairs). Here are some other ways: | ||
|
||
\begin{defn} Let $R$, $S$ be relations and $X$ a set. | ||
\begin{enumerate} | ||
\item The \emph{inverse}~$R^{-1}$ of $R$ is $R^-1 = \{ (b, a) : (a, b) \in R\}$. | ||
\item The \emph{relative product}~$R \mid S$ of $R$ and $S$ is | ||
\[ | ||
(R \mid S) = \{(a, c) : \text{for some }b, Rab \text{ and } Rbc\} | ||
\] | ||
\item The \emph{restriction}~$R \restrict X$ of $R$ to $X$ | ||
\item The \emph{application}~$R[X]$ of $R$ to $X$ is | ||
\[ | ||
R[X] = \{b : \text{for some }a, Rab\} | ||
\] | ||
\end{enumerate} | ||
\end{defn} | ||
|
||
\begin{defn} | ||
The \emph{transitive closure}~$R^+$ of a relation $R$ is $R^+ = \bigcup_{i=1}^\infty R^i$ where $R^1 = R$ and $R^{i+1} = R^i \mid R$. | ||
|
||
The reflexive transitive closure~$R^*$ of $R$ is $R* = R^+ \cup I_{\dom{R}}$. | ||
\end{defn} | ||
|
||
\begin{prob} | ||
Show that the transitive closure of $R$ is in fact transitive. | ||
\end{prob} | ||
|
||
\end{document} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
\documentclass[modal-logic]{subfiles} | ||
|
||
\begin{document} | ||
|
||
\section{Axiom Systems for Normal Modal Logics} | ||
|
||
One way of specifying normal modal logics as the set of formulas provable in certain proof systems. The simplest and historically oldest proof systems are so-called Hilbert-type axiomatic proof systems. Hilbert-type proof systems for many normal modal logics are relatively easy to construct, they are simple as objects of metatheoretical study (e.g., to prove soundness and completeness), but they are much harder to use to prove formulas in than, say, natural deduction systems. | ||
|
||
In Hilbert-type proof systems, a derivation of a formula is a sequence of formulas leading from certain axioms, via a handful of inference rules, to the formula in question. For normal modal logics, there are only two inference rules that need to be assumed: modus ponens and necessitation. A axioms we take all (substitution instances) of tautologies, and, depending on the modal logic we deal with, a number of modal axioms. In order to generate a normal modal logic, all substitution instances of K and Dual count as axioms. This alone generates the minimal normal modal logic~$\Log K$. Additional axioms generate other normal modal logics. | ||
|
||
\begin{defn} | ||
The rule of \emph{modus ponens} is the inference schema | ||
\[ | ||
\infer{!B}{!A & !A \lif !B} | ||
\] | ||
We say a formula $!B$ follows from formulas $!A$, $!C$ by modus ponens iff $!C \ident !A \lif !B$. | ||
\end{defn} | ||
|
||
\begin{defn} | ||
The rule of \emph{necessitation} is the inference schema | ||
\[ | ||
\infer{\Box !A}{!A} | ||
\] | ||
We say the formula $!B$ follows from the formulas $!A$ by necessitation iff $!B \ident \Box !A$. | ||
\end{defn} | ||
|
||
\begin{defn} | ||
A \emph{derivation} from a set of axioms~$\Sigma$ is a sequence of formulas $!B_1$, $!B_2$, \dots, $!B_n$, where each $!B_i$ is either | ||
\begin{enumerate} | ||
\item a substitution instance of a tautology, or | ||
\item a substitution instance of a formula in~$\Sigma$, or | ||
\item follows from two formulas $!B_j$, $!B_k$ with $j, k < i$ by modus ponens, or | ||
\item follows from a formula $!B_j$ with $j < i$ by necessitation. | ||
\end{enumerate} | ||
If there is such a derivation with $!B_n \ident !A$, we say that $!A$ is \emph{$\Sigma$-derivable}, in symbols $\Deriv{\Sigma} !A$. | ||
\end{defn} | ||
|
||
\end{document} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
\documentclass[modal-logic]{subfiles} | ||
|
||
\begin{document} | ||
|
||
\section{The Language of Basic Modal Logic} | ||
|
||
The basic language of modal logic contains propositional variables | ||
$p$, $q$, \dots, $\bot$ (the falsity symbol), the familiar logical connective $\lnot$ (``not''), | ||
$\land$ (``and''), $\lor$ (``or''), $\lif$, (``if\dots then''), as | ||
well as the two basic modalities $\Box$ and $\Diamond$. | ||
|
||
\begin{defn} | ||
\emph{Formulas} of the basic modal language are inductively defined as follows: | ||
\begin{enumerate} | ||
\item Every propositional variable $p \in \Var$ is an (atomic) formula. | ||
\item $\bot$ is an (atomic) formula. | ||
\item If $!A$ is a formula, so is $\lnot !A$. | ||
\item If $!A$ and $!B$ are formulas, so are $(!A \land !B)$, $(!A \lor !B)$, and $(!A \lif !B)$. | ||
\item If $!A$ is a formula, so are $\Box !A$ and $\Diamond !A$. | ||
\end{enumerate} | ||
\end{defn} | ||
|
||
% modal depth | ||
|
||
\end{document} |
Oops, something went wrong.