Evento em Epistemologia Contemporânea

[Rafael Testa]

Prezados,

aproveito o espaço para convidar a todos para o Workshop em Epistemologia Contemporânea, que será realizado no CLE-Unicamp na próxima semana. O foco será basicamente representação formal do conhecimento e revisão de crenças (o que poderíamos englobar como Epistemologia Formal).

Mais informações no link:
https://gamerationality.wordpress.com/events/1st_epic/

Gostaria de divulgar o grupo recém criado GAME: Group for Analytic Metaphysics and Epistemology, e convidá-los para participar do mesmo. Por enquanto somos apenas dois :) Este workshop é nossa primeira atividade aberta, justamente para divulgar nossa iniciativa, e conta com a colaboração de professores do Departamento de Filosofia (Unicamp), além do apoio do CLE e suporte financeiro da Fapesp.

Abraços,

Rafael Testa
Research associate and postdoctoral fellow
Centre for Logic, Epistemology and the History of Science (CLE-Unicamp)
page: www.rafaeltesta.com.br

[JAIME ALEJANDRO BOHORQUEZ VILLAMIZAR]

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-Lö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