Ruy de Queiroz

Last updated
Ruy de Queiroz Ruy de Queiroz bw.jpg
Ruy de Queiroz

Ruy J. Guerra B. de Queiroz (born January 11, 1958 in Recife) is an associate professor at Universidade Federal de Pernambuco and holds significant works in the research fields of Mathematical logic, proof theory, foundations of mathematics and philosophy of mathematics. [1] He is the founder of the Workshop on Logic, Language, Information and Computation (WoLLIC), which has been organised annually since 1994, typically in June or July.

Contents

Ruy de Queiroz received his B.Eng in Electrical Engineering from Escola Politecnica de Pernambuco in 1980, his M.Sc in Informatics from Universidade Federal de Pernambuco in 1984, and his Ph.D in Computing from the Imperial College, London in 1990, for which he defended the Dissertation Proof Theory and Computer Programming. An Essay into the Logical Foundations of Computation.

Research profile

In the late 1980s, Ruy de Queiroz has offered a reformulation of Martin-Löf type theory based on a novel reading of Wittgenstein’s "meaning-is-use", where the explanation of the consequences of a given proposition gives the meaning to the logical constant dominating the proposition. This amounts to a non-dialogical interpretation of logical constants via the effect of elimination rules over introduction rules, which finds a parallel in Paul Lorenzen's and Jaakko Hintikka's dialogue/game-semantics. This led to a type theory called "Meaning as Use Type Theory". [2] In reference to the use of Wittgenstein's dictum, he has shown that the aspect concerning the explanation of the consequences of a proposition is present since a very early date when in a letter to Bertrand Russell, where Wittgenstein refers to the universal quantifier only having meaning when one sees what follows from it. [3]

Since later in the 1990s, Ruy de Queiroz has been engaged, jointly with Dov Gabbay, in a program of providing a general account of the functional interpretation of classical and non-classical logics via the notion of labeled natural deduction. As a result, novel accounts of the functional interpretation of the existential quantifier, as well as the notion of propositional equality, were put forward, the latter allowing for a recasting of Richard Statman's notion of direct computation, and a novel approach to the dichotomy "intensional versus extensional" accounts of propositional equality via the Curry–Howard correspondence.

Since the early 2000s, Ruy de Queiroz has been investigating, jointly with Anjolina de Oliveira, a geometric perspective of natural deduction based on a graph-based account of Kneale's symmetric natural deduction. [4]

Service to the profession

Key publications

  1. (with de Oliveira, A.) The Functional Interpretation of Direct Computations. Electronic Notes in Theoretical Computer Science 269:19-40, 2011.
  2. On reduction rules, meaning-as-use, and proof-theoretic semantics, Studia Logica 90(2):211-247, November 2008.
  3. (with de Oliveira, A.) Geometry of Deduction via Graphs of Proof. In Logic for Concurrency and Synchronisation, R. de Queiroz (ed.), volume 18 of the Trends in Logic series, Kluwer Acad. Pub., Dordrecht, July 2003, ISBN   1-4020-1270-5, pp. 3–88.
  4. Meaning, function, purpose, usefulness, consequences - interconnected concepts. Logic Journal of the Interest Group in Pure and Applied Logics, 9(5):693-734, September 2001, Oxford Univ. Press.
  5. (with Gabbay, D.) Labelled Natural Deduction. In Logic, Language and Reasoning. Essays in Honor of Dov Gabbay, H.J. Ohlbach and U. Reyle (eds.), volume 5 of Trends in Logic series, Kluwer Academic Publishers, Dordrecht, June 1999, pp. 173–250.
  6. (with de Oliveira, A.) A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction. Logic Journal of the Interest Group in Pure and Applied Logics, 7(2):173-215, 1999, Oxford Univ. Press. Full version of a paper presented at 2nd WoLLIC'95, Recife, Brazil, July 1995. Abstract appeared in Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.
  7. (with Gabbay, D.) The Functional Interpretation of the Existential Quantifier, in Bulletin of the Interest Group in Pure and Applied Logics 3(2-3):243-290, 1995. (Special Issue on Deduction and Language, Guest Editor: Ruth Kempson). Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.
  8. Normalisation and Language-Games. In Dialectica 48(2):83-123, 1994. (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
  9. (with Gabbay, D.) Extending the Curry-Howard interpretation to linear, relevant and other resource logics, in Journal of Symbolic Logic 57(4):1319-1365. Paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.
  10. (with Maibaum, T.) Abstract Data Types and Type Theory: Theories as Types, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 37:149-166.
  11. (with Maibaum, T.) Proof Theory and Computer Programming, in Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36:389-414.
  12. A Proof-Theoretic Account of Programming and the Rôle of Reduction Rules, in Dialectica 42(4):265-282.
  13. de Queiroz, R. de Oliveira, A., & Gabbay, D.: 2011, The Functional Interpretation of Logical Deduction. Vol. 5 of Advances in Logic series. Imperial College Press / World Scientific. ISBN   978-981-4360-95-1.

Teaching

Ruy de Queiroz has taught several disciplines related to logic and theoretical computer science, including Set Theory, Recursion Theory (as a follow-up to a course given by Solomon Feferman), Logic for Computer Science, Discrete Mathematics, Theory of Computation, Proof Theory, Model Theory, Foundations of Cryptography. He has had seven Ph.D. students in the fields of Mathematical Logic and Theoretical Computer Science.

Honors and awards

Related Research Articles

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

<span class="mw-page-title-main">History of logic</span> Study of the history of the science of valid inference

The history of logic deals with the study of the development of the science of valid inference (logic). Formal logics developed in ancient times in India, China, and Greece. Greek methods, particularly Aristotelian logic as found in the Organon, found wide application and acceptance in Western science and mathematics for millennia. The Stoics, especially Chrysippus, began the development of predicate logic.

Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

Metalogic is the study of the metatheory of logic. Whereas logic studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems. Logic concerns the truths that may be derived using a logical system; metalogic concerns the truths that may be derived about the languages and systems that are used to express truths.

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax.

Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes.

<span class="mw-page-title-main">Samson Abramsky</span> British computer scientist

Samson Abramsky is Professor of Computer Science at University College London. He has made contributions to the areas of domain theory, the lazy lambda calculus, strictness analysis, concurrency theory, interaction categories, geometry of interaction, game semantics and quantum computing.

In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics include notion of compound connectives, using a technique known as focusing or focalisation, and its use of locations or loci over a base instead of propositions.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

Giorgi Japaridze is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze is best known for his invention of computability logic, cirquent calculus, and Japaridze's polymodal logic.

Non-classical logics are formal systems that differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done, including by way of extensions, deviations, and variations. The aim of these departures is to make it possible to construct different models of logical consequence and logical truth.

Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.

In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic. The name of the interpretation comes from the journal Dialectica, where Gödel's paper was published in a 1958 special issue dedicated to Paul Bernays on his 70th birthday.

WoLLIC, the Workshop on Logic, Language, Information and Computation is an academic conference in the field of pure and applied logic and theoretical computer science. WoLLIC has been organised annually since 1994, typically in June or July; the conference is scientifically sponsored by the Association for Logic, Language and Information, the Association for Symbolic Logic, the European Association for Theoretical Computer Science and the European Association for Computer Science Logic.

Dialogical logic was conceived as a pragmatic approach to the semantics of logic that resorts to concepts of game theory such as "winning a play" and that of "winning strategy".

<span class="mw-page-title-main">Logic</span> Study of correct reasoning

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises in a topic-neutral way. When used as a countable noun, the term "a logic" refers to a logical formal system that articulates a proof system. Formal logic contrasts with informal logic, which is associated with informal fallacies, critical thinking, and argumentation theory. While there is no general agreement on how formal and informal logic are to be distinguished, one prominent approach associates their difference with whether the studied arguments are expressed in formal or informal languages. Logic plays a central role in multiple fields, such as philosophy, mathematics, computer science, and linguistics.

Valeria Correa Vaz de Paiva is a Brazilian mathematician, logician, and computer scientist. Her work includes research on logical approaches to computation, especially using category theory, knowledge representation and natural language semantics, and functional programming with a focus on foundations and type theories.

References

  1. ↑ GABBAY, Dov M.; WOODS, John (2009-04-27). The International Directory of Logicians. College Publications. ISBN   978-1-904987-90-1 . Retrieved 2011-07-28.
  2. ↑ de Queiroz, R. "Meaning as grammar plus consequences", in Dialectica 45(1):83-86.
  3. ↑ de Queiroz, R. "The mathematical language and its semantics: to show the consequences of a proposition is to give its meaning". In Weingartner, Paul and Schurz, Gerhard, editors, Reports of the Thirteenth International Wittgenstein Symposium 1988, volume 18 of Schriftenreihe der Wittgenstein-Gesellschaft, Vienna, 304pp. Hölder–Pichler–Tempsky, pp. 259–266. Symposium held in Kirchberg/Wechsel, Austria, August 14–21, 1988.
  4. ↑ de Queiroz; de Oliveira (2011). "Propositional equality, identity types, and direct computational paths". arXiv: 1107.1901 [cs.LO].
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.