Church, Alonzo
Publié le 22/02/2012
Extrait du document
«
principal expression of this language is an abstraction operator which is used to construct an expression for a
function from an expression for an arbitrary value.
For example, ' ¸x:x 2 ' denotes the function which takes any
number to its square.
The rules of transformation (conversion) of the calculus provide a guide for derivations
among expressions of the above type.
The ¸-calculus has had a significant effect on the development of logic.
It was shown that the original formulation
of the calculus is equivalent to the combinatory logic of Schönfinkel and, for this reason, Church is considered to
be one of the founders of combinatory logic.
The ¸-calculus also played an important role in the development of
intensional logic, particularly in that part of it which takes intensions as functions of a certain type.
A study of general properties of functions led Church to two seminal discoveries concerning the problem of
whether it is possible to make all of mathematics algorithmic.
The first of these was his conjecture concerning a
precise demarcation of the class of functions characterized intuitively as algorithmically or effectively computable.
This conjecture, which has come to be known as 'Church's thesis' , is that this intuitively characterized class of
functions is identical with the precisely characterized class of functions known as general recursive.
The second is Church's proof that the so-called 'decision problem' is unsolvable.
The
general decision problem for mathematics asks whether for every class of mathematical problems there is an
algorithm which decides the answer.
More particularly, the decision problem for predicate logic asks whether there
is an algorithm for deciding logical truth.
Church established a negative answer to both questions.
3 The logic of sense and denotation
Church's work on functions is partly responsible for his interest in developing a theory of intensions.
His
¸-calculus utilizes a notion of 'function -in- intension' (as opposed to 'function -in- extension' ) and he notes that two
functions-in-intension f and g might be different - might, that is, differ in intension or 'meaning' - even if they
share the same domain of arguments and for each n-tuple of objects a1; : : : ; a n of that domain,
f(a1; : : : ; a n) = g(a1; : : : ; a n).
In his earlier work, the notion of difference in meaning was left unexplained.
The
last four decades, however, he devoted to developing a theory of this difference in meaning.
The result was his
'logic of sense and denotation' , based on Frege's theory of proper names.
Church follows Frege in assigning two sorts of semantic values to proper names.
A proper name is said to express
its 'sense' and to name its 'denotation' (or 'reference' ).
Frege and Church are of the view that two names having
the same denotation might none the less differ in sense.
Another characteristic feature of the Frege-Church theory is that declarative sentences are treated as names.
They
express their senses (propositions), and denote (or name) their truth-values.
Like Frege, Church also distinguished between two uses of proper names: the ordinary and the oblique.
The
principal criterion for obliqueness is the failure of substitutivity for equality ( =), and for material equivalence.
»
↓↓↓ APERÇU DU DOCUMENT ↓↓↓
Liens utiles
- Vincent van Gogh I INTRODUCTION Church at Auvers by Van Gogh Dutch artist Vincent van Gogh spent the last months of his life in Auvers-sur-Oise, near Paris, under the care of Dr.
- George Frideric Handel I INTRODUCTION Handel's Water Music In addition to his popular operas and oratorios, German-born composer George Frideric Handel wrote music in the 1700s for the church and for royal celebrations.
- Church (building) I INTRODUCTION Church (building), a building designed for worship for groups of Christians.
- Church's theorem and the decision problem
- Roman Catholic Church.