First-order logic

Beyond First-order Logic

content/first-order-logic/beyond/beyond.tex

% Part: first-order-logic% Chapter: beyond\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{fol}{byd}{Beyond First-order Logic}\begin{editorial}  This chapter, adapted from Jeremy Avigad's logic notes, gives the  briefest of glimpses into which other logical systems there are. It  is intended as a chapter suggesting further topics for study in a  course that does not cover them.  Each one of the topics mentioned  here will---hopefully---eventually receive its own part-level  treatment in the Open Logic Project.\end{editorial}\olimport{introduction}\olimport{many-sorted-logic}\olimport{second-order-logic}\olimport{higher-order-logic}\olimport{intuitionistic-logic}\olimport{modal-logics}\olimport{other-logics}\OLEndChapterHook\end{document}

content/first-order-logic/beyond/introduction.tex

% Part: first-order-logic% Chapter: beyond% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{int}\olsection{Overview}First-order logic is not the only system of logic of interest: thereare many extensions and variations of first-order logic. A logictypically consists of the formal specification of a language, usually,but not always, a deductive system, and usually, but not always, anintended semantics. But the technical use of the term raises anobvious question: what do logics that are not first-order logic haveto do with the word ``logic,'' used in the intuitive or philosophicalsense? All of the systems described below are designed to modelreasoning of some form or another; can we say what makes them logical?No easy answers are forthcoming. The word ``logic'' is used indifferent ways and in different contexts, and the notion, like that of``truth,'' has been analyzed from numerous philosophical stances. Forexample, one might take the goal of logical reasoning to be thedetermination of which statements are necessarily true, true a priori,true independent of the interpretation of the nonlogical terms, trueby virtue of their form, or true by linguistic convention; and each ofthese conceptions requires a good deal of clarification. Even if onerestricts one's attention to the kind of logic used in mathematics,there is little agreement as to its scope. For example, in the\textit{Principia Mathematica}, Russell and Whitehead tried to developmathematics on the basis of logic, in the {\em logicist} traditionbegun by Frege. Their system of logic was a form of higher-type logicsimilar to the one described below. In the end they were forced tointroduce axioms which, by most standards, do not seem purely logical(notably, the axiom of infinity, and the axiom of reducibility), butone might nonetheless hold that some forms of higher-order reasoningshould be accepted as logical. In contrast, Quine, whose ontology doesnot admit ``propositions'' as legitimate objects of discourse, arguesthat second-order and higher-order logic are really manifestations ofset theory in sheep's clothing; in other words, systems involvingquantification over predicates are not purely logical.For now, it is best to leave such philosophical issues for a rainyday, and simply think of the systems below as formal idealizations ofvarious kinds of reasoning, logical or otherwise.\end{document}

content/first-order-logic/beyond/many-sorted-logic.tex

% Part: first-order-logic% Chapter: beyond% Section: many-sorted-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{msl}\olsection{Many-Sorted Logic}In first-order logic, variables and quantifiers range over a single!!{domain}. But it is often useful to have multiple (disjoint)!!{domain}s: for example, you might want to have !!a{domain} of numbers,!!a{domain} of geometric objects, !!a{domain} of functions fromnumbers to numbers, !!a{domain} of abelian groups, and so on.Many-sorted logic provides this kind of framework. One starts with alist of ``sorts''---the ``sort'' of an object indicates the``!!{domain}'' it is supposed to inhabit. One then has !!{variable}sand quantifiers for each sort, and (usually) an !!{identity} for eachsort. Functions and relations are also ``typed'' by the sorts ofobjects they can take as arguments. Otherwise, one keeps the usualrules of first-order logic, with versions of the quantifier-rulesrepeated for each sort.For example, to study international relations we might choose alanguage with two sorts of objects, French citizens and Germancitizens. We might have a unary relation, ``drinks wine,'' for objectsof the first sort; another unary relation, ``eats wurst,'' for objectsof the second sort; and a binary relation, ``forms a multinationalmarried couple,'' which takes two arguments, where the first argumentis of the first sort and the second argument is of the second sort. Ifwe use variables $a$, $b$, $c$ to range over French citizens and $x$, $y$, $z$to range over German citizens, then\[\lforall[a][\lforall x][(\Atom{\Obj{MarriedTo}}{a,x} \lif(\Atom{\Obj{DrinksWine}}{a} \lor \lnot \Atom{\Obj{EatsWurst}}{x})]]\]asserts that if any French person is married to a German, either theFrench person drinks wine or the German doesn't eat wurst.Many-sorted logic can be embedded in first-order logic in a naturalway, by lumping all the objects of the many-sorted !!{domain}s togetherinto one first-order !!{domain}, using unary !!{predicate}s to keep track ofthe sorts, and relativizing quantifiers. For example, the first-orderlanguage corresponding to the example above would have unary !!{predicate}s``$\Obj{German}$'' and ``$\Obj{French}$,'' in addition to the other relationsdescribed, with the sort requirements erased. A sorted quantifier $\lforall[x][!A]$, where $x$ is !!a{variable} of the German sort, translates to\[\lforall[x][(\Atom{\Obj{German}}{x} \lif !A)].\]We need to add axioms that insure that the sorts are separate---e.g.,$\lforall[x][\lnot (\Atom{\Obj{German}}{x} \land  \Atom{\Obj{French}}{x})]$---as well as axioms that guarantee that``drinks wine'' only holds of objects satisfying the predicate$\Atom{\Obj{French}}{x}$, etc. With these conventions and axioms, itis not difficult to show that many-sorted !!{sentence}s translate tofirst-order !!{sentence}s, and many-sorted !!{derivation}s translateto first-order !!{derivation}s. Also, many-sorted !!{structure}s``translate'' to corresponding first-order !!{structure}s andvice-versa, so we also have a completeness theorem for many-sortedlogic.\end{document}

content/first-order-logic/beyond/second-order-logic.tex

% Part: first-order-logic% Chapter: beyond% Section: second-order-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{sol}\olsection{Second-Order logic}The language of second-order logic allows one to quantify not justover !!a{domain} of individuals, but over relations on that!!{domain} as well. Given a first-order language $\Lang{L}$, for each$k$ one adds !!{variable}s $R$ which range over $k$-ary relations, andallows quantification over those variables. If $R$ is !!a{variable} for a$k$-ary relation, and $t_1$, \dots,~$t_k$ are ordinary (first-order) terms,$\Atom{R}{t_1,\dots,t_k}$ is an atomic !!{formula}. Otherwise, the set of!!{formula}s is defined just as in the case of first-order logic, withadditional clauses for second-order quantification. Note that we onlyhave the !!{identity} for first-order terms: if $R$ and $S$ are relation!!{variable}s of the same arity~$k$, we can define $\eq[R][S]$ to be anabbreviation for\[\lforall[x_1 \dots][\lforall[x_k][(\Atom{R}{x_1, \dots, x_k} \liff  \Atom{S}{x_1, \dots, x_k})]].\]The rules for second-order logic simply extend the quantifier rules tothe new second order variables. Here, however, one has to be a littlebit careful to explain how these variables interact with the !!{predicate}sof~$\Lang{L}$, and with !!{formula}s of~$\Lang{L}$ more generally. At the bareminimum, relation variables count as terms, so one has inferences ofthe form\[!A(R) \Proves \lexists[R][!A(R)]\]But if $\Lang{L}$ is the language of arithmetic with a constantrelation symbol~$<$, one would also expect the following inference tobe valid:\[x < y \Proves \lexists[R][\Atom{R}{x,y}]\]or for a given !!{formula}~$!A$,\[!A(x_1, \dots, x_k) \Proves \lexists[R][\Atom{R}{x_1,\dots,x_k}]\]More generally, we might want to allow inferences of the form\[\Subst{!A}{\lambd[\vec x][!B(\vec x)]}{R} \Proves\lexists[R][!A]\]where $\Subst{!A}{\lambd[\vec x][!B(\vec x)]}{R}$ denotes the resultof replacing every atomic !!{formula} of the form$\Obj{R}{t_1,\dots,t_k}$ in~$!A$ by $!B(t_1, \dots, t_k)$. This lastrule is equivalent to having a {\em comprehension schema}, i.e., anaxiom of the form\[\lexists[R][\lforall[x_1, \dots, x_k][(!A(x_1, \dots, x_k) \liff\Atom{R}{x_1, \dots, x_k})]],\]one for each !!{formula}~$!A$ in the second-order language, in which$R$ is not a free variable. (Exercise: show that if $R$ is allowed tooccur in~$!A$, this schema is inconsistent!)When logicians refer to the ``axioms of second-order logic'' theyusually mean the minimal extension of first-order logic bysecond-order quantifier rules together with the comprehensionschema. But it is often interesting to study weaker subsystems ofthese axioms and rules. For example, note that in its full generalitythe axiom schema of comprehension is \emph{impredicative}: it allowsone to assert the existence of a relation $\Atom{R}{x_1, \dots, x_k}$that is ``defined'' by !!a{formula} with second-order quantifiers; andthese quantifiers range over the set of all such relations---a setwhich includes $R$ itself!{} Around the turn of the twentieth century, acommon reaction to Russell's paradox was to lay the blame on suchdefinitions, and to avoid them in developing the foundations ofmathematics. If one prohibits the use of second-order quantifiers inthe !!{formula}~$!A$, one has a {\em predicative} form ofcomprehension, which is somewhat weaker.From the semantic point of view, one can think of a second-order!!{structure} as consisting of a first-order !!{structure} for thelanguage, coupled with a set of relations on the !!{domain} over whichthe second-order quantifiers range (more precisely, for each $k$ thereis a set of relations of arity~$k$). Of course, if comprehension isincluded in the !!{derivation} system, then we have the added requirement thatthere are enough relations in the ``second-order part'' to satisfy thecomprehension axioms---otherwise the !!{derivation} system is not sound!{} Oneeasy way to ensure that there are enough relations around is to takethe second-order part to consist of \emph{all} the relations on thefirst-order part. Such !!a{structure} is called \emph{full}, and, in asense, is really the ``intended !!{structure}'' for the language. Ifwe restrict our attention to full !!{structure}s we have what is knownas the \emph{full} second-order semantics. In that case, specifying a!!{structure} boils down to specifying the first-order part, since thecontents of the second-order part follow from that implicitly.To summarize, there is some ambiguity when talking about second-orderlogic. In terms of the !!{derivation} system, one might have in mind either\begin{enumerate}\item A ``minimal'' second-order !!{derivation} system, together with some  comprehension axioms.\item The ``standard'' second-order !!{derivation} system, with full  comprehension.\end{enumerate}In terms of the semantics, one might be interested in either\begin{enumerate}\item The ``weak'' semantics, where !!a{structure} consists of a first-order  part, together with a second-order part big enough to satisfy the  comprehension axioms.\item The ``standard'' second-order semantics, in which one considers  full !!{structure}s only.\end{enumerate}When logicians do not specify the !!{derivation} system or the semantics theyhave in mind, they are usually referring to the second item on eachlist. The advantage to using this semantics is that, as we will see,it gives us categorical descriptions of many natural mathematicalstructures; at the same time, the !!{derivation} system is quite strong, andsound for this semantics. The drawback is that the !!{derivation} system is\emph{not} complete for the semantics; in fact, \emph{no} effectivelygiven !!{derivation} system is complete for the full second-order semantics. Onthe other hand, we will see that the !!{derivation} system \emph{is} completefor the weakened semantics; this implies that if a sentence is notprovable, then there is \emph{some} !!{structure}, not necessarily thefull one, in which it is false.The language of second-order logic is quite rich. One can identifyunary relations with subsets of the !!{domain}, and so in particular youcan quantify over these sets; for example, one can express inductionfor the natural numbers with a single axiom\[\lforall[R][((\Atom{R}{\Obj{0}} \land \lforall[x][(\Atom{R}{x} \lif    \Atom{R}{x'})]) \lif \lforall[x][\Atom{R}{x}])].\]If one takes the language of arithmetic to have symbols $\Obj 0, \Obj \prime, +,\times$ and $<$, one can add the following axioms to describe theirbehavior:\begin{enumerate}\item $\lforall[x][\lnot x' = \Obj 0]$\item $\lforall[x][\lforall[y][(s(x) = s(y) \lif x = y)]]$\item $\lforall[x][(x + \Obj 0) = x]$\item $\lforall[x][\lforall[y][(x + y') = (x + y)']]$\item $\lforall[x][(x \times \Obj 0) = \Obj 0]$\item $\lforall[x][\lforall[y][(x \times y') = ((x \times y) + x)]]$\item $\lforall[x][\lforall[y][(x < y \liff \lexists[z][y = (x + z')])]]$\end{enumerate}It is not difficult to show that these axioms, together with the axiomof induction above, provide a categorical description of the!!{structure}~$\Struct{N}$, the standard model of arithmetic, providedwe are using the full second-order semantics. Given any!!{structure}~$\Struct{M}$ in which these axioms are true, define afunction~$f$ from $\Nat$ to the !!{domain} of $\Struct{M}$ usingordinary recursion on $\Nat$, so that $f(0) = \Assign{\Obj 0}{M}$ and$f(x+1) = \Assign{\prime}{M}(f(x))$. Using ordinary inductionon~$\Nat$ and the fact that axioms (1) and~(2) hold in~$\Struct M$, wesee that $f$ is !!{injective}. To see that $f$ is !!{surjective},let~$P$ be the set of elements of~$\Domain{M}$ that are in the rangeof~$f$. Since $\Struct M$ is full, $P$ is in the second-order!!{domain}. By the construction of~$f$, we know that $\Assign{\Obj  0}{M}$ is in~$P$, and that $P$~is closed under$\Assign{\prime}{M}$. The fact that the induction axiom holds in$\Struct M$ (in particular, for~$P$) guarantees that $P$~is equal tothe entire first-order !!{domain} of~$\Struct M$. This shows that $f$is !!a{bijection}. Showing that $f$ is a homomorphism is no moredifficult, using ordinary induction on $\Nat$ repeatedly.In set-theoretic terms, a function is just a special kind of relation;for example, a unary function~$f$ can be identified with a binaryrelation~$R$ satisfying $\lforall[x][\lexists![y][R(x,y)]]$. As a result, onecan quantify over functions too. Using the full semantics, one canthen define the class of infinite !!{structure}s to be the class of!!{structure}s $\Struct M$ for which there is an injective function from the!!{domain} of $\Struct M$ to a proper subset of itself:\[\lexists[f][(\lforall[x][\lforall[y][(\eq[f(x)][f(y)] \lif \eq[x][y])]]  \land \lexists[y][\lforall[x][\eq/[f(x)][y]]])].\]The negation of this sentence then defines the class of finite!!{structure}s.In addition, one can define the class of well-orderings, by adding thefollowing to the definition of a linear ordering:\[\lforall[P][(\lexists[x][\Atom{P}{x}] \lif \lexists[x][(\Atom{P}{x}    \land \lforall[y][(y < x \lif \lnot \Atom{P}{y})])])].\]This asserts that every non-empty set has a least element, modulo theidentification of ``set'' with ``one-place relation''. For anotherexample, one can express the notion of connectedness for graphs, bysaying that there is no nontrivial separation of the vertices intodisconnected parts:\[\lnot \lexists[A][(\lexists[x][A(x)] \land \lexists[y][\lnot A(y)]  \land \lforall[w][\lforall[z][((\Atom{A}{w} \land \lnot \Atom{A}{z})      \lif \lnot \Atom{R}{w,z})]])].\]For yet another example, you might try as an exercise to define theclass of finite !!{structure}s whose !!{domain} has even size. Morestrikingly, one can provide a categorical description of the realnumbers as a complete ordered field containing the rationals.In short, second-order logic is much more expressive than first-orderlogic. That's the good news; now for the bad. We have alreadymentioned that there is no effective !!{derivation} system that is complete forthe full second-order semantics. For better or for worse, many of theproperties of first-order logic are absent, including compactness andthe L\"owenheim--Skolem theorems.On the other hand, if one is willing to give up the full second-ordersemantics in terms of the weaker one, then the minimal second-order!!{derivation} system is complete for this semantics. In other words, if weread $\Proves$ as ``proves in the minimal system'' and $\Entails$ as``logically implies in the weaker semantics'', we can show thatwhenever $\Gamma \Entails !A$ then $\Gamma \Proves !A$. If one wantsto include specific comprehension axioms in the !!{derivation} system, one hasto restrict the semantics to second-order structures that satisfythese axioms: for example, if $\Delta$ consists of a set ofcomprehension axioms (possibly all of them), we have that if $\Gamma\cup \Delta \Entails !A$, then $\Gamma \cup \Delta \Proves !A$. Inparticular, if $!A$ is not provable using the comprehension axioms weare considering, then there is a model of $\lnot !A$ in which thesecomprehension axioms nonetheless hold.The easiest way to see that the completeness theorem holds for theweaker semantics is to think of second-order logic as a many-sortedlogic, as follows. One sort is interpreted as the ordinary``first-order'' !!{domain}, and then for each $k$ we have !!a{domain}of ``relations of arity $k$.'' We take the language to have built-inrelation symbols ``$\Atom{\Obj{true}_k}{R,x_1,\dots,x_k}$'' which ismeant to assert that $R$ holds of $x_1$, \dots,~$x_k$, where $R$ is avariable of the sort ``$k$-ary relation'' and $x_1$, \dots,~$x_k$ areobjects of the first-order sort.With this identification, the weak second-order semantics is essentiallythe usual semantics for many-sorted logic; and we have alreadyobserved that many-sorted logic can be embedded in first-order logic.Modulo the translations back and forth, then, the weaker conception ofsecond-order logic is really a form of first-order logic in disguise,where the !!{domain} contains both ``objects'' and ``relations''governed by the appropriate axioms.\end{document}

content/first-order-logic/beyond/higher-order-logic.tex

% Part: first-order-logic% Chapter: beyond% Section: higher-order-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{hol}\olsection{Higher-Order logic}Passing from first-order logic to second-order logic enabled us totalk about sets of objects in the first-order !!{domain}, within theformal language. Why stop there? For example, third-order logic shouldenable us to deal with sets of sets of objects, or perhaps even setswhich contain both objects and sets of objects. And fourth-order logicwill let us talk about sets of objects of that kind. As you may haveguessed, one can iterate this idea arbitrarily.In practice, higher-order logic is often !!{formula}ted in terms offunctions instead of relations. (Modulo the natural identifications,this difference is inessential.) Given some basic ``sorts'' $A$, $B$,$C$,~\dots (which we will now call ``types''), we can create new onesby stipulating\begin{quote}If $\sigma$ and $\tau$ are finite types then so is $\sigma \to \tau$.\end{quote}Think of types as syntactic ``labels,'' which classify the objects wewant in our !!{domain}; $\sigma \to \tau$ describes those objects thatare functions which take objects of type~$\sigma$ to objects oftype~$\tau$. For example, we might want to have a type $\Omega$ oftruth values, ``true'' and ``false,'' and a type $\Nat$ of naturalnumbers. In that case, you can think of objects of type $\Nat \to\Omega$ as unary relations, or subsets of $\Nat$; objects of type$\Nat \to \Nat$ are functions from natural numbers to natural numbers;and objects of type $(\Nat \to \Nat) \to \Nat$ are ``functionals,''that is, higher-type functions that take functions to numbers.As in the case of second-order logic, one can think of higher-orderlogic as a kind of many-sorted logic, where there is a sort for eachtype of object we want to consider. But it is usually clearer just todefine the syntax of higher-type logic from the ground up. Forexample, we can define a set of finite types inductively, as follows:\begin{enumerate}\item $\Nat$ is a finite type.\item If $\sigma$ and $\tau$ are finite types, then so is $\sigma  \to \tau$.\item If $\sigma$ and $\tau$ are finite types, so is $\sigma \times  \tau$.\end{enumerate}Intuitively, $\Nat$ denotes the type of the natural numbers,$\sigma \to \tau$ denotes the type of functions from $\sigma$ to$\tau$, and $\sigma \times \tau$ denotes the type of pairs of objects,one from $\sigma$ and one from $\tau$. We can then define a set ofterms inductively, as follows:\begin{enumerate}\item For each type $\sigma$, there is a stock of variables $x$, $y$,  $z$, \dots of type $\sigma$\item $\Obj 0$ is a term of type $\Nat$\item $\Obj S$ (successor) is a term of type $\Nat \to \Nat$\item If $s$ is a term of type $\sigma$, and $t$ is a term of type  $\Nat \to (\sigma \to \sigma)$, then $\Obj{R}_{st}$ is a term of type  $\Nat \to \sigma$\item If $s$ is a term of type $\tau \to \sigma$ and $t$ is a  term of type~$\tau$, then $s(t)$ is a term of type $\sigma$\item If $s$ is a term of type~$\sigma$ and $x$ is a variable of  type~$\tau$, then $\lambd[x][s]$ is a term of type $\tau \to \sigma$.\item If $s$ is a term of type~$\sigma$ and $t$ is a term of  type~$\tau$, then $\tuple{s, t}$ is a term of type $\sigma \times  \tau$.\item If $s$ is a term of type~$\sigma \times \tau$ then $p_1(s)$ is a  term of type~$\sigma$ and $p_2(s)$ is a term of type~$\tau$.\end{enumerate}Intuitively, $\Obj{R}_{st}$ denotes the function defined recursively by\begin{align*}\Obj{R}_{st}(0) & = s \\\Obj{R}_{st}(x+1) & = t(x, R_{st}(x)),\end{align*}$\tuple{s, t}$ denotes the pair whose first component is~$s$ and whosesecond component is~$t$, and $p_1(s)$ and~$p_2(s)$ denote the firstand second elements (``projections'') of~$s$. Finally, $\lambd[x][s]$denotes the function~$f$ defined by\[f(x) = s\]for any~$x$ of type~$\sigma$; so item (6) gives us a form ofcomprehension, enabling us to define functions usingterms. !!^{formula}s are built up from !!{identity} statements $\eq[s][t]$between terms of the same type, the usual propositional connectives,and higher-type quantification. One can then take the axioms of thesystem to be the basic equations governing the terms defined above,together with the usual rules of logic with quantifiers and !!{identity}.If one augments the finite type system with a type $\Omega$ of truthvalues, one has to include axioms which govern its use as well. Infact, if one is clever, one can get rid of complex !!{formula}sentirely, replacing them with terms of type $\Omega$!{} The proofsystem can then be modified accordingly. The result is essentially the\emph{simple theory of types} set forth by Alonzo Church in the 1930s.As in the case of second-order logic, there are different versions ofhigher-type semantics that one might want to use. In the full version,variables of type $\sigma \to \tau$ range over the set of \emph{all}functions from the objects of type~$\sigma$ to objects of type~$\tau$.As you might expect, this semantics is too strong to admit a complete,effective !!{derivation} system. But one can consider a weaker semantics, inwhich !!a{structure} consists of sets of elements $T_\tau$ for eachtype $\tau$, together with appropriate operations for application,projection, etc. If the details are carried out correctly, one canobtain completeness theorems for the kinds of !!{derivation} systems describedabove.Higher-type logic is attractive because it provides a framework inwhich we can embed a good deal of mathematics in a natural way:starting with $\Nat$, one can define real numbers, continuousfunctions, and so on. It is also particularly attractive in thecontext of intuitionistic logic, since the types have clear``constructive'' interpretations. In fact, one can develop constructiveversions of higher-type semantics (based on intuitionistic, ratherthan classical logic) that clarify these constructive interpretationsquite nicely, and are, in many ways, more interesting than theclassical counterparts.\end{document}

content/first-order-logic/beyond/intuitionistic-logic.tex

% Part: first-order-logic% Chapter: beyond% Section: intuitionistic-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{il}\olsection{Intuitionistic Logic}In contrast to second-order and higher-order logic, intuitionisticfirst-order logic represents a restriction of the classical version,intended to model a more ``constructive'' kind of reasoning. Thefollowing examples may serve to illustrate some of the underlyingmotivations.Suppose someone came up to you one day and announced that they haddetermined a natural number~$x$, with the property that if $x$ isprime, the Riemann hypothesis is true, and if $x$ is composite, theRiemann hypothesis is false. Great news!{} Whether the Riemannhypothesis is true or not is one of the big open questions ofmathematics, and here they seem to have reduced the problem to one ofcalculation, that is, to the determination of whether a specificnumber is prime or not.What is the magic value of $x$? They describe it as follows: $x$ isthe natural number that is equal to $7$ if the Riemann hypothesis istrue, and $9$ otherwise.Angrily, you demand your money back. From a classical point of view,the description above does in fact determine a unique value of $x$;but what you really want is a value of $x$ that is given\emph{explicitly}.To take another, perhaps less contrived example, consider thefollowing question. We know that it is possible to raise an irrationalnumber to a rational power, and get a rational result. For example,$\sqrt{2}^2 = 2$. What is less clear is whether or not it is possibleto raise an irrational number to an \emph{irrational} power, and get arational result. The following theorem answers this in theaffirmative:\begin{thm}There are irrational numbers $a$ and $b$ such that $a^b$ is rational.\end{thm}\begin{proof}Consider $\sqrt{2}^{\sqrt{2}}$. If this is rational, we are done:we can let $a = b = \sqrt{2}$. Otherwise, it is irrational. Then wehave\[(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2} \cdot  \sqrt{2}} = \sqrt{2}^2 = 2,\]which is certainly rational. So, in this case, let $a$ be$\sqrt{2}^{\sqrt{2}}$, and let $b$ be~$\sqrt 2$.\end{proof}Does this constitute a valid proof? Most mathematicians feel that itdoes. But again, there is something a little bit unsatisfying here: wehave proved the existence of a pair of real numbers with a certainproperty, without being able to say \emph{which} pair of numbers itis.  It is possible to prove the same result, but in such a way thatthe pair $a$, $b$ \emph{is} given in the proof: take $a = \sqrt{3}$and $b = \log_3 4$. Then\[a^b = \sqrt{3}^{\log_3 4} = 3^{1/2 \cdot \log_3 4} = (3^{\log_3  4})^{1/2} = 4^{1/2}= 2,\]since $3^{\log_3 x} = x$.Intuitionistic logic is designed to model a kind of reasoning wheremoves like the one in the first proof are disallowed. Proving theexistence of an $x$ satisfying~$!A(x)$ means that you have to give aspecific~$x$, and a proof that it satisfies $!A$, like in the secondproof. Proving that $!A$ or $!B$ holds requires that you can prove oneor the other.Formally speaking, intuitionistic first-order logic is what you get ifyou restrict !!a{derivation} system for first-order logic in a certainway. Similarly, there are intuitionistic versions of second-order orhigher-order logic. From the mathematical point of view, these arejust formal deductive systems, but, as already noted, they areintended to model a kind of mathematical reasoning. One can take thisto be the kind of reasoning that is justified on a certainphilosophical view of mathematics (such as Brouwer's intuitionism);one can take it to be a kind of mathematical reasoning which is more``concrete'' and satisfying (along the lines of Bishop'sconstructivism); and one can argue about whether or not the formaldescription captures the informal motivation. But whateverphilosophical positions we may hold, we can study intuitionistic logicas a formally presented logic; and for whatever reasons, manymathematical logicians find it interesting to do so.There is an informal constructive interpretation of the intuitionistconnectives, usually known as the BHK interpretation (named afterBrouwer, Heyting, and Kolmogorov). It runs as follows: a proof of $!A\land !B$ consists of a proof of $!A$ paired with a proof of $!B$; aproof of $!A \lor !B$ consists of either a proof of $!A$, or a proofof $!B$, where we have explicit information as to which is the case; aproof of $!A \lif !B$ consists of a procedure, which transforms aproof of $!A$ to a proof of~$!B$; a proof of $\lforall[x][!A(x)]$consists of a procedure which returns a proof of $!A(x)$ for any valueof~$x$; and a proof of $\lexists[x][!A(x)]$ consists of a valueof~$x$, together with a proof that this value satisfies~$!A$. One candescribe the interpretation in computational terms known as the``Curry--Howard isomorphism'' or the ``!!{formula}s-as-typesparadigm'': think of !!a{formula} as specifying a certain kind ofdata type, and proofs as computational objects of these data typesthat enable us to see that the corresponding !!{formula} is true.Intuitionistic logic is often thought of as being classical logic``minus'' the law of the excluded middle. This following theorem makesthis more precise.\begin{thm}Intuitionistically, the following axiom schemata are equivalent:\begin{enumerate}\item $(\lnot !A \lif \lfalse) \lif !A$.\item $!A \lor \lnot !A$\item $\lnot \lnot !A \lif !A$\end{enumerate}\end{thm}Obtaining instances of one schema from either of the others is a goodexercise in intuitionistic logic.The first deductive systems for intuitionistic propositionallogic, put forth as formalizations of Brouwer's intuitionism, are due,independently, to Kolmogorov, Glivenko, and Heyting. The firstformalization of intuitionistic first-order logic (and parts ofintuitionist mathematics) is due to Heyting. Though a number ofclassically valid schemata are not intuitionistically valid, many are.The \emph{double-negation translation} describes an importantrelationship between classical and intuitionist logic. It is definedinductively follows (think of $!A^N$ as the ``intuitionist''translation of the classical !!{formula}~$!A$):\begin{align*}!A^N & \ident \lnot\lnot !A \quad \text{for atomic !!{formula}s $!A$} \\(!A \land !B)^N & \ident (!A^N \land !B^N) \\(!A \lor !B)^N & \ident  \lnot\lnot (!A^N \lor !B^N) \\(!A \lif !B)^N & \ident (!A^N \lif !B^N) \\(\lforall[x][!A])^N & \ident \lforall[x][!A^N] \\(\lexists[x][!A])^N & \ident \lnot\lnot\lexists[x][!A^N]\end{align*}Kolmogorov and Glivenko had versions of this translation forpropositional logic; for predicate logic, it is due to G\"odel andGentzen, independently. We have\begin{thm}\begin{enumerate}\item $!A \liff !A^N$ is provable classically\item If $!A$ is provable classically, then $!A^N$ is provable  intuitionistically.\end{enumerate}\end{thm}We can now envision the following dialogue. Classical mathematician:``I've proved $!A$!'' Intuitionist mathematician: ``Your proof isn'tvalid. What you've really proved is $!A^N$.'' Classical mathematician:``Fine by me!'' As far as the classical mathematician is concerned, theintuitionist is just splitting hairs, since the two areequivalent. But the intuitionist insists there is a difference.Note that the above translation concerns pure logic only; it does notaddress the question as to what the appropriate \emph{nonlogical}axioms are for classical and intuitionistic mathematics, or what therelationship is between them. But the following slight extension ofthe theorem above provides some useful information:\begin{thm}If $\Gamma$ proves $!A$ classically, $\Gamma^N$ proves $!A^N$intuitionistically.\end{thm}In other words, if $!A$ is provable from some hypotheses classically,then $!A^N$ is provable from their double-negation translations.To show that a sentence or propositional !!{formula} is intuitionisticallyvalid, all you have to do is provide a proof. But how can you showthat it is not valid? For that purpose, we need a semanticsthat is sound, and preferably complete. A semanticsdue to Kripke nicely fits the bill.We can play the same game we did for classical logic: define thesemantics, and prove soundness and completeness. It is worthwhile,however, to note the following distinction. In the case of classicallogic, the semantics was the ``obvious'' one, in a sense implicit inthe meaning of the connectives. Though one can provide some intuitivemotivation for Kripke semantics, the latter does not offer the samefeeling of inevitability. In addition, the notion of a classical!!{structure} is a natural mathematical one, so we can either take thenotion of !!a{structure} to be a tool for studying classical first-orderlogic, or take classical first-order logic to be a tool for studyingmathematical !!{structure}s. In contrast, Kripke !!{structure}s can only beviewed as a logical construct; they don't seem to have independentmathematical interest.A Kripke !!{structure}~$\mModel M = \tuple{W, R, V}$ for a propositionallanguage consists of a set~$W$, partial order~$R$ on~$W$ with a least!!{element}, and an ``monotone'' assignment of propositional variables tothe !!{element}s of~$W$. The intuition is that the !!{element}s of $W$represent ``worlds,'' or ``states of knowledge''; an element $v \gequ$ represents a ``possible future state'' of~$u$; and thepropositional variables assigned to~$u$ are the propositions that areknown to be true in state~$u$. The forcing relation $\mSat{M}{!A}[w]$then extends this relationship to arbitrary !!{formula}s in thelanguage; read $\mSat{M}{!A}[w]$ as ``$!A$ is true in state~$w$.'' Therelationship is defined inductively, as follows:\begin{enumerate}\item $\mSat{M}{\Obj p_i}[w]$ iff $\Obj p_i$ is one of the  propositional variables assigned to~$w$.\item $\mSat/{M}{\lfalse}[w]$.\item $\mSat{M}{(!A \land !B)}[w]$ iff $\mSat{M}{!A}[w]$ and $\mSat{M}{!B}[w]$.\item $\mSat{M}{(!A \lor !B)}[w]$ iff $\mSat{M}{!A}[w]$ or $\mSat{M}{!B}[w]$.\item $\mSat{M}{(!A \lif !B)}[w]$ iff, whenever $w' \geq w$ and  $\mSat{M}{!A}[w']$, then $\mSat{M}{!B}[w']$.\end{enumerate}It is a good exercise to try to show that $\lnot (p \land q) \lif(\lnot p \lor \lnot q)$ is not intuitionistically valid, by cooking up aKripke !!{structure} that provides a counterexample.\end{document}

content/first-order-logic/beyond/modal-logics.tex

% Part: first-order-logic% Chapter: beyond% Section: modal-logics\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{mod}\olsection{Modal Logics}Consider the following example of a conditional sentence:\begin{quote}  If Jeremy is alone in that room, then he is drunk and naked and  dancing on the chairs.\end{quote}This is an example of a conditional assertion that may be materiallytrue but nonetheless misleading, since it seems to suggest that thereis a stronger link between the antecedent and conclusion other thansimply that either the antecedent is false or the consequenttrue. That is, the wording suggests that the claim is not only true inthis particular world (where it may be trivially true, because Jeremyis not alone in the room), but that, moreover, the conclusion\emph{would have} been true \emph{had} the antecedent been true. Inother words, one can take the assertion to mean that the claim is truenot just in this world, but in any ``possible'' world; or that it is\emph{necessarily} true, as opposed to just true in this particularworld.Modal logic was designed to make sense of this kind of necessity. Oneobtains modal propositional logic from ordinarypropositional logic by adding a box operator; which is to say, if$!A$ is !!a{formula}, so is $\Box !A$.  Intuitively, $\Box !A$asserts that $!A$ is \emph{necessarily} true, or true in any possibleworld. $\Diamond !A$ is usually taken to be an abbreviation for$\lnot \Box \lnot !A$, and can be read as asserting that $!A$ is\emph{possibly} true. Of course, modality can be added to predicatelogic as well.Kripke !!{structure}s can be used to provide a semantics for modallogic; in fact, Kripke first designed this semantics with modal logicin mind. Rather than restricting to partial orders, more generally onehas a set of ``possible worlds,'' $P$, and a binary ``accessibility''relation $\Atom{R}{x,y}$ between worlds. Intuitively, $\Atom{R}{p,q}$asserts that the world~$q$ is compatible with~$p$; i.e., if we are``in'' world~$p$, we have to entertain the possibility that theworld could have been like~$q$.Modal logic is sometimes called an ``intensional'' logic, as opposedto an ``extensional'' one. The intended semantics for an extensionallogic, like classical logic, will only refer to a single world, the``actual'' one; while the semantics for an ``intensional'' logicrelies on a more elaborate ontology. In addition to !!{structure}ingnecessity, one can use modality to !!{structure} other linguisticconstructions, reinterpreting $\Box$ and $\Diamond$ according to theapplication. For example:\begin{enumerate}\item In provability logic, $\Box !A$ is read ``$!A$ is provable''  and $\Diamond !A$ is read ``$!A$ is consistent.''\item In epistemic logic, one might read $\Box !A$ as ``I know  $!A$'' or ``I believe $!A$.''\item In temporal logic, one can read $\Box !A$ as ``$!A$ is always  true'' and $\Diamond !A$ as ``$!A$ is sometimes true.''\end{enumerate}One would like to augment logic with rules and axioms dealing withmodality. For example, the system $\Log{S4}$ consists of the ordinaryaxioms and rules of propositional logic, together with the followingaxioms:\begin{align*}& \Box (!A \lif !B) \lif (\Box !A \lif \Box !B)\\& \Box !A \lif !A \\& \Box !A \lif \Box \Box !A\intertext{as well as a rule, ``from $!A$ conclude $\Box !A$.''  $\Log{S5}$ adds the following axiom:}& \Diamond !A \lif \Box \Diamond !A\end{align*}Variations of these axioms may be suitable for different applications;for example, S5 is usually taken to characterize the notion of logicalnecessity. And the nice thing is that one can usually find a semanticsfor which the !!{derivation} system is sound and complete by restricting theaccessibility relation in the Kripke !!{structure}s in naturalways. For example, $\Log{S4}$ corresponds to the class of Kripke!!{structure}s in which the accessibility relation is reflexive andtransitive. $\Log{S5}$ corresponds to the class of Kripke!!{structure}s in which the accessibility relation is {\em universal},which is to say that every world is accessible from every other; so$\Box !A$ holds if and only if $!A$ holds in every world.\end{document}

content/first-order-logic/beyond/other-logics.tex

% Part: first-order-logic% Chapter: beyond% Section: other-logics\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{fol}{byd}{oth}\olsection{Other Logics}As you may have gathered by now, it is not hard to design a new logic.You too can create your own a syntax, make up a deductive system, andfashion a semantics to go with it. You might have to be a bit cleverif you want the !!{derivation} system to be complete for the semantics, and itmight take some effort to convince the world at large that your logicis truly interesting. But, in return, you can enjoy hours of good,clean fun, exploring your logic's mathematical and computationalproperties.Recent decades have witnessed a veritable explosion of formal logics.Fuzzy logic is designed to model reasoning about vagueproperties. Probabilistic logic is designed to modelreasoning about uncertainty. Default logics and nonmonotonic logicsare designed to model defeasible forms of reasoning, which isto say, ``reasonable'' inferences that can later be overturned in theface of new information. There are epistemic logics, designed tomodel reasoning about knowledge; causal logics, designed tomodel reasoning about causal relationships; and even``deontic'' logics, which are designed to model reasoningabout moral and ethical obligations. Depending on whether the primarymotivation for introducing these systems is philosophical,mathematical, or computational, you may find such creatures studiesunder the rubric of mathematical logic, philosophical logic,artificial intelligence, cognitive science, or elsewhere.The list goes on and on, and the possibilities seem endless. Wemay never attain Leibniz' dream of reducing all of human reason tocalculation---but that can't stop us from trying.\end{document}