Logic programming and Logical quantifier: Difference between pages

From TCS Wiki
(Difference between pages)
Jump to navigation Jump to search
imported>Eptalon
 
imported>Auntof6
(categorize; use standard simple heading; add missig ref section)
 
Line 1: Line 1:
'''Logic programming''' is using [[mathematical logic]] to write [[computer program]]s. There are specialized [[programming language]]s where the user can directly enter logical statements. Probably the best-known of these languages is called [[Prolog]]. [[Alonzo Church]] used a form of logic programming in what is known as [[lambda calculus]] today. Logic programming has also been used in [[LISP]].  
In [[logic]], a '''quantifier''' is a way to state that a certain number of elements fulfill some criteria.  For example, every [[natural number]] has another natural number larger than it. In this example, the word "every" is a quantifier. Therefore, the sentence "every natural number has another natural number larger than it" is a quantified expression. Quantifiers and quantified expressions are a useful part of formal languages. They are useful because they let rigorous statements claim how widespread a criteria is. Two basic kinds of quantifiers used in [[predicate logic]] are universal and existential quantifiers. A [[universal quantifier]] states that all the elements considered fulfill the criteria. The universal quantifier is symbolized with "∀", an upside down "[[A]]", to stand for "all". An [[existence quantifier]] (symbolized with "∃") states that at least one element considered fits the criteria. The existential quantifier is symbolized with "∃", a backwards "[[E]]", to stand for "exists".
 
Quantifiers are also used in natural languages. Examples of quantifiers in English are ''for all'', ''for some'', ''many'', ''few'', ''a lot'', and ''no''.
 
==Mathematics==
This statement is [[Infinity|infinitely]] long:
: 1 · 2 = 1 + 1, and 2 · 2 = 2 + 2, and 3 · 2 = 3 + 3, ..., and 100 · 2 = 100 + 100, and ..., etc.
 
This is a problem for [[Formal language|formal languages]], since a formal statement needs to be finite in length. These problems can be avoided by using ''universal quantification''. This results in the following compact statement:
: For each [[natural number]] ''n'', ''n'' · 2 = ''n'' + ''n''.
In the same way, we can shorten an infinite sequence of statements joined by or:
: 1 is equal to 5 + 5, or 2 is equal to 5 + 5, or 3 is equal to 5 + 5, ... , or 100 is equal to 5 + 5, or ..., etc.
which can be rewritten using ''existential quantification'':
: For at least one [[natural number]] ''n'', ''n'' is equal to 5+5.
 
==Notation==
 
The two quantifiers most widely used are the [[universal quantifier]] and the [[existence quantifier]].
 
The universal quantifier is used to claim that for elements in a set, the elements all match some criteria. Usually, this statement "for all elements" is shortened to an "[[A]]" flipped upside down, which is "∀".
 
The existential quantifier is used to claim that for elements in a set, there exists at least one element that matches some criteria. Usually, this statement "there exists an element" is shortened to an "[[E]]" flipped upside down, which is "∃".
 
We can rewrite an example English statement with symbols, [[Predicate (grammar)|predicates]] representing criteria, and quantifiers. The example is "Each of Peter's friends either likes to dance or likes to go to the beach". Let ''X'' be the set of all Peter's friends. Let ''P''(''x'') be the predicate "''x'' likes to dance". Let ''Q''(''x'') be the predicate "''x'' likes to go to the beach". We can rewrite the example using formal notation as <math> \forall{x}{\in}X, P(x) \or Q(x) </math>. The statement can be read as "for every ''x'' that is a member of ''X'', ''P'' applies to ''x'' or ''Q'' applies to ''x''."
 
There are other ways to use quantifiers in formal language. Each of the following statements below says the same thing as <math>\exists{x}{\in}X, P(x)</math>:
* <math>\exists{x} P</math>
* <math>(\exists{x}) P</math>
* <math>(\exists x \ . \ P)</math>
* <math>\exists x \ \cdot \ P</math>
* <math>(\exists x : P)</math>
* <math>\exists{x}{\in}X \, P</math>
* <math>\exists\, x{:}X \, P</math>
There are a few more ways to represent the universal quantifier:
* <math>(x) \, P</math>
* <math>\bigwedge_{x} P</math>
 
Several statements above explicitly include ''X'', the set of elements that the quantifier applies to. This set of elements is also known as the range of quantification, or the [[universe of discourse]]. Some of the statements above do not include such a set. In this case, the set will have to be specified before the statement. For example, "''x'' is an apple" must be stated before <math>\exists{x} P(x)</math>. In this case, we are making a statement that at least one apple fits the predicate ''P''.
 
Using quantifiers formally does not require using the symbol ''x''. The symbol ''x'' has been used throughout this article, but any symbol can be used, like ''y''. Make sure not to refer to two different things with the same symbol when choosing symbols.
 
==Nesting==
It is important to put quantifiers in the right order. This is an example English sentence showing how meaning changes with order:
:For every natural number ''n'', there exists a natural number ''s'' such that ''s'' = ''n''<sup>2</sup>.
This statement is true. It states that every natural number has a square. However, if we turn the order of the quantifiers around:
:There exists a natural number ''s'', such that for every natural number ''n'', ''s'' = ''n''<sup>2</sup>.
This statement is false. It claims that there is one natural number ''s'' that is the square of ''every'' natural number.
 
In certain circumstances changing the order of quantifiers does not change the meaning of the statement. For instance:
:There exists a natural number ''x'', and there exists a natural number ''y'' such that ''x'' = ''y''<sup>2</sup>.
 
==Other quantifiers==
There are also less common quantifiers used by mathematicians.
 
An example is the solution quantifier<ref>[[E. C. R. Hehner|Hehner, Eric C. R.]], 2004, [http://www.cs.utoronto.ca/~hehner/aPToP ''Practical Theory of Programming''], 2nd edition, p. 28</ref>. It is used to state which elements solve a particular equation. The solution quantifier is represented by a § (section sign). For example, the following statement claims the squares of 0, 1 and 2 are smaller than 4.  :<math> \left [ \S n \in \mathbb{N} \quad n^2 \leq 4 \right ] = \left\{0, 1, 2\right\}</math>
 
Other quantifiers are:
*There are many elements such that...
*There are few elements such that...
*There are infinitely many elements such that...
*For all but finitely many elements... (sometimes expressed as "for almost all elements...").
*There are [[Infinity#Counting_infinity|uncountable]] many elements such that...
*For all but countably many elements...
 
==History==
 
Term logic was developed by Aristotle. It was an early form of logic, and included quantification. The use of quantification was closer to that of natural language. This meant that statements in term logic with quantifiers were less suited for formal analysis. Term logic included quantifiers for ''All'', ''Some''  and ''No'' (none) in 4th century BC.
 
In 1879, [[Gottlob Frege]] created a notation for universal quantification. Unlike today, he would represent a universal quantification by writing a variable over a dimple in an otherwise straight line. Frege did not create a notation for existential quantification. Instead, he combined universal quantification and a number of [[logical negation|negations]] to make an equivalent statement. Frege's use of quantification was not widely known until [[Bertrand Russell]]'s 1903 ''Principles of Mathematics''.
 
In 1885, [[Charles Sanders Peirce]] and his student [[Oscar Howard Mitchell]] also created a notation for universal and existential quantifiers. They wrote Π<sub>x</sub> and Σ<sub>x</sub> where we now write ∀''x'' and ∃''x''. Pierce's notation was used by many mathematicians into the 1950s.
 
In 1897, [[William Ernest Johnson]] and [[Giuseppe Peano]] created another notation for universal and existential quantification. They were influenced by Pierce's previous quantification notation. Johnson and Peano used the simple (''x'') for universal quantification, and ∃''x'' for existential quantification. Peano's influence on math spread this notation across Europe.
 
In 1935, [[Gerhard Gentzen]] created the ∀ symbol for universal quantification. It was not widely used until the 1960s.
 
==Related pages==
*[[Logic]]
 
==References==
{{Wiktionary|quantification}}
{{reflist}}


Programs consist of a set of rules and facts. In most cases, logic programming uses what is called [[negation as failure]] or ''weak negation:'' This means that if it is not possible to derive some clause <math>p</math> from the facts and rules, the system will assume that its negation is true.
[[Category:Logic]]
[[Category:Logic]]

Latest revision as of 06:11, 20 June 2016

In logic, a quantifier is a way to state that a certain number of elements fulfill some criteria. For example, every natural number has another natural number larger than it. In this example, the word "every" is a quantifier. Therefore, the sentence "every natural number has another natural number larger than it" is a quantified expression. Quantifiers and quantified expressions are a useful part of formal languages. They are useful because they let rigorous statements claim how widespread a criteria is. Two basic kinds of quantifiers used in predicate logic are universal and existential quantifiers. A universal quantifier states that all the elements considered fulfill the criteria. The universal quantifier is symbolized with "∀", an upside down "A", to stand for "all". An existence quantifier (symbolized with "∃") states that at least one element considered fits the criteria. The existential quantifier is symbolized with "∃", a backwards "E", to stand for "exists".

Quantifiers are also used in natural languages. Examples of quantifiers in English are for all, for some, many, few, a lot, and no.

Mathematics

This statement is infinitely long:

1 · 2 = 1 + 1, and 2 · 2 = 2 + 2, and 3 · 2 = 3 + 3, ..., and 100 · 2 = 100 + 100, and ..., etc.

This is a problem for formal languages, since a formal statement needs to be finite in length. These problems can be avoided by using universal quantification. This results in the following compact statement:

For each natural number n, n · 2 = n + n.

In the same way, we can shorten an infinite sequence of statements joined by or:

1 is equal to 5 + 5, or 2 is equal to 5 + 5, or 3 is equal to 5 + 5, ... , or 100 is equal to 5 + 5, or ..., etc.

which can be rewritten using existential quantification:

For at least one natural number n, n is equal to 5+5.

Notation

The two quantifiers most widely used are the universal quantifier and the existence quantifier.

The universal quantifier is used to claim that for elements in a set, the elements all match some criteria. Usually, this statement "for all elements" is shortened to an "A" flipped upside down, which is "∀".

The existential quantifier is used to claim that for elements in a set, there exists at least one element that matches some criteria. Usually, this statement "there exists an element" is shortened to an "E" flipped upside down, which is "∃".

We can rewrite an example English statement with symbols, predicates representing criteria, and quantifiers. The example is "Each of Peter's friends either likes to dance or likes to go to the beach". Let X be the set of all Peter's friends. Let P(x) be the predicate "x likes to dance". Let Q(x) be the predicate "x likes to go to the beach". We can rewrite the example using formal notation as [math]\displaystyle{ \forall{x}{\in}X, P(x) \or Q(x) }[/math]. The statement can be read as "for every x that is a member of X, P applies to x or Q applies to x."

There are other ways to use quantifiers in formal language. Each of the following statements below says the same thing as [math]\displaystyle{ \exists{x}{\in}X, P(x) }[/math]:

  • [math]\displaystyle{ \exists{x} P }[/math]
  • [math]\displaystyle{ (\exists{x}) P }[/math]
  • [math]\displaystyle{ (\exists x \ . \ P) }[/math]
  • [math]\displaystyle{ \exists x \ \cdot \ P }[/math]
  • [math]\displaystyle{ (\exists x : P) }[/math]
  • [math]\displaystyle{ \exists{x}{\in}X \, P }[/math]
  • [math]\displaystyle{ \exists\, x{:}X \, P }[/math]

There are a few more ways to represent the universal quantifier:

  • [math]\displaystyle{ (x) \, P }[/math]
  • [math]\displaystyle{ \bigwedge_{x} P }[/math]

Several statements above explicitly include X, the set of elements that the quantifier applies to. This set of elements is also known as the range of quantification, or the universe of discourse. Some of the statements above do not include such a set. In this case, the set will have to be specified before the statement. For example, "x is an apple" must be stated before [math]\displaystyle{ \exists{x} P(x) }[/math]. In this case, we are making a statement that at least one apple fits the predicate P.

Using quantifiers formally does not require using the symbol x. The symbol x has been used throughout this article, but any symbol can be used, like y. Make sure not to refer to two different things with the same symbol when choosing symbols.

Nesting

It is important to put quantifiers in the right order. This is an example English sentence showing how meaning changes with order:

For every natural number n, there exists a natural number s such that s = n2.

This statement is true. It states that every natural number has a square. However, if we turn the order of the quantifiers around:

There exists a natural number s, such that for every natural number n, s = n2.

This statement is false. It claims that there is one natural number s that is the square of every natural number.

In certain circumstances changing the order of quantifiers does not change the meaning of the statement. For instance:

There exists a natural number x, and there exists a natural number y such that x = y2.

Other quantifiers

There are also less common quantifiers used by mathematicians.

An example is the solution quantifier[1]. It is used to state which elements solve a particular equation. The solution quantifier is represented by a § (section sign). For example, the following statement claims the squares of 0, 1 and 2 are smaller than 4.  :[math]\displaystyle{ \left [ \S n \in \mathbb{N} \quad n^2 \leq 4 \right ] = \left\{0, 1, 2\right\} }[/math]

Other quantifiers are:

  • There are many elements such that...
  • There are few elements such that...
  • There are infinitely many elements such that...
  • For all but finitely many elements... (sometimes expressed as "for almost all elements...").
  • There are uncountable many elements such that...
  • For all but countably many elements...

History

Term logic was developed by Aristotle. It was an early form of logic, and included quantification. The use of quantification was closer to that of natural language. This meant that statements in term logic with quantifiers were less suited for formal analysis. Term logic included quantifiers for All, Some and No (none) in 4th century BC.

In 1879, Gottlob Frege created a notation for universal quantification. Unlike today, he would represent a universal quantification by writing a variable over a dimple in an otherwise straight line. Frege did not create a notation for existential quantification. Instead, he combined universal quantification and a number of negations to make an equivalent statement. Frege's use of quantification was not widely known until Bertrand Russell's 1903 Principles of Mathematics.

In 1885, Charles Sanders Peirce and his student Oscar Howard Mitchell also created a notation for universal and existential quantifiers. They wrote Πx and Σx where we now write ∀x and ∃x. Pierce's notation was used by many mathematicians into the 1950s.

In 1897, William Ernest Johnson and Giuseppe Peano created another notation for universal and existential quantification. They were influenced by Pierce's previous quantification notation. Johnson and Peano used the simple (x) for universal quantification, and ∃x for existential quantification. Peano's influence on math spread this notation across Europe.

In 1935, Gerhard Gentzen created the ∀ symbol for universal quantification. It was not widely used until the 1960s.

Related pages

References

Template:Wiktionary Template:Reflist