Univalent foundations of mathematics are expressed in type theory (homotopy type theory), and type theories are efficient logical and computational frameworks for computer formalization of mathematics. How does this apply to working with category theory, and what is the contribution of univalent foundations to the notion of set that category theory still has to refer to inside type theory? We have a look at the notions of univalence for types, for categories and for bicategories and argue that working with complex categorical structures benefits from computer formalizations, illustrated with the UniMath library of univalent mathematics that was started by the late Vladimir Voevodsky on top of the Coq proof assistant. In particular, the UniMath library exhibits the constructive nature of the logic that is used for mathematical reasoning in general category theory, including many of its applications.
Proof-theoretic semantics is an approach to semantics trying to explain meaning in terms of proofs (as well as the meaning of proofs). This way, proof-theoretic semantics is a recent alternative to the more traditional conception of meaning as denotation reflected by the usual semantics. The idea of our talk is to introduce some fundamental concepts of proof-theoretic semantics, to discuss them and to consider their conceptual relationship, and to obtain this way some basic intuitions about proof-theoretic semantics. We intend to brighten up our talk by some historical comments and examples taken from the literature and our own work.
Subsistem muitas incertezas quanto à data das obras lógicas de Pedro Hispano e à definitiva identificação deste autor. Uma longa tradição tem-no identificado com o português Pedro Julião, que foi papa entre 1276 e 1277 com o nome de João XXI. As duas obras lógicas que lhe estão atribuídas, os Tractatus ou Summulae logicales e os Syncategoremata, ambas compostas em meados do século XIII, tiveram uma extraordinária fortuna literária e académica. Da primeira subsistem centenas de manuscritos e centenas de edições até cerca de 1650, que atestam a imensa influência desta obra na formação básica dos estudantes da maioria das universidades do continente europeu, quase até ao final do século XVII. Nesta conferência serão tratadas três questões: (1) a tradição antiga e medieval da lógica como instrumento do pensamento, (2) a re-sistematização da lógica e as novidades medievais no Tractatus de Pedro Hispano, (3) como o espírito científico europeu foi formado tendo como base o estudo da linguagem e da lógica pelo manual de Pedro Hispano.
