Sessão Especial de Lógica Matemática - 1st Joint Meeting Brazil Mexico in Mathematics
38 views
Skip to first unread message
samuel
Aug 27, 2025, 11:14:20 AM (12 days ago) Aug 27
to LOGICA-L
Prezados,
Seguindo com a tradição de manter sessões especiais de Lógica Matemática nos encontros bilaterais entre a Sociedade Brasileira de Matemática e suas homólogas de outros países nos últimos anos (Brasil-Espanha 2015, Brasil-Italia 2016, Brasil-França 2019 e Brasil-Portugal 2022, não esquecendo da palestra da Profa. Itala D'Ottaviano no Brasil-Estados Unidos de 2008), sempre com o apoio da Sociedade Brasileira de Lógica,
Segue a programação da Sessão Especial de Lógica Matemática no 1st Joint Meeting Brazil México in Mathematics, evento esse que vai ocorrer entre os dias 08 e 12 de Setembro em Fortaleza, Ceará, no Hotel Mareiro.
A Sessão Especial de Lógica Matemática vai ocorrer nas tardes da segunda e da terça-feira, dias 08 e 09 de Setembro.
Programação:
Lunes, 08 Septiembre
14h-14h30 Claudia Nalon (UnB)
14h30-15h Nancy Nunez (UNAM)
15h-15h30 Francisco Hernandez Quiroz (UNAM)
15h30-16h30 Coffee Break
16h30-17h Favio Miranda Perea (UNAM)
17h-17h30 Daniel Ventura (UFG)
17h30-18h Lourdes Gonzales Huesca (UNAM)
Martes, 09 Septiembre
14h-14h30 Ulises Ariet Ramos Garcia (UNAM Morelia)
14h30-15h Samuel Gomes da Silva / Ciro Russo (UFBA)
15h-15h30 Salvador Garcia-Ferreira (UNAM Morelia)
15h30-16h30 Coffee break
Resumos:
***************************************************************************************
Claudia Nalon (UnB (Brazil))
Title of the talk: Automated Reasoning for Non-Classical Logics
Abstract of the talk: We will discuss two different resolution-based calculi for the multimodal logic Kn with particular focus on the characteristics that have impact on theorem-proving. We will report on experimental results and the influence of proof strategies and processing techniques for both calculi.
Francisco Hern\'andez Quiroz (UNAM FCiencias (México))
Title of the talk: Inferential Information Complexity
Abstract of the talk: An analogous to Kolmogorov complexity can be used to measure the epistemic contribution of deduction. Minimal proof length (in terms of inferential steps) in decidable systems is a good indication of the minimal information needed to prove a theorem. This measure is independent of the chosen proof system, provided it meets some natural requirements.
Salvador Garcia-Ferreira (UNAM (Morelia, México))
Title of the talk: Semigroup actions and filters
Abstract of the talk: We will show the importance of certain filters on a semigroup when it acts on a compact metric space. Mainly, in the study of the invariant closed subsets. We give several examples of such filters in various semigroups. We present also examples of actions of semigroups on countable compact metric spaces.
Samuel Gomes da Silva (UFBA (Brazil))
Title of the talk: On Forcing Axioms and Weakenings of the Axiom of Choice\\
Abstract of the talk: We prove forcing axiom equivalents of two families of weakenings of the Axiom of Choice (like the hundreds listed in the standard reference Howard and Rubin, ``Consequences of the Axiom of Choice''):
a trichotomy principle for cardinals isolated by L\'evy, $H_\kappa$, and $DC_\kappa$, the principle of dependent choices generalized to cardinals $\kappa$, for regular cardinals $\kappa$. Using these equivalents we obtain new forcing axiom formulations of the Axiom of Choice, $\mathbf{AC}$. A point of interest is that we use a new template for forcing axioms. For the class of forcings to which we asks that the axioms apply, we do not ask that they apply to all collections of dense sets of a certain cardinality (as previously done by Viale and others), but rather only for each particular forcing to a specific family of dense sets of the cardinality in question.
Ciro Russo (UFBA (Brazil))
Title of the talk: Priestley-type Duality for positive MV-algebras \\
Abstract of the talk: In this talk we shall present a Priestley-type duality between positive MV algebras and a suitable class of ordered fuzzy topological spaces. The duality theorem will include, as special cases, both the classical Priestley duality and the Stone-type duality proved by the speaker in a previous work.
Ulises Ariet Ramos-Garcia (UNAM MatMorelia (México))
Title of the talk: Hindman-tall ideals and the Ramsey property for pairs in ordered-union ultrafilters
Abstract of the talk: We will show an equivalence between the Ramsey's property for pairs in ordered-union ultrafilters on FIN in terms of Hindman-tall ideals on FIN. This characterization is useful to address an old problem of A. Blass asking if every ordered-union ultrafilter has the Ramsey's property for pairs. This work is in collaboration with Angel Augusto Camacho-Acosta and Carlos L\'opez-Callejas.
Daniel Ventura (UFG (Brazil))
Title of the talk: Linearisation Based on Normalisation Strategies\\
Abstract of the talk: Linear terms/functions have interesting properties, such as no infinite reductions, typability in polynomial time, and simpler and optimised abstract machines for their execution, due to their no-duplication operational semantics. Linearisation of strong-normalising terms has been proposed based on typing information an intersection types system provides. More recently, a weak-linearisation procedure --originally defined through a static characterisation of virtual redices, based on legal paths computed from the term syntactic tree--, was devised based on a quantitative type system. In such a procedure, functions not applied in any reduction path are not linearised. Therefore, the quantitative system provides information related to a maximal normalisation strategy. In this work, we explore linearisation procedures based on different normalisation strategies.
Favio Ezequiel Miranda Perea (UNAM (México))
Title of the talk: TBA
Abstract of the talk: TBA
Lourdes del Carmen Gonzalez Huesca (UNAM (México))
Title of the talk: TBA
Abstract of the talk: TBA
Nancy Abigail Nunez Hernandez (UNAM-FES, Acatlan (México))
Title of the talk: Why AI is not going to take mathematicians' jobs (or on the complexity of mathematicians' jobs)
Abstract of the talk: The rapid development of AI is causing a lot of concern among many people working in a wide variety of fields: teachers, journalists, lawyers, physicians, and even programmers are worried about losing their jobs to some form of AI. The question that I want to explore in this work is whether AI can also take mathematicians' jobs. In 1956, G\"odel wrote to von Neuman inquiring whether "the reasoning of mathematicians about yes-or-no questions can be completely replaced by machines." (Hartmanis 1993, p. 6) This letter has become famous among theoretical computer scientists interested in the open problem of determining if P and NP are different complexity classes. Although G\"odel was inquiring about an NP-complete problem (Buss 1995), a mathematician's job is also directly related to coNP-complete problems; for instance, when they have to decide whether a given sentence follows from some set of axioms or other theorems. This work proposes that because of the complexity of the problems mathematicians deal with, AI should not be able to take their jobs so easily.
Title of the talk: Automated Reasoning for Non-Classical Logics
Abstract of the talk: We will discuss two different resolution-based calculi for the multimodal logic Kn with particular focus on the characteristics that have impact on theorem-proving. We will report on experimental results and the influence of proof strategies and processing techniques for both calculi.
Francisco Hern\'andez Quiroz (UNAM FCiencias (México))
Title of the talk: Inferential Information Complexity
Abstract of the talk: An analogous to Kolmogorov complexity can be used to measure the epistemic contribution of deduction. Minimal proof length (in terms of inferential steps) in decidable systems is a good indication of the minimal information needed to prove a theorem. This measure is independent of the chosen proof system, provided it meets some natural requirements.
Salvador Garcia-Ferreira (UNAM (Morelia, México))
Title of the talk: Semigroup actions and filters
Abstract of the talk: We will show the importance of certain filters on a semigroup when it acts on a compact metric space. Mainly, in the study of the invariant closed subsets. We give several examples of such filters in various semigroups. We present also examples of actions of semigroups on countable compact metric spaces.
Samuel Gomes da Silva (UFBA (Brazil))
Title of the talk: On Forcing Axioms and Weakenings of the Axiom of Choice\\
Abstract of the talk: We prove forcing axiom equivalents of two families of weakenings of the Axiom of Choice (like the hundreds listed in the standard reference Howard and Rubin, ``Consequences of the Axiom of Choice''):
a trichotomy principle for cardinals isolated by L\'evy, $H_\kappa$, and $DC_\kappa$, the principle of dependent choices generalized to cardinals $\kappa$, for regular cardinals $\kappa$. Using these equivalents we obtain new forcing axiom formulations of the Axiom of Choice, $\mathbf{AC}$. A point of interest is that we use a new template for forcing axioms. For the class of forcings to which we asks that the axioms apply, we do not ask that they apply to all collections of dense sets of a certain cardinality (as previously done by Viale and others), but rather only for each particular forcing to a specific family of dense sets of the cardinality in question.
Ciro Russo (UFBA (Brazil))
Title of the talk: Priestley-type Duality for positive MV-algebras \\
Abstract of the talk: In this talk we shall present a Priestley-type duality between positive MV algebras and a suitable class of ordered fuzzy topological spaces. The duality theorem will include, as special cases, both the classical Priestley duality and the Stone-type duality proved by the speaker in a previous work.
Ulises Ariet Ramos-Garcia (UNAM MatMorelia (México))
Title of the talk: Hindman-tall ideals and the Ramsey property for pairs in ordered-union ultrafilters
Abstract of the talk: We will show an equivalence between the Ramsey's property for pairs in ordered-union ultrafilters on FIN in terms of Hindman-tall ideals on FIN. This characterization is useful to address an old problem of A. Blass asking if every ordered-union ultrafilter has the Ramsey's property for pairs. This work is in collaboration with Angel Augusto Camacho-Acosta and Carlos L\'opez-Callejas.
Daniel Ventura (UFG (Brazil))
Title of the talk: Linearisation Based on Normalisation Strategies\\
Abstract of the talk: Linear terms/functions have interesting properties, such as no infinite reductions, typability in polynomial time, and simpler and optimised abstract machines for their execution, due to their no-duplication operational semantics. Linearisation of strong-normalising terms has been proposed based on typing information an intersection types system provides. More recently, a weak-linearisation procedure --originally defined through a static characterisation of virtual redices, based on legal paths computed from the term syntactic tree--, was devised based on a quantitative type system. In such a procedure, functions not applied in any reduction path are not linearised. Therefore, the quantitative system provides information related to a maximal normalisation strategy. In this work, we explore linearisation procedures based on different normalisation strategies.
Favio Ezequiel Miranda Perea (UNAM (México))
Title of the talk: TBA
Abstract of the talk: TBA
Lourdes del Carmen Gonzalez Huesca (UNAM (México))
Title of the talk: TBA
Abstract of the talk: TBA
Nancy Abigail Nunez Hernandez (UNAM-FES, Acatlan (México))
Title of the talk: Why AI is not going to take mathematicians' jobs (or on the complexity of mathematicians' jobs)
Abstract of the talk: The rapid development of AI is causing a lot of concern among many people working in a wide variety of fields: teachers, journalists, lawyers, physicians, and even programmers are worried about losing their jobs to some form of AI. The question that I want to explore in this work is whether AI can also take mathematicians' jobs. In 1956, G\"odel wrote to von Neuman inquiring whether "the reasoning of mathematicians about yes-or-no questions can be completely replaced by machines." (Hartmanis 1993, p. 6) This letter has become famous among theoretical computer scientists interested in the open problem of determining if P and NP are different complexity classes. Although G\"odel was inquiring about an NP-complete problem (Buss 1995), a mathematician's job is also directly related to coNP-complete problems; for instance, when they have to decide whether a given sentence follows from some set of axioms or other theorems. This work proposes that because of the complexity of the problems mathematicians deal with, AI should not be able to take their jobs so easily.
****************************************************************************************
Todos os interessados que possam comparecer, sintam-se fortemente convidados !
Atenciosamente
[]s Samuel, em nome dos organizadores da Sessão (Samuel e João Marcos pelo Brasil, Lourdes Huesca e Favio Miranda-Perea pelo México).
samuel
Sep 3, 2025, 1:58:10 PM (5 days ago) Sep 3
to LOGICA-L, samuel
... Complementando com os resumos de Favio Miranda Perea e Lourdes Huesca, da UNAM:
Title of the talk: A global Curry-Howard correspondence for strong normalization in intuitionistic logic.
Abstract of the talk: Normalization theorems are pillars of Proof Theory, since they ensure that any derivation, usually in Natural Deduction, can be transformed in a specific proof having no detours, and in the case of strong normalization this can be done by simplifying redundancies in an arbitrary way. We can classify normalization proofs as diagrammatical or algebraic, the former are those native of the Gentzen-Prawitz tradition where the argumentations depend on the manipulation of proof-tree diagrams, whereas the latter are based on lambda calculi where discussions are purely algebraic, justified by the well-known Curry-Howard correspondence. However, both approaches are separated by an explanatory gap which prohibits the interpretation of lambda terms by proof trees in a non-local manner. That is, beyond the mapping of a lambda term into a particular instance of an inference rule. In this talk we propose an algebraic proof representation by means of enhanced lambda terms that capture not only the proof search process of a detour but also provide an encoding of global proof trees including ellipsis, which are common in structural proof theory arguments. This way we provide a lambda calculus which conciliates both approaches in the case of intuitionistic logic, allowing to construct a mechanizable strong normalization proof that keeps the proof-theoretical intuition, thus providing not only guarantee but explanation. This research is being supported by UNAM-DGAPA-PAPIIT grant IN101723.
Abstract of the talk: In proof-assistants, there are proof methodologies that are non directly referred to deductive systems. There is a gap between a formal system or logic, for instance, the Calculus of Inductive Constructions, and the practical side of it.
In this talk, we analyse the useful \texttt{apply} tactic in the Rocq proof-assistant. The internal mechanism of Rocq does not show a transparent application of the tactic, while in a deductive system can be seen as an iterated application of left-rules for the operators `forall' and `implication'. The proposal of a multiary rule corresponding to the \texttt{apply} tactic gives a family of rule-schemas showing the low-level requirements of such tactic.
Favio Ezequiel Miranda Perea (UNAM FCiencias (M\'exico))
Title of the talk: A global Curry-Howard correspondence for strong normalization in intuitionistic logic.
Abstract of the talk: Normalization theorems are pillars of Proof Theory, since they ensure that any derivation, usually in Natural Deduction, can be transformed in a specific proof having no detours, and in the case of strong normalization this can be done by simplifying redundancies in an arbitrary way. We can classify normalization proofs as diagrammatical or algebraic, the former are those native of the Gentzen-Prawitz tradition where the argumentations depend on the manipulation of proof-tree diagrams, whereas the latter are based on lambda calculi where discussions are purely algebraic, justified by the well-known Curry-Howard correspondence. However, both approaches are separated by an explanatory gap which prohibits the interpretation of lambda terms by proof trees in a non-local manner. That is, beyond the mapping of a lambda term into a particular instance of an inference rule. In this talk we propose an algebraic proof representation by means of enhanced lambda terms that capture not only the proof search process of a detour but also provide an encoding of global proof trees including ellipsis, which are common in structural proof theory arguments. This way we provide a lambda calculus which conciliates both approaches in the case of intuitionistic logic, allowing to construct a mechanizable strong normalization proof that keeps the proof-theoretical intuition, thus providing not only guarantee but explanation. This research is being supported by UNAM-DGAPA-PAPIIT grant IN101723.
Lourdes del Carmen Gonz\'alez Huesca (UNAM FCiencias (M\'exico))
Title of the talk: On multiary rules
Abstract of the talk: In proof-assistants, there are proof methodologies that are non directly referred to deductive systems. There is a gap between a formal system or logic, for instance, the Calculus of Inductive Constructions, and the practical side of it.
In this talk, we analyse the useful \texttt{apply} tactic in the Rocq proof-assistant. The internal mechanism of Rocq does not show a transparent application of the tactic, while in a deductive system can be seen as an iterated application of left-rules for the operators `forall' and `implication'. The proposal of a multiary rule corresponding to the \texttt{apply} tactic gives a family of rule-schemas showing the low-level requirements of such tactic.
Reply all
Reply to author
Forward
0 new messages