Beyond First-order Logic

Document

Beyond First-order Logic

olimportintroduction

olimportmany-sorted-logic

olimportsecond-order-logic

olimporthigher-order-logic

olimportintuitionistic-logic

olimportmodal-logics

olimportother-logics

Document

olfileidfolbydint

Overview

First-order logic is not the only system of logic of interest: there are many extensions and variations of first-order logic. A logic typically consists of the formal specification of a language, usually, but not always, a deductive system, and usually, but not always, an intended semantics. But the technical use of the term raises an obvious question: what do logics that are not first-order logic have to do with the word “logic,” used in the intuitive or philosophical sense? All of the systems described below are designed to model reasoning of some form or another; can we say what makes them logical?

No easy answers are forthcoming. The word “logic” is used in different ways and in different contexts, and the notion, like that of “truth,” has been analyzed from numerous philosophical stances. For example, one might take the goal of logical reasoning to be the determination of which statements are necessarily true, true a priori, true independent of the interpretation of the nonlogical terms, true by virtue of their form, or true by linguistic convention; and each of these conceptions requires a good deal of clarification. Even if one restricts one's attention to the kind of logic used in mathematics, there is little agreement as to its scope. For example, in the Principia Mathematica, Russell and Whitehead tried to develop mathematics on the basis of logic, in the em logicist tradition begun by Frege. Their system of logic was a form of higher-type logic similar to the one described below. In the end they were forced to introduce axioms which, by most standards, do not seem purely logical (notably, the axiom of infinity, and the axiom of reducibility), but one might nonetheless hold that some forms of higher-order reasoning should be accepted as logical. In contrast, Quine, whose ontology does not admit “propositions” as legitimate objects of discourse, argues that second-order and higher-order logic are really manifestations of set theory in sheep's clothing; in other words, systems involving quantification over predicates are not purely logical.

For now, it is best to leave such philosophical issues for a rainy day, and simply think of the systems below as formal idealizations of various kinds of reasoning, logical or otherwise.

Document

olfileidfolbydmsl

Many-Sorted Logic

In first-order logic, variables and quantifiers range over a single domain. But it is often useful to have multiple (disjoint) domains: for example, you might want to have a domain of numbers, a domain of geometric objects, a domain of functions from numbers to numbers, a domain of abelian groups, and so on.

Many-sorted logic provides this kind of framework. One starts with a list of “sorts”---the “sort” of an object indicates the “domain” it is supposed to inhabit. One then has variables and quantifiers for each sort, and (usually) an identity predicate for each sort. Functions and relations are also “typed” by the sorts of objects they can take as arguments. Otherwise, one keeps the usual rules of first-order logic, with versions of the quantifier-rules repeated for each sort.

For example, to study international relations we might choose a language with two sorts of objects, French citizens and German citizens. We might have a unary relation, “drinks wine,” for objects of the first sort; another unary relation, “eats wurst,” for objects of the second sort; and a binary relation, “forms a multinational married couple,” which takes two arguments, where the first argument is of the first sort and the second argument is of the second sort. If we use variables $a$source, $b$source, $c$source to range over French citizens and $x$source, $y$source, $z$source to range over German citizens, then

asserts that if any French person is married to a German, either the French person drinks wine or the German doesn't eat wurst.

Many-sorted logic can be embedded in first-order logic in a natural way, by lumping all the objects of the many-sorted domains together into one first-order domain, using unary predicate symbols to keep track of the sorts, and relativizing quantifiers. For example, the first-order language corresponding to the example above would have unary predicate symbols “$\mathrm{German}$source” and “$\mathrm{French}$source,” in addition to the other relations described, with the sort requirements erased. A sorted quantifier $\forall xA$source, where $x$source is a variable of the German sort, translates to

We need to add axioms that insure that the sorts are separate---e.g., $\forall x\neg (\mathrm{German}\left(x\right)\wedge \mathrm{French}\left(x\right))$source---as well as axioms that guarantee that “drinks wine” only holds of objects satisfying the predicate $\mathrm{French}\left(x\right)$source, etc. With these conventions and axioms, it is not difficult to show that many-sorted sentences translate to first-order sentences, and many-sorted derivations translate to first-order derivations. Also, many-sorted structures “translate” to corresponding first-order structures and vice-versa, so we also have a completeness theorem for many-sorted logic.

Document

olfileidfolbydsol

Second-Order logic

The language of second-order logic allows one to quantify not just over a domain of individuals, but over relations on that domain as well. Given a first-order language $L$source, for each $k$source one adds variables $R$source which range over $k$source-ary relations, and allows quantification over those variables. If $R$source is a variable for a $k$source-ary relation, and $t_1$source, dots, $t_k$source are ordinary (first-order) terms, $R\left(t_1,\dots ,t_k\right)$source is an atomic formula. Otherwise, the set of formulas is defined just as in the case of first-order logic, with additional clauses for second-order quantification. Note that we only have the identity predicate for first-order terms: if $R$source and $S$source are relation variables of the same arity $k$source, we can define $R=S$source to be an abbreviation for

The rules for second-order logic simply extend the quantifier rules to the new second order variables. Here, however, one has to be a little bit careful to explain how these variables interact with the predicate symbols of $L$source, and with formulas of $L$source more generally. At the bare minimum, relation variables count as terms, so one has inferences of the form

But if $L$source is the language of arithmetic with a constant relation symbol $<$source, one would also expect the following inference to be valid:

or for a given formula $A$source,

More generally, we might want to allow inferences of the form

where $A[\lambda \overrightarrow{x}.B\left(\overrightarrow{x}\right)/R]$source denotes the result of replacing every atomic formula of the form $R{t}_1,\dots ,t_k$source in $A$source by $B(t_1,\dots ,t_k)$source. This last rule is equivalent to having a em comprehension schema, i.e., an axiom of the form

one for each formula $A$source in the second-order language, in which $R$source is not a free variable. (Exercise: show that if $R$source is allowed to occur in $A$source, this schema is inconsistent!)

When logicians refer to the “axioms of second-order logic” they usually mean the minimal extension of first-order logic by second-order quantifier rules together with the comprehension schema. But it is often interesting to study weaker subsystems of these axioms and rules. For example, note that in its full generality the axiom schema of comprehension is impredicative: it allows one to assert the existence of a relation $R\left(x_1,\dots ,x_k\right)$source that is “defined” by a formula with second-order quantifiers; and these quantifiers range over the set of all such relations---a set which includes $R$source itself! Around the turn of the twentieth century, a common reaction to Russell's paradox was to lay the blame on such definitions, and to avoid them in developing the foundations of mathematics. If one prohibits the use of second-order quantifiers in the formula $A$source, one has a em predicative form of comprehension, 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 the language, coupled with a set of relations on the domain over which the second-order quantifiers range (more precisely, for each $k$source there is a set of relations of arity $k$source). Of course, if comprehension is included in the derivation system, then we have the added requirement that there are enough relations in the “second-order part” to satisfy the comprehension axioms---otherwise the derivation system is not sound! One easy way to ensure that there are enough relations around is to take the second-order part to consist of all the relations on the first-order part. Such a structure is called full, and, in a sense, is really the “intended structure” for the language. If we restrict our attention to full structures we have what is known as the full second-order semantics. In that case, specifying a structure boils down to specifying the first-order part, since the contents of the second-order part follow from that implicitly.

To summarize, there is some ambiguity when talking about second-order logic. In terms of the derivation system, one might have in mind either

1. A “minimal” second-order derivation system, together with some comprehension axioms.

2. The “standard” second-order derivation system, with full comprehension.

In terms of the semantics, one might be interested in either

1. 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.

2. The “standard” second-order semantics, in which one considers full structures only.

When logicians do not specify the derivation system or the semantics they have in mind, they are usually referring to the second item on each list. The advantage to using this semantics is that, as we will see, it gives us categorical descriptions of many natural mathematical structures; at the same time, the derivation system is quite strong, and sound for this semantics. The drawback is that the derivation system is not complete for the semantics; in fact, no effectively given derivation system is complete for the full second-order semantics. On the other hand, we will see that the derivation system is complete for the weakened semantics; this implies that if a sentence is not provable, then there is some structure, not necessarily the full one, in which it is false.

The language of second-order logic is quite rich. One can identify unary relations with subsets of the domain, and so in particular you can quantify over these sets; for example, one can express induction for the natural numbers with a single axiom

If one takes the language of arithmetic to have symbols $0,\prime ,+,\times$source and $<$source, one can add the following axioms to describe their behavior:

1. $\forall x\neg x^{\prime }=0$source

2. $\forall x\forall y\left(s\right(x)=s(y)\to x=y)$source

3. $\forall x(x+0)=x$source

4. $\forall x\forall y(x+y^{\prime })={(x+y)}^{\prime }$source

5. $\forall x(x\times 0)=0$source

6. $\forall x\forall y(x\times y^{\prime })=\left(\right(x\times y)+x)$source

7. $\forall x\forall y(x<y\leftrightarrow \exists zy=(x+z^{\prime }))$source

It is not difficult to show that these axioms, together with the axiom of induction above, provide a categorical description of the structure $N$source, the standard model of arithmetic, provided we are using the full second-order semantics. Given any structure $M$source in which these axioms are true, define a function $f$source from $\mathbb{N}$source to the domain of $M$source using ordinary recursion on $\mathbb{N}$source, so that $f\left(0\right)=0^M$source and $f(x+1)={\prime }^M\left(f\right(x\left)\right)$source. Using ordinary induction on $\mathbb{N}$source and the fact that axioms (1) and (2) hold in $M$source, we see that $f$source is injective. To see that $f$source is surjective, let $P$source be the set of elements of $\left|M\right|$source that are in the range of $f$source. Since $M$source is full, $P$source is in the second-order domain. By the construction of $f$source, we know that $0^M$source is in $P$source, and that $P$source is closed under ${\prime }^M$source. The fact that the induction axiom holds in $M$source (in particular, for $P$source) guarantees that $P$source is equal to the entire first-order domain of $M$source. This shows that $f$source is a bijection. Showing that $f$source is a homomorphism is no more difficult, using ordinary induction on $\mathbb{N}$source repeatedly.

In set-theoretic terms, a function is just a special kind of relation; for example, a unary function $f$source can be identified with a binary relation $R$source satisfying $\forall x\exists !yR(x,y)$source. As a result, one can quantify over functions too. Using the full semantics, one can then define the class of infinite structures to be the class of structures $M$source for which there is an injective function from the domain of $M$source to a proper subset of itself:

The negation of this sentence then defines the class of finite structures.

In addition, one can define the class of well-orderings, by adding the following to the definition of a linear ordering:

This asserts that every non-empty set has a least element, modulo the identification of “set” with “one-place relation”. For another example, one can express the notion of connectedness for graphs, by saying that there is no nontrivial separation of the vertices into disconnected parts:

For yet another example, you might try as an exercise to define the class of finite structures whose domain has even size. More strikingly, one can provide a categorical description of the real numbers as a complete ordered field containing the rationals.

In short, second-order logic is much more expressive than first-order logic. That's the good news; now for the bad. We have already mentioned that there is no effective derivation system that is complete for the full second-order semantics. For better or for worse, many of the properties of first-order logic are absent, including compactness and the L\"owenheim--Skolem theorems.

On the other hand, if one is willing to give up the full second-order semantics in terms of the weaker one, then the minimal second-order derivation system is complete for this semantics. In other words, if we read $⊢$source as “proves in the minimal system” and $\models$source as “logically implies in the weaker semantics”, we can show that whenever $\Gamma \models A$source then $\Gamma ⊢A$source. If one wants to include specific comprehension axioms in the derivation system, one has to restrict the semantics to second-order structures that satisfy these axioms: for example, if $\Delta$source consists of a set of comprehension axioms (possibly all of them), we have that if $\Gamma \cup \Delta \models A$source, then $\Gamma \cup \Delta ⊢A$source. In particular, if $A$source is not provable using the comprehension axioms we are considering, then there is a model of $\neg A$source in which these comprehension axioms nonetheless hold.

The easiest way to see that the completeness theorem holds for the weaker semantics is to think of second-order logic as a many-sorted logic, as follows. One sort is interpreted as the ordinary “first-order” domain, and then for each $k$source we have a domain of “relations of arity $k$source.” We take the language to have built-in relation symbols “${\mathrm{true}}_k\left(R,x_1,\dots ,x_k\right)$source” which is meant to assert that $R$source holds of $x_1$source, dots, $x_k$source, where $R$source is a variable of the sort “$k$source-ary relation” and $x_1$source, dots, $x_k$source are objects of the first-order sort.

With this identification, the weak second-order semantics is essentially the usual semantics for many-sorted logic; and we have already observed that many-sorted logic can be embedded in first-order logic. Modulo the translations back and forth, then, the weaker conception of second-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.

Document

olfileidfolbydhol

Higher-Order logic

Passing from first-order logic to second-order logic enabled us to talk about sets of objects in the first-order domain, within the formal language. Why stop there? For example, third-order logic should enable us to deal with sets of sets of objects, or perhaps even sets which contain both objects and sets of objects. And fourth-order logic will let us talk about sets of objects of that kind. As you may have guessed, one can iterate this idea arbitrarily.

In practice, higher-order logic is often formulated in terms of functions instead of relations. (Modulo the natural identifications, this difference is inessential.) Given some basic “sorts” $A$source, $B$source, $C$source, dots (which we will now call “types”), we can create new ones by stipulating

Think of types as syntactic “labels,” which classify the objects we want in our domain; $\sigma \to \tau$source describes those objects that are functions which take objects of type $\sigma$source to objects of type $\tau$source. For example, we might want to have a type $\Omega$source of truth values, “true” and “false,” and a type $\mathbb{N}$source of natural numbers. In that case, you can think of objects of type $\mathbb{N}\to \Omega$source as unary relations, or subsets of $\mathbb{N}$source; objects of type $\mathbb{N}\to \mathbb{N}$source are functions from natural numbers to natural numbers; and objects of type $(\mathbb{N}\to \mathbb{N})\to \mathbb{N}$source 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-order logic as a kind of many-sorted logic, where there is a sort for each type of object we want to consider. But it is usually clearer just to define the syntax of higher-type logic from the ground up. For example, we can define a set of finite types inductively, as follows:

1. $\mathbb{N}$source is a finite type.

2. If $\sigma$source and $\tau$source are finite types, then so is $\sigma \to \tau$source.

3. If $\sigma$source and $\tau$source are finite types, so is $\sigma \times \tau$source.

Intuitively, $\mathbb{N}$source denotes the type of the natural numbers, $\sigma \to \tau$source denotes the type of functions from $\sigma$source to $\tau$source, and $\sigma \times \tau$source denotes the type of pairs of objects, one from $\sigma$source and one from $\tau$source. We can then define a set of terms inductively, as follows:

1. For each type $\sigma$source, there is a stock of variables $x$source, $y$source, $z$source, dots of type $\sigma$source

2. $0$source is a term of type $\mathbb{N}$source

3. $S$source (successor) is a term of type $\mathbb{N}\to \mathbb{N}$source

4. If $s$source is a term of type $\sigma$source, and $t$source is a term of type $\mathbb{N}\to (\sigma \to \sigma )$source, then $R_{st}$source is a term of type $\mathbb{N}\to \sigma$source

5. If $s$source is a term of type $\tau \to \sigma$source and $t$source is a term of type $\tau$source, then $s\left(t\right)$source is a term of type $\sigma$source

6. If $s$source is a term of type $\sigma$source and $x$source is a variable of type $\tau$source, then $\lambda x.s$source is a term of type $\tau \to \sigma$source.

7. If $s$source is a term of type $\sigma$source and $t$source is a term of type $\tau$source, then $⟨s,t⟩$source is a term of type $\sigma \times \tau$source.

8. If $s$source is a term of type $\sigma \times \tau$source then $p_1\left(s\right)$source is a term of type $\sigma$source and $p_2\left(s\right)$source is a term of type $\tau$source.

Intuitively, $R_{st}$source denotes the function defined recursively by

$⟨s,t⟩$source denotes the pair whose first component is $s$source and whose second component is $t$source, and $p_1\left(s\right)$source and $p_2\left(s\right)$source denote the first and second elements (“projections”) of $s$source. Finally, $\lambda x.s$source denotes the function $f$source defined by

for any $x$source of type $\sigma$source; so item (6) gives us a form of comprehension, enabling us to define functions using terms. Formulas are built up from identity predicate statements $s=t$source between terms of the same type, the usual propositional connectives, and higher-type quantification. One can then take the axioms of the system to be the basic equations governing the terms defined above, together with the usual rules of logic with quantifiers and identity predicate.

If one augments the finite type system with a type $\Omega$source of truth values, one has to include axioms which govern its use as well. In fact, if one is clever, one can get rid of complex formulas entirely, replacing them with terms of type $\Omega$source! The proof system can then be modified accordingly. The result is essentially the simple theory of types set forth by Alonzo Church in the 1930s.

As in the case of second-order logic, there are different versions of higher-type semantics that one might want to use. In the full version, variables of type $\sigma \to \tau$source range over the set of all functions from the objects of type $\sigma$source to objects of type $\tau$source. As you might expect, this semantics is too strong to admit a complete, effective derivation system. But one can consider a weaker semantics, in which a structure consists of sets of elements $T_{\tau }$source for each type $\tau$source, together with appropriate operations for application, projection, etc. If the details are carried out correctly, one can obtain completeness theorems for the kinds of derivation systems described above.

Higher-type logic is attractive because it provides a framework in which we can embed a good deal of mathematics in a natural way: starting with $\mathbb{N}$source, one can define real numbers, continuous functions, and so on. It is also particularly attractive in the context of intuitionistic logic, since the types have clear “constructive” interpretations. In fact, one can develop constructive versions of higher-type semantics (based on intuitionistic, rather than classical logic) that clarify these constructive interpretations quite nicely, and are, in many ways, more interesting than the classical counterparts.

Document

olfileidfolbydil

Intuitionistic Logic

In contrast to second-order and higher-order logic, intuitionistic first-order logic represents a restriction of the classical version, intended to model a more “constructive” kind of reasoning. The following examples may serve to illustrate some of the underlying motivations.

Suppose someone came up to you one day and announced that they had determined a natural number $x$source, with the property that if $x$source is prime, the Riemann hypothesis is true, and if $x$source is composite, the Riemann hypothesis is false. Great news! Whether the Riemann hypothesis is true or not is one of the big open questions of mathematics, and here they seem to have reduced the problem to one of calculation, that is, to the determination of whether a specific number is prime or not.

What is the magic value of $x$source? They describe it as follows: $x$source is the natural number that is equal to $7$source if the Riemann hypothesis is true, and $9$source 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$source; but what you really want is a value of $x$source that is given explicitly.

To take another, perhaps less contrived example, consider the following question. We know that it is possible to raise an irrational number to a rational power, and get a rational result. For example, ${\sqrt{2}}^2=2$source. What is less clear is whether or not it is possible to raise an irrational number to an irrational power, and get a rational result. The following theorem answers this in the affirmative:

Does this constitute a valid proof? Most mathematicians feel that it does. But again, there is something a little bit unsatisfying here: we have proved the existence of a pair of real numbers with a certain property, without being able to say which pair of numbers it is. It is possible to prove the same result, but in such a way that the pair $a$source, $b$source is given in the proof: take $a=\sqrt{3}$source and $b={\log }_{3}4$source. Then

since $3^{{\log }_{3}x}=x$source.

Intuitionistic logic is designed to model a kind of reasoning where moves like the one in the first proof are disallowed. Proving the existence of an $x$source satisfying $A\left(x\right)$source means that you have to give a specific $x$source, and a proof that it satisfies $A$source, like in the second proof. Proving that $A$source or $B$source holds requires that you can prove one or the other.

Formally speaking, intuitionistic first-order logic is what you get if you restrict a derivation system for first-order logic in a certain way. Similarly, there are intuitionistic versions of second-order or higher-order logic. From the mathematical point of view, these are just formal deductive systems, but, as already noted, they are intended to model a kind of mathematical reasoning. One can take this to be the kind of reasoning that is justified on a certain philosophical 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's constructivism); and one can argue about whether or not the formal description captures the informal motivation. But whatever philosophical positions we may hold, we can study intuitionistic logic as a formally presented logic; and for whatever reasons, many mathematical logicians find it interesting to do so.

There is an informal constructive interpretation of the intuitionist connectives, usually known as the BHK interpretation (named after Brouwer, Heyting, and Kolmogorov). It runs as follows: a proof of $A\wedge B$source consists of a proof of $A$source paired with a proof of $B$source; a proof of $A\vee B$source consists of either a proof of $A$source, or a proof of $B$source, where we have explicit information as to which is the case; a proof of $A\to B$source consists of a procedure, which transforms a proof of $A$source to a proof of $B$source; a proof of $\forall xA\left(x\right)$source consists of a procedure which returns a proof of $A\left(x\right)$source for any value of $x$source; and a proof of $\exists xA\left(x\right)$source consists of a value of $x$source, together with a proof that this value satisfies $A$source. One can describe the interpretation in computational terms known as the “Curry--Howard isomorphism” or the “formulas-as-types paradigm”: think of a formula as specifying a certain kind of data type, and proofs as computational objects of these data types that 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 makes this more precise.

Obtaining instances of one schema from either of the others is a good exercise in intuitionistic logic.

The first deductive systems for intuitionistic propositional logic, put forth as formalizations of Brouwer's intuitionism, are due, independently, to Kolmogorov, Glivenko, and Heyting. The first formalization of intuitionistic first-order logic (and parts of intuitionist mathematics) is due to Heyting. Though a number of classically valid schemata are not intuitionistically valid, many are.

The double-negation translation describes an important relationship between classical and intuitionist logic. It is defined inductively follows (think of $A^N$source as the “intuitionist” translation of the classical formula $A$source):

Kolmogorov and Glivenko had versions of this translation for propositional logic; for predicate logic, it is due to G\"odel and Gentzen, independently. We have

We can now envision the following dialogue. Classical mathematician: “I've proved $A$source!” Intuitionist mathematician: “Your proof isn't valid. What you've really proved is $A^N$source.” Classical mathematician: “Fine by me!” As far as the classical mathematician is concerned, the intuitionist is just splitting hairs, since the two are equivalent. But the intuitionist insists there is a difference.

Note that the above translation concerns pure logic only; it does not address the question as to what the appropriate nonlogical axioms are for classical and intuitionistic mathematics, or what the relationship is between them. But the following slight extension of the theorem above provides some useful information:

In other words, if $A$source is provable from some hypotheses classically, then $A^N$source is provable from their double-negation translations.

To show that a sentence or propositional formula is intuitionistically valid, all you have to do is provide a proof. But how can you show that it is not valid? For that purpose, we need a semantics that is sound, and preferably complete. A semantics due to Kripke nicely fits the bill.

We can play the same game we did for classical logic: define the semantics, and prove soundness and completeness. It is worthwhile, however, to note the following distinction. In the case of classical logic, the semantics was the “obvious” one, in a sense implicit in the meaning of the connectives. Though one can provide some intuitive motivation for Kripke semantics, the latter does not offer the same feeling of inevitability. In addition, the notion of a classical structure is a natural mathematical one, so we can either take the notion of a structure to be a tool for studying classical first-order logic, or take classical first-order logic to be a tool for studying mathematical structures. In contrast, Kripke structures can only be viewed as a logical construct; they don't seem to have independent mathematical interest.

A Kripke structure $M=⟨W,R,V⟩$source for a propositional language consists of a set $W$source, partial order $R$source on $W$source with a least element, and an “monotone” assignment of propositional variables to the elements of $W$source. The intuition is that the elements of $W$source represent “worlds,” or “states of knowledge”; an element $v\ge u$source represents a “possible future state” of $u$source; and the propositional variables assigned to $u$source are the propositions that are known to be true in state $u$source. The forcing relation $M,w⊩A$source then extends this relationship to arbitrary formulas in the language; read $M,w⊩A$source as “$A$source is true in state $w$source.” The relationship is defined inductively, as follows:

1. $M,w⊩p_i$source iff $p_i$source is one of the propositional variables assigned to $w$source.

2. $M,w⊮\perp$source.

3. $M,w⊩(A\wedge B)$source iff $M,w⊩A$source and $M,w⊩B$source.

4. $M,w⊩(A\vee B)$source iff $M,w⊩A$source or $M,w⊩B$source.

5. $M,w⊩(A\to B)$source iff, whenever $w^{\prime }\ge w$source and $M,w^{\prime }⊩A$source, then $M,w^{\prime }⊩B$source.

It is a good exercise to try to show that $\neg (p\wedge q)\to (\neg p\vee \neg q)$source is not intuitionistically valid, by cooking up a Kripke structure that provides a counterexample.

Document

olfileidfolbydmod

Modal Logics

Consider the following example of a conditional sentence:

This is an example of a conditional assertion that may be materially true but nonetheless misleading, since it seems to suggest that there is a stronger link between the antecedent and conclusion other than simply that either the antecedent is false or the consequent true. That is, the wording suggests that the claim is not only true in this particular world (where it may be trivially true, because Jeremy is not alone in the room), but that, moreover, the conclusion would have been true had the antecedent been true. In other words, one can take the assertion to mean that the claim is true not just in this world, but in any “possible” world; or that it is necessarily true, as opposed to just true in this particular world.

Modal logic was designed to make sense of this kind of necessity. One obtains modal propositional logic from ordinary propositional logic by adding a box operator; which is to say, if $A$source is a formula, so is $\square A$source. Intuitively, $\square A$source asserts that $A$source is necessarily true, or true in any possible world. $◇A$source is usually taken to be an abbreviation for $\neg \square \neg A$source, and can be read as asserting that $A$source is possibly true. Of course, modality can be added to predicate logic as well.

Kripke structures can be used to provide a semantics for modal logic; in fact, Kripke first designed this semantics with modal logic in mind. Rather than restricting to partial orders, more generally one has a set of “possible worlds,” $P$source, and a binary “accessibility” relation $R\left(x,y\right)$source between worlds. Intuitively, $R\left(p,q\right)$source asserts that the world $q$source is compatible with $p$source; i.e., if we are “in” world $p$source, we have to entertain the possibility that the world could have been like $q$source.

Modal logic is sometimes called an “intensional” logic, as opposed to an “extensional” one. The intended semantics for an extensional logic, like classical logic, will only refer to a single world, the “actual” one; while the semantics for an “intensional” logic relies on a more elaborate ontology. In addition to structureing necessity, one can use modality to structure other linguistic constructions, reinterpreting $\square$source and $◇$source according to the application. For example:

1. In provability logic, $\square A$source is read “$A$source is provable” and $◇A$source is read “$A$source is consistent.”

2. In epistemic logic, one might read $\square A$source as “I know $A$source” or “I believe $A$source.”

3. In temporal logic, one can read $\square A$source as “$A$source is always true” and $◇A$source as “$A$source is sometimes true.”

One would like to augment logic with rules and axioms dealing with modality. For example, the system $S4$source consists of the ordinary axioms and rules of propositional logic, together with the following axioms:

Variations of these axioms may be suitable for different applications; for example, S5 is usually taken to characterize the notion of logical necessity. And the nice thing is that one can usually find a semantics for which the derivation system is sound and complete by restricting the accessibility relation in the Kripke structures in natural ways. For example, $S4$source corresponds to the class of Kripke structures in which the accessibility relation is reflexive and transitive. $S5$source corresponds to the class of Kripke structures in which the accessibility relation is em universal, which is to say that every world is accessible from every other; so $\square A$source holds if and only if $A$source holds in every world.

Document

olfileidfolbydoth

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, and fashion a semantics to go with it. You might have to be a bit clever if you want the derivation system to be complete for the semantics, and it might take some effort to convince the world at large that your logic is truly interesting. But, in return, you can enjoy hours of good, clean fun, exploring your logic's mathematical and computational properties.

Recent decades have witnessed a veritable explosion of formal logics. Fuzzy logic is designed to model reasoning about vague properties. Probabilistic logic is designed to model reasoning about uncertainty. Default logics and nonmonotonic logics are designed to model defeasible forms of reasoning, which is to say, “reasonable” inferences that can later be overturned in the face of new information. There are epistemic logics, designed to model reasoning about knowledge; causal logics, designed to model reasoning about causal relationships; and even “deontic” logics, which are designed to model reasoning about moral and ethical obligations. Depending on whether the primary motivation for introducing these systems is philosophical, mathematical, or computational, you may find such creatures studies under the rubric of mathematical logic, philosophical logic, artificial intelligence, cognitive science, or elsewhere.

The list goes on and on, and the possibilities seem endless. We may never attain Leibniz' dream of reducing all of human reason to calculation---but that can't stop us from trying.