Dear Cheerful Logicians and Friends of Logic, There will be no official supergroup talk this week, as we are attempting to avoid having as many scheduling conflicts this week as we had last week. That said, there are many excellent logic events going on. Before detailing the individual talks below, a reminder: On 5-6 November, the University of Melbourne will host an Applied Proof Theory Workshop to mark the end of the Australian Research Council-funded project Meaning in Action. The workshop webpage is https://blogs.unimelb.edu.au/logic/applied-proof-theory-workshop/. To register as a participant, please email either Shawn Standefer ( [email protected]) or Greg Restall ([email protected]).
One further note: this week the US did its semiannual timezone shennaniganry. So, from now until March, I'll be posting all times in GMT-6 rather than GMT-5. There are also four talks being hosted by member groups this week: one each on Monday, Wednesday, Thursday, and Friday. Details are below. *Logic and Metaphysics Workshop* (CUNY) *Speaker: *Heinrich Wansing *Title: *A Note on Synonymy in Proof-Theoretic Semantics *Time and Date: *Monday, November 2nd, 15:15 GMT-6 *Link:* https://gc-cuny.zoom.us/j/95564820696?pwd=RWRObUN3RFQ1M0ZBS0lKR2ZpK3lKQT09 *Meeting ID:* 955 6482 0696 *Passcode:* 381972 *Abstract: *The topic of identity of proofs was put on the agenda of general (or structural) proof theory at an early stage. The relevant question is: When are the differences between two distinct proofs (understood as linguistic entities, proof figures) of one and the same formula so inessential that it is justified to identify the two proofs? The paper addresses another question: When are the differences between two distinct formulas so inessential that these formulas admit of identical proofs? The question appears to be especially natural if the idea of working with more than one kind of derivations is taken seriously. If a distinction is drawn between proofs and disproofs (or refutations) as primitive entities, it is quite conceivable that a proof of one formula amounts to a disproof of another formula, and vice versa. The paper develops this idea. *Helsinki Logic Seminar* *Speaker: *Ralf Schindler *Title: *Martin's Maximum^++ implies the P_max axiom (*) *Time and Date: *Wednesday, November 4th 04:00 GMT-6 *Link: * https://us02web.zoom.us/j/4762106037?pwd=ckc1UzhDSHJmQ3I2bEpmNjNWcDNsZz09 *Abstract: *Forcing axioms spell out the dictum that if a statement can be forced, then it is already true. The P_max axiom (*) goes beyond that by claiming that if a statement is consistent, then it is already true. Here, the statement in question needs to come from a resticted class of statements, and "consistent" needs to mean "consistent in a strong sense." It turns out that (*) is actually equivalent to a forcing axiom, and the proof is by showing that the (strong) consistency of certain theories gives rise to a corresponding notion of forcing producing a model of that theory. This is joint work with D. Asperó building upon earlier work of R. Jensen and (ultimately) Keisler's "consistency properties." *Lógicos em Quarentena* *Speaker: *Carlos Olarte *Title: *The L-Framework*: Structural Proof Theory in Rewriting Logic *Time and Date: *Thursday, November 5th 13:00 GMT-6 *Link: *https://meet.google.com/pkq-fxvz-iou *Abstract: *Structural properties such as admissibility and invertibility of rules are crucial in proof theory, and they can be used for establishing other key properties such as cut-elimination and completeness of focusing in sequent systems. Finding proofs for these properties requires inductive reasoning over the provability relation, which is often quite elaborated, exponentially exhaustive, and error prone. We propose automatic procedures for proving structural properties of sequent systems. Our techniques are based on the rewriting logic metalogical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in Maude and the resulting framework is generic and modular since cut-freeness, admissibility, and invertibility can be proved incrementally. The L-Framework achieves a great degree of automation when used on several sequent systems. Case studies include intuitionistic, classical, substructural and modal logics. *Logic Webinar@IITK* *Speaker: *Prof Friedrich Wehrung (Universite de Caen, France) *Title: *Purity and freshness (in categorial model theory) *Time and Date: *Friday, November 6th 04:30 GMT-6 *Link: *https://zoom.us/j/91420898789?pwd=WnRqWGhYRVEvd0pwZXpkaEd6WDB1dz09 *Meeting ID: *914 2089 8789 *Passcode*: 874519 *Abstract*: The aim of this talk is to introduce the basic concepts of a technique enabling to prove that certain naturally defined classes of structures are ``intractable’’ in the sense that they cannot be described as classes of models of any infinitely formula (or more generally, of any class of $L_{\infty,\lambda}$ formulas, for any infinite cardinal $\lambda$). The main idea is that for any suitably ``continuous’’ functor $F$, from the category of all subsets of some set $X$ and one-to-one maps between those, to a category $C$ of models, all large enough morphisms in the range of $F$ are elementary embeddings with respect to large infinitary languages. This yields the concept of anti-elementarity, which entails intractability. In particular, this applies to classes such as (1) the class of all posets of finitely generated ideals in rings, (2) the class of all ordered $K_0$ groups of unit-regular rings, (3) the class of all lattices of principal $l$-ideals of abelian lattice-ordered groups (yields a negative answer to the so-called MV-spectrum problem). Other Notes and Announcements: - *The Logic Supergroup has a YouTube channel!* Recordings of almost all talks are available at https://www.youtube.com/channel/UCqOAS8SHP-5nGjYEE2FE6xw If you are part of a member group, are recording talks, and would like the supergroup to host them, then let us know! We'd be happy to help. Yay for logic! -- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMTR990wBVVH_JaNFcivat2vDZjnkyOne%2BXdY%3DwVF2Vd3hs2vg%40mail.gmail.com.
