what would be wrong or inadequate with interpreting in ZF types as sets fulfilling certain conditions to avoid dealing with a theory of types or with order-sorted logic?
> Could you say more about what conditions do you have in mind? > As JM pointed out, I can't see why someone would want to avoid to "dealing > with a theory of types or with order-sorted logic" either. Hi Joao and Bruno I'm sorry I took so long to answer your questions, but I wanted first to read all the literature you pointed to, and carefully reflect about my answer. Here it goes... It is natural to think of formal logic as a language to express and reason about mathematical arguments. In fact, two of the main areas of foundational studies, more properly of mathematical logic, have to do with syntax (including proof calculation) and semantics. However, pragmatics is also an important aspect of a working language. According to the article " Why Is Discrete Math Hard To Teach?" in https://rjlipton.wordpress.com/ there, the author proposes 'viewing learning discrete math as learning a new language'. He mentions Viète and Descartes referring to their development of symbolic notations to express and solve numerical equations, which meant a great advance for their time with respect to the unwieldy rhetorical way of reasoning of the Arabs for solving algebraic problems. This was really a breakthrough that boosted further notational and calculational development that allowed to reason mathematically in a more effective way. However, four centuries after that, and in spite of a century of developments in the foundations of mathematics, and in mathematical logic in particular, it seems that there have not been anymore advances in this respect. The author of the above-mentioned article thinks that reasoning must be done through rhetorical arguments. He does not conceive that an analogous achievement to the one done by Viète and Descartes for algebraic reasoning can be (or has been) done for logical reasoning. Well, he must have a point there. So called natural deduction, sequent, tableaux and resolution systems are actually, artificial ways of proving, perhaps appropriate for machine theorem-proving, but not compatible at all with the "rhetoric" with which most mathematicians express their proofs. However, Avigad in his article “Clarifying the nature of the infinite” states: "Logic can be construed as the science of symbolic representations of logical notions, and the means of calculating with them. This viewpoint underlies Leibniz’ notion of a calculus ratiocinator." And also: "Logic [may be viewed] as a branch of algebra or as a mathematical tool in the tradition of Boole and Peirce." Only from a theoretical or a potential point of view can Logic be considered a mathematical tool useful for (human) reasoning and calculation . But, it does not seem to offer anything of practical value to the working mathematician in terms of complementing or clarifying the rhetoric with which he expresses his proofs. I am not against explaining our intuitions using natural (human) languages but, in the same way that the algebraic notations and calculations of Viète and Descartes help to clarify and avoid obscure rhetoric in the daily practice of mathematics, we should expect something analogous from a predicate logic deduction system. This is why I find the theory of types, in particular the mimicking of logic by way of the Curry-Howard isomorphism, very awkward and contrived as a practical tool for effective mathematical reasoning. Please, do not misunderstand me, I considered the Curry-Howard isomorphism a nice and interesting result; and for those interested in Logic as an object of study (and not as a practical tool to express and reason about mathematical arguments ) it is most surely, an area for deep and attractive results. True, there are important advances in mechanical theorem proving based on the calculus of construction, Martin-Lo¨f's dependable theory of types, hott, and so on. But in absence of explanations in terms of the rhetoric used by mathematicians or at least in terms of a formalization compatible with it, they will only work as oracles whose cryptic messages will only be understood by the initiated. Needless to say, this situation is unpalatable for the average mathematician. I wonder which way is easier, adapting machines to the way people reason and express their proofs, or the other way around, adapting people to the way machines better do and express their proofs. Both ways seem to be considerable challenges. (Maybe I would not have a problem working with order-sorted logic, Having to put up with the clutter necessary to express and prove (by hand) a simple argument using those alternative foundations of mathematics is what I do not feel attracted to.) Abrazos calurosos. Jaime -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/BY2PR0101MB0886D1AB225F51495B99B025AD490%40BY2PR0101MB0886.prod.exchangelabs.com.
