|
Results for criterions:- Keyword: Function
Modify search criterions 4 matches
| Title |
Critical analysis of variable (semiotic and formal viewpoints) [second part] |
| Author |
DESCLES Jean-Pierre, CHEONG Kye-Seop |
| Keywords |
Algebra, Combinatory logic, Function, Quantification, Semiotics, Variable |
| Topics |
Combinatorics, Linguistics, Logic, Semiology |
| Abstract |
For B. Russell «The variable is perhaps the most distinctively mathematical of all notions ; it is certainly also one of the most difficult to understand» (The Principles of Mathematics, 1903). The aim of this paper is to highlight the meaning of variable in different fields of Mathematics: the expression of equations in Algebra with indeterminate entities; the analytical expression of functions in Analysis; the expression of quantification in Logic. We give a historical survey of this notion from Viète and Descartes to Frege's representations of a concept, viewed as a non numerical function, yielding to the modern theory of quantification in first order languages. On one hand, the Peirce's theory of signs, and on the other hand, with Church's functional types, l-calculus «with bound variables» and Curry's combinatory logic «without bound variables», are very useful tools for investigating different kinds of variables in Mathematics, in Logic and in theoretical Computer Sciences. For instance, it was showed that «bound variables» were not semiotic tools necessary to formulate quantification (in Frege's sense) in «classical» Logic. Indeed, a simple quantifier is an operator which applies to a predicate by building a proposition; restricted quantifiers are derived from simple quantifiers by formal combinations with logical connectors (conditional or conjunction operators). We propose to take into account and to formalize, inside the framework of Combinatory Logic with types, (i) the «old logical notions» of «extension / intension»; (ii) determination operations from Port Royal's Logic; (iii) the distinction from the anthropology and cognitive psychology between «typical» and «atypical» instances of a concept, which brings us to define new quantifiers, called «star quantifiers», conceived as determination operators acting on terms. These quantifiers are more adequate than the fregean quantifiers, for a natural languages processing. Thus, we are able to give a conceptual distinction between the meanings of «Whatever» and «Indeterminate», implicitly used in Gentzen's Natural Deduction; thanks to this distinction, we can clarify an apparent «paradox» emerging with the universal quantifier introduction rule. |
| Number |
174, Summer 2006 |
| Language |
French | Read the article
| Title |
Critical Analysis of Variable (Semiotic and Formal Viewpoints) [First part] |
| Author |
DESCLES Jean-Pierre, CHEONG Kye-Seop |
| Keywords |
Algebra, Combinatory logic, Correlation, Function, Quantification, Semiotics, Variable |
| Topics |
Algebra, Linguistics, Logic, Modelling, Semiology |
| Abstract |
For B. Russell «The variable is perhaps the most distinctively mathematical of all notions ; it is certainly also one of the most difficult to understand» (The Principles of Mathematics, 1903). The aim of this paper is to highlight the meaning of variable in different fields of Mathematics: the expression of equations in Algebra with indeterminate entities; the analytical expression of functions in Analysis; the expression of quantification in Logic. We give a historical survey of this notion from Viète and Descartes to Frege's representations of a concept, viewed as a non numerical function, yielding to the modern theory of quantification in first order languages. On one hand, the Peirce's theory of signs, and on the other hand, with Church's functional types, ?-calculus «with bound variables» and Curry's combinatory logic «without bound variables», are very useful tools for investigating different kinds of variables in Mathematics, in Logic and in theoretical Computer Sciences. For instance, it was showed that «bound variables» were not semiotic tools necessary to formulate quantification (in Frege's sense) in «classical» Logic. Indeed, a simple quantifier is an operator which applies to a predicate by building a proposition; restricted quantifiers are derived from simple quantifiers by formal combinations with logical connectors (conditional or conjunction operators). We propose to take into account and to formalize, inside the framework of Combinatory Logic with types, (i) the «old logical notions» of «extension / intension»; (ii) determination operations from Port Royal's Logic; (iii) the distinction from the anthropology and cognitive psychology between «typical» and «atypical» instances of a concept, which brings us to define new quantifiers, called «star quantifiers», conceived as determination operators acting on terms. These quantifiers are more adequate than the fregean quantifiers, for a natural languages processing. Thus, we are able to give a conceptual distinction between the meanings of «Whatever» and «Indeterminate», implicitly used in Gentzen's Natural Deduction; thanks to this distinction, we can clarify an apparent «paradox» emerging with the universal quantifier introduction rule. |
| Number |
173, Spring 2006 |
| Language |
French | Read the article
| Title |
Type theory and proof processing system |
| Author |
DOWEK Gilles |
| Keywords |
Computation, Deduction, Function, Mathematical language, Proof, Proof processing systems, Set theory, Type theory |
| Topics |
Computer Sciences, Computing, Logic, Sets, Software |
| Abstract |
Since the end of the sixties, several computer programs allowing to process mathematical knowledge, and in particular mathematical proofs, have been designed. Building such programs raises new questions, in particular that of the conception of logical frameworks where mathematics can be formalized in practice. This is a new direction for fundational studies, more interested, so far, in formalization of mathematics in principle, than in practice. Several reasons explain that the designers of such programs often chose type theory rather than set theory to formalize mathematics. |
| Number |
165, Spring 2004, special issue: Constructive type theory |
| Language |
French | Read the article
Users rights :

The entire journal is licensed under a Creative Commons license
|