Logic | Rod Carvalho

Posts Tagged ‘Logic’

From classical deduction to Bayesian probability

August 15, 2012

Terence Tao on classical deduction and Bayesian probability:

In classical logic, one can represent one’s information about a system as a set of possible states that the system could be in, based on the information at hand. With each new measurement of the system, some possibilities could be eliminated, leading to an updated posterior set of information that is an improvement over the prior set of information. A good example of this type of updating occurs when solving a Sudoku puzzle; each new cell value that one learns about constrains the possible values of the remaining cells. Other examples can be found in the classic detective stories of Arthur Conan Doyle featuring Sherlock Holmes. Proof by contradiction can also be viewed as an instance of this type of deduction.

A modern refinement of classical deduction is that of Bayesian probability. Here, one’s information about a system is not merely represented as a set of possible states, but by a probability distribution on the space of all states, indicating one’s current beliefs on the likelihood of each particular state actually being the true state. Each new measurement of the system then updates a prior probability distribution to a posterior probability distribution, using Bayes’ formula

$P (A \mid B) = \displaystyle \frac{P (B \mid A) P(A)}{ P(B) }$ .

Bayesian probability is widely used in statistics, in machine learning, and in the sciences.

To relate Bayesian probability to classical deduction, recall that every probability distribution has a support, which (in the case when the space of states is discrete) is the set of all states that occur with non-zero probability. When performing a Bayesian update on a discrete space, any state which is inconsistent with the new piece of information will have its posterior probability set to zero, and thus be removed from the support. Thus we see that whilst the probability distribution evolves by Bayesian updating, the support evolves by classical deductive logic. Thus one can view classical logic as the qualitative projection of Bayesian probability, or equivalently, one can view Bayesian probability as a quantitative refinement of classical logic.

Alternatively, one can view Bayesian probability as a special case of classical logic by taking a frequentist interpretation. In this interpretation, one views the actual universe (or at least the actual system) as just one of a large number of possible universes (or systems). In each of these universes, the system is in one of the possible states; the probability assigned to each state is then the proportion of the possible universes in which that state is attained. Each new measurement eliminates some fraction of the universes in a given state, depending on how likely or unlikely that state was to actually produce that measurement; the surviving universes then have a new posterior probability distribution, which is related to the prior distribution by Bayes’ formula.

It is instructive to interpret Sherlock Holmes‘ famous quote, “When you have eliminated all which is impossible, then whatever remains, however improbable, must be the truth,” from a Bayesian viewpoint. The statement is technically correct; however, when performing this type of elimination to an (a priori) improbable conclusion, the denominator in Bayes’ formula is extremely small, and so the deduction is unstable if it later turns out that some of the possibilities thought to have been completely eliminated, were in fact only incompletely eliminated. (See also the mantra “extraordinary claims require extraordinary evidence”, which can be viewed as the Bayesian counterpoint to Holmes’ classical remark.)

Another interesting place where one can contrast classical deduction with Bayesian deduction is with regard to taking converses. In classical logic, if one knows that $A$ implies $B$ , one cannot then deduce that $B$ implies $A$ . However, in Bayesian probability, if one knows that the presence of $A$ elevates the likelihood that $B$ is true, then an observation of $B$ will conversely elevate the prior probability that $A$ is true, thanks to Bayes’ formula: if $P(B \mid A) > P(B)$ , then $P(A \mid B) > P(A)$ . This may help explain why taking converses is an intuitive operation to those who have not yet been thoroughly exposed to classical logic. (It is also instructive to understand why this disparity between the two types of deduction is not in conflict with the previously mentioned links between the two. This disparity is roughly analogous to the disparity between worst-case analysis and average-case analysis.)

Bayesian probability can be generalised further; for instance, quantum mechanics (with the Copenhagen interpretation) can be viewed as a noncommutative generalisation of Bayesian probability, though the connection to classical logic is then lost when one is dealing with observables that do not commute. But this is another story…

__________

Please do note that Terence Tao’s original post contains neither links nor boldface highlighting. I took the liberty of adding those for convenience and emphasis. To improve legibility I also wrote the mathematical expressions in $\LaTeX$ .

__________

Source:

Terence Tao, “A modern refinement of classical deduction is that of Bayesian probability”, Google Buzz, April 4, 2010.

Tags:Bayesian Deduction, Bayesianism, Classical Deduction, Frequentism, Logic, Philosophy of Probability, Terence Tao
Posted in Logic, Probability Theory, Thoughts | Leave a Comment »

Deciding the surjectivity of finite functions

March 19, 2012

Consider a function $f : \mathcal{X} \to \mathcal{Y}$ . We say that $f$ is a finite function if and only if both $\mathcal{X}$ and $\mathcal{Y}$ are finite sets. As mentioned two weeks ago, function $f$ is surjective if and only if

$\forall y \exists x \left( f (x) = y \right)$

where $x$ and $y$ range over sets $\mathcal{X}$ and $\mathcal{Y}$ , respectively. We now introduce the surjectivity predicate $\varphi : \mathcal{X} \times \mathcal{Y} \to \{\text{True}, \text{False}\}$ , defined by $\varphi (x, y) =\left( f (x) = y\right)$ so that function $f$ is surjective if and only if $\forall y \exists x \, \varphi (x, y)$ evaluates to $\text{True}$ .

Let $m := |\mathcal{X}|$ and $n := |\mathcal{Y}|$ denote the cardinalities of sets $\mathcal{X}$ and $\mathcal{Y}$ , respectively. Deciding $\forall y \exists x \, \varphi (x, y)$ should then require a total of $m n$ evaluations of predicate $\varphi$ . Let us write $\mathcal{X} = \{x_1, x_2, \dots, x_m\}$ and $\mathcal{Y} = \{y_1, y_2, \dots, y_n\}$ , and introduce $\Phi \in \{\text{True}, \text{False}\}^{m \times n}$ , a Boolean matrix defined as follows

$\Phi = \left[\begin{array}{cccc} \varphi (x_1,y_1) & \varphi (x_1,y_2) & \ldots & \varphi (x_1,y_n)\\ \varphi (x_2,y_1) & \varphi (x_2,y_2) & \ldots & \varphi (x_2,y_n)\\ \vdots & \vdots & \ddots & \vdots\\ \varphi (x_m,y_1) & \varphi (x_m,y_2) & \ldots & \varphi (x_m,y_n)\\\end{array}\right]$

Stating that $f$ is surjective, i.e., $\forall y \exists x \, \varphi (x, y)$ evaluates to $\text{True}$ , is equivalent to saying that every column of matrix $\Phi$ contains at least one entry that evaluates to $\text{True}$ . We now introduce a new predicate, $\psi : \mathcal{Y} \to \{\text{True}, \text{False}\}$ , defined by

$\psi (y) = \exists x \, \varphi (x,y)$

so that $\forall y \exists x \, \varphi (x, y)$ can be rewritten in the form $\forall y \, \psi (y)$ , where $y$ ranges over set $\mathcal{Y}$ . Note that $\psi (y)$ can be viewed as the disjunction of the $m$ atoms $\varphi (x_1, y), \varphi (x_2, y), \dots, \varphi (x_m, y)$ , i.e.,

$\psi (y) = \displaystyle\bigvee_{i =1}^m \varphi (x_i, y)$ .

Note also that $\forall y \, \psi (y)$ can be viewed as the conjunction of the $n$ atoms $\psi (y_1), \psi (y_2), \dots, \psi (y_n)$ . Thus, we can decide surjectivity using the following procedure:

Compute $\psi (y) = \exists x \, \varphi (x,y)$ for all $y \in \mathcal{Y}$ .
Compute the conjunction $\bigwedge_{j=1}^n \psi (y_j)$ . If its truth value is $\text{True}$ , then the function is surjective.

Let us now consider two simple examples and implement this decision procedure in Haskell.

__________

Example #1

Let us define $\mathbb{Z}_4 := \{0, 1, 2, 3\}$ . Consider the finite function

$\begin{array}{rl} f : \mathbb{Z}_4 &\to \mathbb{Z}_4\\ n &\mapsto 3 n \pmod{4}\end{array}$

where $\pmod{4}$ denotes modulo 4 arithmetic. Note that $f (0) = 0$ , $f (1) = 3$ , $f (2) = 2$ , and $f (3) = 1$ . Hence, we easily conclude that $f$ is both injective and surjective (and, thus, is bijective). In Haskell:

Prelude> let f n = (3 * n) `mod` 4
Prelude> let xs = [0..3]
Prelude> let ys = [0..3]
Prelude> let psi y = or [(f x == y) | x <- xs]
Prelude> all psi ys
True

which allows us to conclude that $f$ is surjective. Note that we used function or to perform disjunction, and function all to perform universal quantification.

__________

Example #2

Consider now the following finite function

$\begin{array}{rl} g : \mathbb{Z}_4 &\to \mathbb{Z}_4\\ n &\mapsto 2 n \pmod{4}\end{array}$

Note that $g (0) = g (2) = 0$ and $g (1) = g (3) = 2$ . Hence, function $g$ is neither injective nor surjective. In Haskell, we have the following:

Prelude> let g n = (2 * n) `mod` 4
Prelude> let xs = [0..3]
Prelude> let ys = [0..3]
Prelude> let psi y = or [(g x == y) | x <- xs]
Prelude> all psi ys
False

which allows us to conclude that $g$ is not surjective. Why? The following code returns a list of lists of Booleans where each sublist is a column of matrix $\Phi$ (where each entry is $\Phi_{ij} = (g(x_i) = y_j)$ )

Prelude> [[(g x == y) | x <- xs] | y <- ys]
[[True,False,True,False],[False,False,False,False],
[False,True,False,True],[False,False,False,False]]

Note that the 2nd and 4th sublists contain only $\text{False}$ truth values. Hence, it is not the case that every column of matrix $\Phi$ contains at least one entry that evaluates to $\text{True}$ . Thus, $g$ is not surjective.

Tags:Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Logic, Predicate Logic, Surjectivity
Posted in Haskell, Logic, Mathematics | Leave a Comment »

Deciding the injectivity of finite functions II

March 17, 2012

Last week we considered the following finite function

$\begin{array}{rl} f : \mathbb{Z}_4 &\to \mathbb{Z}_4\\ n &\mapsto 3 n \pmod{4}\end{array}$

where $\mathbb{Z}_4 := \{0, 1, 2, 3\}$ and $\pmod{4}$ denotes modulo 4 arithmetic. We know that function $f$ is injective if and only if

$\forall x_1 \forall x_2 \left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

where $x_1$ and $x_2$ range over set $\mathbb{Z}_4$ . We introduce the injectivity predicate $\varphi : \mathbb{Z}_4 \times \mathbb{Z}_4 \to \{\text{True}, \text{False}\}$ , defined by

$\varphi (x_1, x_2) =\left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

so that function $f$ is injective if and only if the universally-quantified sentence $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ evaluates to $\text{True}$ .

__________

A naive decision procedure

We can determine the truth value of $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ by evaluating the predicate $\varphi$ at all $(x_1, x_2) \in \mathbb{Z}_4 \times \mathbb{Z}_4$ , which will require a total of $|\mathbb{Z}_4|^2 = 4^2 = 16$ evaluations. We implemented this decision procedure in Haskell last week. Here’s a rather brief GHCi session:

Prelude> let f n = (3 * n) `mod` 4
Prelude> let phi (x1,x2) = (f x1 /= f x2) || (x1 == x2)
Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
True

which allows us to conclude that $f$ is injective. Note that we used the following equivalence

$\left( f (x_1) = f (x_2) \implies x_1 = x_2\right) \equiv \left( f (x_1) \neq f (x_2) \lor x_1 = x_2\right)$

to implement $\varphi$ . Can we do better than this? In fact, we can.

__________

A better decision procedure

We introduce matrix $\Phi \in \{\text{True}, \text{False}\}^{4 \times 4}$ , defined by

$\Phi = \left[\begin{array}{cccc} \varphi (0,0) & \varphi (0,1) & \varphi (0,2) & \varphi (0,3)\\ \varphi (1,0) & \varphi (1,1) & \varphi (1,2) & \varphi (1,3)\\ \varphi (2,0) & \varphi (2,1) & \varphi (2,2) & \varphi (2,3)\\ \varphi (3,0) & \varphi (3,1) & \varphi (3,2) & \varphi (3,3)\\\end{array}\right]$

Stating that $f$ is injective, i.e., $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ evaluates to $\text{True}$ , is equivalent to saying that all the $4^2 = 16$ entries of matrix $\Phi$ evaluate to $\text{True}$ . Note, however, that the four entries on the main diagonal of $\Phi$ will always evaluate to $\text{True}$ , as the implication

$f (x) = f (x) \implies x = x$

evaluates to $\text{True}$ for every $x$ . Moreover, from the equivalence

$\left( f (x_1) = f (x_2) \implies x_1 = x_2\right) \equiv \left( f (x_2) = f (x_1) \implies x_2 = x_1\right)$

we can conclude that $\varphi (x_1, x_2) = \varphi (x_2, x_1)$ for all $x_1$ and $x_2$ , which tells us that matrix $\Phi$ is symmetric (i.e., $\Phi = \Phi^T$ ). Therefore, we do not need to evaluate all entries of matrix $\Phi$ , only the ones above the main diagonal, as illustrated below

$\left[\begin{array}{cccc} \ast & \varphi (0,1) & \varphi (0,2) & \varphi (0,3)\\ \ast & \ast & \varphi (1,2) & \varphi (1,3)\\ \ast & \ast & \ast & \varphi (2,3)\\ \ast & \ast & \ast & \ast\\\end{array}\right]$

where the symbol $\ast$ denotes “don’t care”, i.e., entries we do not need to evaluate. Hence, instead of evaluating the predicate $\varphi$ a total of $4^2 = 16$ times, we now only need to evaluate it ${4 \choose 2} = 6$ times, which is $37.5 \%$ of the original total. We can generate all pairs $(x_1, x_2)$ with $x_2 > x_1$ using the following Haskell code:

Prelude> [(x1,x2) | x1 <- [0..3], x2 <- [(x1+1)..3]]
[(0,1),(0,2),(0,3),(1,2),(1,3),(2,3)]

We thus implement a more efficient decision procedure as follows:

Prelude> let f n = (3 * n) `mod` 4
Prelude> let phi (x1,x2) = (f x1 /= f x2) || (x1 == x2)
Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [(x1+1)..3]]
True

which requires less than half of the number of evaluations required by the previous (naive) procedure.

__________

Conclusions

Given a finite function $f : \mathcal{X} \to \mathcal{Y}$ , we introduce the injectivity predicate $\varphi : \mathcal{X} \times \mathcal{X} \to \{\text{True}, \text{False}\}$ , defined by

$\varphi (x_1, x_2) =\left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

so that (finite) function $f$ is injective if and only if $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ evaluates to $\text{True}$ . Let $n := |\mathcal{X}|$ denote the cardinality of set $\mathcal{X}$ . Deciding $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ using the naive procedure will require a total of $n^2$ evaluations of the predicate $\varphi$ . Since $\varphi (x,x) = \text{True}$ for every $x$ , and taking into account that $\varphi (x_1,x_2) = \varphi (x_2,x_1)$ , using the improved procedure we can decide injectivity at a cost of only ${n \choose 2} = \frac{n (n-1)}{2}$ evaluations of the predicate $\varphi$ . As $n$ approaches infinity, the ratio ${n \choose 2} / n^2$ approaches $1/2$ . Hence, for “large” problems, the improved procedure will require approximately half the number of evaluations required by the naive procedure.

Tags:Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Injectivity, Logic, Predicate Logic
Posted in Haskell, Logic, Mathematics | Leave a Comment »

Deciding the injectivity of finite functions

March 7, 2012

Consider a function $f : \mathcal{X} \to \mathcal{Y}$ . We say that $f$ is a finite function if and only if both $\mathcal{X}$ and $\mathcal{Y}$ are finite sets. As mentioned last week, function $f$ is injective if and only if

$\forall x_1 \forall x_2 \left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

where $x_1$ and $x_2$ range over set $\mathcal{X}$ . We now introduce the injectivity predicate $\varphi : \mathcal{X} \times \mathcal{X} \to \{\text{True}, \text{False}\}$ , defined by

$\varphi (x_1, x_2) =\left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$

so that function $f$ is injective if and only if $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ is true. In this post we will restrict our attention to finite functions, for which it is fairly straightforward to devise a decision procedure to decide injectivity. Let $n := |\mathcal{X}|$ denote the cardinality of set $\mathcal{X}$ . Then, determining the truth value of $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ will require a total of $n^2$ evaluations of the predicate $\varphi$ .

__________

Example

Let us define $\mathbb{Z}_4 := \{0, 1, 2, 3\}$ . Consider the finite function

$\begin{array}{rl} f : \mathbb{Z}_4 &\to \mathbb{Z}_4\\ n &\mapsto 3 n \pmod{4}\end{array}$

where $\pmod{4}$ denotes modulo 4 arithmetic. Is $f$ injective? Note that $f (0) = 0$ , $f (1) = 3$ , $f (2) = 2$ , and $f (3) = 1$ . Hence, we easily conclude that $f$ is injective. Suppose that we do not want to enumerate the images of the elements of $\mathbb{Z}_4$ under $f$ ; in that case, we can use the following Haskell script to decide that $f$ is injective:

-- define function f
f :: Integral a => a -> a
f n = (3 * n) `mod` 4 

-- define disjunction
(\/) :: Bool -> Bool -> Bool
p \/ q = p || q

-- define implication
(==>) :: Bool -> Bool -> Bool
p ==> q = (not p) \/ q

-- define injectivity predicate
phi :: Integral a => (a,a) -> Bool
phi (x1,x2) = (f x1 == f x2) ==> (x1 == x2)

where we used the fact that $p \implies q$ is semantically equivalent to $\neg p \lor q$ . Let us carry out some testing:

*Main> -- test function f
*Main> [ f n | n <- [0..3]]
[0,3,2,1]
*Main> -- test disjunction
*Main> [ p \/ q | p <-[True, False], q <- [True, False]]
[True,True,True,False]
*Main> -- test implication
*Main> [ p ==> q | p <-[True, False], q <- [True, False]]
[True,False,True,True]

So far, so good. Finally, we can determine the truth value of the sentence $\forall x_1 \forall x_2 \, \varphi (x_1, x_2)$ using function all, as follows:

*Main> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
True

which allows us to conclude that $f$ is injective.

An alternative procedure would be to use function nub from library Data.List to remove duplicates from a given list. Note that $f$ is injective if and only if the list of the images of the elements of $\mathbb{Z}_4$ under $f$ contains no duplicates. Hence, we obtain:

*Main> let images = [ f n | n <- [0..3]]
*Main> import Data.List
*Main Data.List> length (nub images) == length images
True

What a hack! This second procedure might seem much terser than the first one. But if we do away with type declarations and refrain from re-defining disjunction and defining implication, the first procedure can be made quite succinct as well:

Prelude> let f n = (3 * n) `mod` 4
Prelude> let phi (x1,x2) = not (f x1 == f x2) || (x1 == x2)
Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]]
True

which includes the definition of function $f$ . Three lines only! Three!

Tags:Data.List, Decision Problems, Decision Procedures, Finite Functions, Functionology, Haskell, Injectivity, Logic, Predicate Logic
Posted in Haskell, Logic, Mathematics | 5 Comments »

Not all birds can fly

January 1, 2012

Consider the following declarative sentence

Not all birds can fly.

This sentence can be paraphrased as

It is not the case that all things which are birds can fly.

Let $\mathcal{X}$ be the set of all things of interest (i.e., the universe under discussion). We now introduce predicates $B : \mathcal{X} \to \{\text{True}, \text{False}\}$ and $F : \mathcal{X} \to \{\text{True}, \text{False}\}$ , defined by

$B (x) = \begin{cases} \text{True}, & x \textrm{ is a bird}\\ \text{False}, & x \textrm{ is not a bird}\end{cases}$

and

$F (x) = \begin{cases} \text{True}, & x \textrm{ can fly}\\ \text{False}, & x \textrm{ cannot fly}\end{cases}$

Finally, using (unary) predicates $B$ and $F$ , the declarative sentence “Not all birds can fly” can be encoded as follows

$\neg \left( \forall x \, ( B (x) \rightarrow F (x) ) \right)$

where we used negation ( $\neg$ ), universal quantification ( $\forall$ ), and material implication ( $\rightarrow$ ). The (well-formed) formula above should be read as: “it is not the case that for all $x \in \mathcal{X}$ , if $x$ is a bird, then $x$ can fly”. Whether the (universally quantified) formula evaluates to $\text{True}$ or $\text{False}$ depends on the set $\mathcal{X}$ we consider. For example, if $\mathcal{X}$ is the set of all living things on Earth on January 1, 2012, then the formula evaluates to $\text{True}$ because penguins are birds which cannot fly. However, if we spend the next century eradicating all birds that cannot fly, then on January 1, 2112, the formula might evaluate to $\text{False}$ .

__________

Technicalities

Let us consider the formula $\neg\left(\forall x \, \varphi (x)\right)$ , where $\varphi$ is a predicate. If this formula evaluates to $\text{True}$ , then it is not the case that for all $x \in \mathcal{X}$ we have that $\varphi (x) = \text{True}$ , which is the same as saying that there exists a $x \in \mathcal{X}$ for which $\varphi (x) = \text{False}$ or, in other words, for which $\neg \varphi (x) = \text{True}$ . Hence, formula $\neg\left(\forall x \, \varphi (x)\right)$ is equivalent (in some sense) to the formula $\exists x \, \neg \varphi (x)$ , where $\exists$ is the existential quantifier. We write $\neg\left(\forall x \, \varphi (x)\right) \equiv \exists x \, \neg \varphi (x)$ to denote this equivalence. Hence, we conclude that

$\neg \left( \forall x \, ( B (x) \rightarrow F (x) ) \right) \equiv \exists x \, \neg ( B (x) \rightarrow F (x) )$ .

Given propositional atoms $p$ and $q$ , we have that the formula $p \rightarrow q$ is semantically equivalent [1] to the formula $\neg p \lor q$ . We write $p \rightarrow q \equiv \neg p \lor q$ to denote this equivalence. Thus, we have that

$B (x) \rightarrow F (x) \equiv \neg B (x) \lor F (x)$

which allows us to conclude that

$\exists x \, \neg ( B (x) \rightarrow F (x) ) \equiv \exists x \, \neg ( \neg B (x) \lor F (x) )$ .

Using one of De Morgan’s laws, namely, $\neg (p \lor q) \equiv \neg p \land \neg q$ , we conclude that $\neg ( \neg B (x) \lor F (x) ) \equiv \neg \neg B (x) \land \neg F (x)$ . Eliminating the double negation (we can do that in Classical Logic, but not in Intuitionistic Logic), we obtain $\neg ( \neg B (x) \lor F (x) ) \equiv B (x) \land \neg F (x)$ . Without further ado, we have that

$\exists x \, \neg ( \neg B (x) \lor F (x) ) \equiv \exists x \, ( B (x) \land \neg F (x) )$ .

From all these equivalences, we finally conclude that

$\neg \left( \forall x \, ( B (x) \rightarrow F (x) ) \right) \equiv \exists x \, ( B (x) \land \neg F (x) )$ .

What does this equivalence say? It tells us that the declarative sentence “Not all birds can fly” can be paraphrased as follows

There exists a thing which is a bird and which cannot fly.

That “thing” could be, for example, a penguin. For the sake of convenience, let us introduce predicates $\varphi$ and $\psi$ , defined by

$\varphi (x) := B (x) \rightarrow F (x)$

$\psi (x) := B (x) \land \neg F (x)$

so that the last equivalence can be written more compactly as

$\neg \left( \forall x \, \varphi (x) \right) \equiv \exists x \, \psi (x)$

where $\varphi (x) \equiv \neg B (x) \lor F (x)$ . This will be useful later on.

__________

Creating our universe

Let us suppose that we do not know that penguins are birds and that they cannot fly. Evaluating the formula $\exists x \, ( B (x) \land \neg F (x) )$ using planet Earth’s fauna as the set of all things of interest would require us to consult quite a few Zoology books. However, it is Sunday night and the library is closed for the Winter break. And, to make matters worse, we are somewhat lazy.

Instead of bothering with the actual universe, let us create our own imaginary universe in which there are only three classes of animals: birds, cats, and dogs. Each class contains only three species each.

We construct this imaginary universe in Haskell:

-- create Animal data type
data Animal = Bird String |
              Cat String |
              Dog String deriving (Show, Eq)

-- create list of animals
animals = [Bird "Dove", Bird "Hawk", Bird "Penguin",
           Cat "Burmese", Cat "Persian", Cat "Siamese",
           Dog "Dalmatian", Dog "Husky", Dog "Terrier"]

-- define isBird predicate
isBird :: Animal -> Bool
isBird (Bird s) = True
isBird _ = False

-- define canFly predicate
canFly :: Animal -> Bool
canFly (Bird "Dove") = True
canFly (Bird "Hawk") = True
canFly _ = False

-- define phi predicate
phi :: Animal -> Bool
phi x = ((not . isBird) x) || (canFly x) 

-- define psi predicate
psi :: Animal -> Bool
psi x = (isBird x) && ((not . canFly) x)

Let us now play with these objects and predicates and evaluate the quantified formulas using the GHCi interpreter:

*Main> -- print list of animals
*Main> animals
[Bird "Dove",Bird "Hawk",Bird "Penguin",Cat "Burmese",Cat "Persian",
Cat "Siamese",Dog "Dalmatian",Dog "Husky",Dog "Terrier"]
*Main> -- test isBird predicate
*Main> map isBird animals
[True,True,True,False,False,False,False,False,False]
*Main> -- test canFly predicate
*Main> map canFly animals
[True,True,False,False,False,False,False,False,False]
*Main> -- test phi predicate
*Main> map phi animals
[True,True,False,True,True,True,True,True,True]
*Main> -- test psi predicate
*Main> map psi animals
[False,False,True,False,False,False,False,False,False]
*Main> -- evaluate universally quantified formula
*Main> not (all phi animals)
True
*Main> -- evaluate existentially quantified formula
*Main> any psi animals
True

where we used functions all and any to emulate the universal and existential quantifiers, respectively. Note that both formulas evaluate to $\text{True}$ , as expected.

__________

Caution: do not confuse the arrow used in the definition of the predicates with the arrow used in material implication. They look the same, but they are different $\LaTeX$ symbols and context should allow one to distinguish the two.

Remark: this post is based on an example in chapter 2 of Huth & Ryan [1].

__________

References

[1] Michael Huth, Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed., Cambridge University Press, June 2004.

Tags:Haskell, Logic, Predicate Logic
Posted in Haskell, Logic | Leave a Comment »

S	M	T	W	T	F	S
« May
						1
2	3	4	5	6	7	8
9	10	11	12	13	14	15
16	17	18	19	20	21	22
23	24	25	26	27	28	29
30

Rod Carvalho

Posts Tagged ‘Logic’

From classical deduction to Bayesian probability

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

Not all birds can fly

Pages

Categories

Top Posts

Recent Posts

Recent Comments

Tag Cloud

Archives

Blog Stats

Artists

Blogs

Haskell

Math Blogs

MATLAB

Python

Robotics

Software

Symbolic Computation

Powered by FeedBurner

Meta

Follow “Rod Carvalho”

Rod Carvalho

Posts Tagged ‘Logic’

From classical deduction to Bayesian probability

Deciding the surjectivity of finite functions

Deciding the injectivity of finite functions II

Deciding the injectivity of finite functions

Not all birds can fly

Pages

Categories

Top Posts

Recent Posts

Recent Comments

Tag Cloud

Archives

Blog Stats

Artists

Blogs

Haskell

Math Blogs

MATLAB

Python

Robotics

Software

Symbolic Computation

Category Cloud

Powered by FeedBurner

Meta

Follow “Rod Carvalho”