Seminar

Research Seminar of the Department of Logic

11/30/2020

Purity of formal mathematical proofs
Speaker: Robin Martinot (Universiteit Utrecht), Time: Monday November 30, 16:30, Prague time. Place: Zoom (contact Radek Honzik for details).

A phenomenon that has gained attention in the philosophy of proof theory is the property of purity of proof. Intuitively, a pure proof of a mathematical theorem only draws upon notions that belong to the content of the theorem. An impure proof, by contrast, contains notions that are topically unrelated to the theorem. This classification of proofs is connected to other properties of proofs such as simplicity, efficiency and equivalence, and therefore also to Hilbert’s 24th problem. A reliable formal measure of purity would provide insight into what constitutes the gap between two proofs of the same theorem. I will discuss several strategies from the literature for devising such a measure, the most com- mon of which makes use of cut elimination. Most current strategies still have considerable weaknesses, including limited applicability to stronger mathematical theories. I will touch upon some strategies that I am currently exploring to help overcome these vulnerabilities.

11/23/2020

The Limits of Causal Graphs: Density

Speaker: Dean McHugh (University of Amsterdam), Time: Monday November 23, 16:30, Prague time. Place: Zoom (contact Radek Honzik for details).

Causal reasoning is often modelled using causal graphs, such as Bayesian networks and structural causal models (e.g. Pearl 2000, Causality). Given the success of graphical models of causation, one may ask whether they can represent every instance of causal reasoning, or whether a more expressive framework is required. In this talk we show that graphical causal models are limited in their expressive power: some intuitive causal structures are impossible to represent using graphical causal models. Specifically, graphical causal models cannot represent dense causal chains; that is, chains of events where between any two events C and E on the chain there is a third event D on the chain such that C causally influences D and D causally influences E. Dense causal chains appear, arguably, in both our intuitive representation of the world and models in physics that assume spacetime is dense. Since any framework representing causal reasoning should be compatible with these models, a more expressive framework is required—one that can represent dense causal chains.

11/16/2020

P-ultrafilters in Silver extensions
David Chodounsky (Institute of Mathematics, AVCR) will talk about P-ultrafilters in Silver extensions. Time: 16.11.2020, 16:30 Prague time. Write to Radek Honzik to get the Zoom link.

P-ultrafilters are an important and widely used class of ultrafilters on natural numbers. Their existence is however not provable in ZFC. The first model without P-ultrafilters was constructed by Shelah in 1977.  For a long time the method of Shelah was essentially the only known way to get models without P-ultrafilters and many related questions remained 
opened. Many of these questions were settled in our joint paper with O.  Guzman, we proved that there are in fact no P-ultrafilters in the Silver model (and it realtives). I will give a quick overview of this result.

11/09/2020

Incomparable consistency degrees and large-cardinal axioms
Speaker: Radek Honzik (Department of Logic, FFUK) Title: Incomparable consistency degrees and large-cardinal axioms. Time: Monday 9.11.2020; 16:30 Prague time. Please write to Radek Honzik to get the Zoom link.

We will review the folklore fact that if T is a theory allowing the usual Goedel-like analysis (such as PA or ZFC), then there are infinitely many incomparable consistency degrees, i.e. there are infinitely many statements A, B such that T + Con(T +A) does not imply Con(T+B), or conversely.

On the other hand, it is known that virtually all "interesting" independent statements over ZFC have comparable consistency degrees. This is because they are reducible to large-cardinal axioms which are linearly ordered in the consistency ordering. We use this fact to argue that large-cardinal axioms (and statements equivalent to them in the consistency ordering) are natural mathematical propositions which are not affected by self-referential constructions.

10/26/2020

Decision theory and Bayesian agents

Daniel Herrmann, University of California Irvine, will talk about decision theory and Bayesian agents. The talk will take place over Zoom on Monday 16:30, October 26, Prague time (GMT+2), using the stable Zoom link. If you don't know the Zoom link, write to Radek Honzik.

Decision theory attempts to provide an account of rational decision making. To this end decision theorists often reason about idealized Bayesian agents. Sharpening and generalizing some remarks by Brian Skyrms and Richard Jeffrey, I argue that for Bayesian agents with a sufficiently rich algebra there can be no decision problems. This is a problem for decision theory, as most of the debate concerns these kinds of agents. I propose a solution to this problem, but one which comes with a cost: in order for an agent to view herself as in a legitimate decision problem she cannot be ideally Bayesian. I argue that my solution both fits well with certain approaches to decision theory, especially deliberational dynamics, and helps clarify the goals of decision theory.

10/19/2020

Elementary embeddings in set theory

Radek Honzik, department of Logic, will talk about Elementary embeddings in set theory. Monday October 19, 16:30, over Zoom.

Abstract: We will review some applications of elementary embeddings between transitive models of set theory. In particular, we will discuss the method of lifting an embedding to a generic extension which is often used to show that some desirable large-cardinal properties are preserved under forcing. Time: Monday October 19, 16:30 (Prague time, GMT+2) The talk will take place over Zoom (write to Radek Honzik to get the link).

03/16/2020

On enhanced generalization (Cancelled!)

Vitezslav Svejdar (Department of Logic) will talk about enhanced generalization (Monday 16.3).

The generalization rule in logical calculi makes it possible to 
"unsubstitute" a variable $y$ from a formula $\varphi_x(y)$ and conclude 
that $\forall x \varphi$ (or that $\exists x \varphi$ if the step 
is happening in a premise), provided that there are no unwanted free 
occurrences of the unsubstituted variable. We consider an enhanced 
generalization rule that makes it possible to simultaneously 
unsubstitute not only several variables, but also several terms 
(provided that they are pairwise different and there are no unwanted 
occurrences of their outermost symbols). While we cannot claim that this 
enhanced generalization models a step in a reasoning, and it is not 
sound in logic with equality, we show that it is sound in logic without 
equality and that it has a useful application, namely the interpolation 
theorem (for logic without equality but with function symbols).

02/24/2020

Believing the Axioms I
Tereza Stejskalová (logika, FFUK) bude mluvit axiomech ZFC a jejich historii a motivaci. Přednáška je založena na článku P. Maddy Believing the Axioms I (JSL 1988).

02/17/2020

Believing the Axioms II

Radek Honzik will discuss P. Maddy's paper Believing the Axioms II (JSL 1988).

Believing the Axioms II is a continuation of the first paper by Maddy and deals with the Axiom of Determinacy (AD). The paper attempts to argue that AD (or its variants) may be a good candidate for a new strong axiom of set theory. The seminar will review the basic points of the paper (prior knowledge of the paper is not necessary).

12/16/2019

Casual inferences in statistics

Lars S. Laichter (Department of logic) will introduce basic concepts of casual inferences in statistics. CHANGE OF DATE:  16.12.,  16:30.

In my presentation, I will provide a brief introduction and a discussion of the methods of causal inference in statistics. Methods of causal inference have been argued to be an important addition to traditional statistical methods. In particular, I will introduce the notion of the Structural Causal Model (SCM), as proposed by Judeau Pearl, to illustrate some of the major advancements in the general theory of causation. These advancements include methods for inferring a model’s properties based on (1) effects of interventions, (2) probabilities of counterfactuals, and (3) direct and indirect effects. Finally, I will discuss some of the possible applications of this theory, as well as its wider implications for scientific inquiry. Overall, I aim for this presentation to provide an accessible introduction to the methods of causal inference and highlight the advantages of the methods of causal inference over traditional statistical methods.

12/02/2019

Who's who in large cardinals, II

Radek Honzik (Department of logic) will continue talking about large cardinals. Monday 2.12., 16:30. We will discuss "larger" large cardinals, such as measurable and supercompact cardinals, and their effect on the set-theoretical universe and applications in mathematics and set theory.

11/25/2019

THE IMPOSSIBILITY OF SQUARING THE CIRCLE Gregory, Huygens and the limits of Cartesian geometry
Davide Crippa (Institute of Philosophy, AVČR) will talk about the impossibility of squaring the circle. Monday 25. November, 16:30, Department of Logic.

With the emergence of the algebraic movement in XVIth and XVIIth century geometry, the ideal that all mathematical problems should and could be solved by the most adequate means was fostered by outstanding mathematicians (Viète, Descartes). Yet it was a matter of dispute whether certain well-known problems, like the quadrature of the circle, could be solved by geometrically acceptable methods. My talk will explore this issue, considering a controversy occurred in 1668 between the Scottish mathematician James Gregory and the Dutch mathematician Christiaan Huygens, about the possibility of solving the quadrature of central conics (which included the circle) by algebraic means. Whereas the former held it was impossible, the latter believed that the circle could be squared algebraically. This controversy is significant because it hinged upon methodological or foundational questions: which were the bounds of Cartesian geometry? Are the five algebraic operations sufficient in order to express and solve all problems concerning the objects of Euclid's geometry?

11/18/2019

Who's who in large cardinals, I
Radek Honzik (Department of logic) will talk about motivations, history and applications behind large cardinals. 16:30, Monday 18.11.2019.

11/11/2019

Aspekty eliminovatelnosti řezu v různých logikách

Vítězslav Švejdar (Department of Logic, FFUK) bude mluvit o různých neklasických logikách a jejich vztahu k eleminovatelnosti řezu. 11. listopadu, 16:30.

11/04/2019

Finitní verze Gödelových vět o neúplnosti

Martina Maxa bude mluvit o finitních verzích Gödelových vět o neúplnosti a Löbově větě. Monday November 4, 16:30.

Budeme se zabývat finitními protějšky známých vět dotýkajících se základů matematiky, jako jsou Gödelovy věty o neúplnosti či Löbova věta. Jejich finitní verze jsou již silnější než známé otevřené problémy ve výpočetní složitosti jako např. domněnka P se nerovná NP. Kromě finitní verze druhé Gödelovy věty, představíme i finitní verzy první Gödelovy věty a ukážeme vztah mezi těmito domněnkami. Také uvedeme tvrzení, jež by se dalo nazvat finitní verzí Löbovy věty. Cílem je ukázat, že otevřené problémy ve výpočetní složitosti mají blízký vztah k problémům týkajících se logiky a tímto i základů matematiky.


10/21/2019

Most common proposals for solving the CH problem

Radek Honzik will survey old and recent attempts and proposals for solving the Continuum Hypothesis problem. Monday  October 21, 16:30.  Students interested in credits from the seminar should attend and discuss their participation in the seminar.

Students interested in credits from the seminar should attend and discuss their participation in the seminar.

04/29/2019

Složitost Booleovských formulí

Seminář katedry: Vít Fojtík, Department of Logic, FF UK, 17:00, 29.4.2019.

Booleovské formule jsou typ Booleovských obvodů modelující výpočty, při kterých si nelze pamatovat mezivýsledky. Přestože lze ukázat, že existují funkce s exponenciální formulovou složitostí (a dokonce jich je většina), jedním z nevyřešených problémů výpočetní složitosti je najít ,,větší než polynomiální" dolní odhad pro nějakou konkrétní funkci. Snahy o sestrojení odhadu se ubírají dvěma převažujícími směry; první ja založený na abstraktním pojmu míry složitosti, zatímco druhý používá náhodně zvolené podfunkce dané funkce.

03/04/2019

Indestructibility of Kurepa Hypothesis

Šárka Stejskalová, Department of Logic, FF UK

We will review an argument of Jensen and Schlechta form 1990 who showed that Kurepa Hypothesis can be indestructible under all ccc forcing notions. Possible generalizations will be discussed.

02/25/2019

Abstract notion of liftability for supercompact cardinals

Radek Honzík, Department of Logic, FF UK

We will discuss generalizations of the property of kappa-directed closure which appears in the classical theorem of Levy on indestructible supercompact cardinals. Seminar takes place in C119 at 17:00.

05/14/2018

Is there a difference in gaps between convergence and divergence in ZFC and PA?

Peter Vojtáš, Department of Software Engineering, MFF UK


12/18/2017

(Homotopy) Type theory II.
Tomáš Lávička, Department of Logic, FF UK

Type theory is a possible alternative to set theory and first order predicate logic as a tool for mathematical foundations, which has recently been getting more and more attention especially due to the discovery of its close relation to algebraic topology. I will try to give an introductory  lecture to the basic concepts of type theory  and its formalism (not requiring any previous knowledge in the field) in such a way that we could get some idea on how one can do (not only constructive) mathematics with its framework. Along the way I will be suggesting where is the famous connection with algebraic topology coming from.  

Keywords: Types, identity types, dependent types, Univalence, constructive mathematics.

12/11/2017

(Homotopy) Type theory

Tomáš Lávička, Department of Logic, FF UK

Type theory is a possible alternative to set theory and first order predicate logic as a tool for mathematical foundations, which has recently been getting more and more attention especially due to the discovery of its close relation to algebraic topology. I will try to give an introductory  lecture to the basic concepts of type theory  and its formalism (not requiring any previous knowledge in the field) in such a way that we could get some idea on how one can do (not only constructive) mathematics with its framework. Along the way I will be suggesting where is the famous connection with algebraic topology coming from.  

Keywords: Types, identity types, dependent types, Univalence, constructive mathematics. 

11/27/2017

Definability of stationary subsets of $\omega_1$

Stefan Hoffelner, Department of Logic, FF UK


​​​​​​​

11/20/2017

Prediction principles in set theory: It's OK to guess

Miha Habić, Department of Logic, FF UK

Diagonalization arguments play a central role in logic and specifically set theory, reaching from Cantor's proof of the uncountability of the reals to complicated forcing arguments. Guessing principles provide a substitute in cases where there are too many objects to diagonalize against in a naive way. They work by providing small approximations to the objects and guaranteeing that the approximations are correct "often enough". In the talk I shall give a short introduction to some simple guessing principles, after which I shall examine joint guessing principles, which allow us to guess many objects at once.  

10/16/2017

The rearrangement number

William Brian, University of North Carolina at Charlotte, USA

Recall the classical result of Riemann that every conditionally convergent series can be rearranged to get a series which is divergent to infinity, oscillates or converges to an arbitrary real number. A natural question to ask is how many rearrangements are needed to witness the validity of this theorem. This leads to the definition of the rearrangement number which is a cardinal invariant of the continuum. We present recent results related to this number. The talk is based on the preprint by several authors including the speaker. 

12/19/2016

Nestandardní metody v konstrukci modelů slabých aritmetik
Jana Glivická

Představím novou metodu konstrukce modelů slabých aritmetik. Použijeme nestandardních metod ke konstrukci jisté elementární extenze standardního modelu aritmetiky, která je uzavřena na operaci *. Tento fakt nám umožní definovat na univerzu této extenze tzv. gradované verze aritmetických operací sčítání a násobení. Ukážeme, jak volbou různých gradací můžeme ovlivňovat platnost některých aritmetických tvrzení ve vzniklých strukturách. Speciálně předvedeme, jak lze touto metodou získat model Robinsonovy aritmetiky, v němž platí hypotéza prvočíselných dvojčat.

12/12/2016

Birkhoff's subdirect representation from a broader perspective

Tomáš Lávička

It is well known that varieties (resp.. quasi-varieties) are generated by its (relatively) subdirectly irreducible members (Birkhoff's representation). As we will see this representation theorem will not hold in general in the setting of generalized quasi-varieties (classes of algebras described by quasi-equations with countably many premises). I will present some characterization results of Birhoff's representability, which I then use to prove that the proper generalized quasi-variety generated by the [0,1] Lukasiewicz chain is representable in the above sense - the core idea of the proof uses a modification of the well-known topological proof of compactness for classical logic into higher cardinalities.

12/05/2016

Gentzen's cut elimination strategy and Tait's cut elimination strategy in propositional sequent calculus
Anna Horská

Nowadays, we usually eliminate cuts by decreasing the cut-rank of the derivation (Tait's strategy). That is, a cut with the greatest complexity is chosen such that there are only smaller cuts above it and this one is then decomposed into smaller cuts. Gentzen applies another strategy in his article of 1935. He eliminates the highest cuts, i.e., cuts that there are no other cuts above them. Hence, this procedure does not pay attention to the complexity of the chosen cut. The main property of cut elimination that we are interested in is the growth of the height of the derivation during the elimination, especially we want to know the height of the cut-free derivation. I want to show that both strategies mentioned above give us the same cut-free derivation in propositional logic. Not only is the height of the cut-free derivations the same, but they also have the same structure. I will define a procedure for eliminating a single cut (according to Buss) which makes global changes to the derivation. Then, I use Church-Rosser property to obtain that cut-free derivations are the same, when the only difference during the elimination is the way we choose the next cut to eliminate.

11/28/2016

Interpolants in the context of software verification
Martin Blicha

In the first part we present the role of interpolants in some verification algorithms to demonstrate the usefulness of the concept and the motivation for our work. In the second part we examine interpolation systems for propositional logic (the algorithms for computation of interpolants from a refutation proof), namely symmetric system (Pudlák, Krajíček), McMillan's system, and their generalization, framework of Labeled Interpolation Systems (D'Silva et al.). We conclude with incorporating partial variable assignment into the computation of interpolant, done in the framework of Labeled Partial Assignment Interpolation Systems (Jančík et al.).

10/31/2016

Nestovaný sekventový kalkulus pro intuicionistickou logiku
Eva Kolovratníková

Nejprve představíme nestovaný kalkulus pro intuicionistickou logiku a vysvětlíme, jak funguje nestování. Pak přidáme pravidla pro kvantifikátory a získáme kalkulus pro intuicionistickou predikátovou logiku s konstantním univerzem. Následně přidáme omezení, abychom získali kalkulus pro standardní intuicionistickou predikátovou logiku. Na závěr si předvedeme prefixová tabla pro obě varianty intuicionistické logiky a ukážeme, jak transformovat tabla do nestovaných sequentů. (English version of abstract) Firstly, we introduce nested sequent calculus for intuitionistic logics and show how the nesting works. Secondly, we show that standard quantification rules lead to calculus for intuitionistic predicate logic with constant domains. Then we add some restrictions to obtain calculus for standard Intuitionistic predicate logic. Finally, we introduce prefixed tableaux for both variants of Intuitionistic logic and show how we can transform tableaux to nested sequents.

10/10/2016

Vopěnkův princip a Vopěnkovy kardinály
Radek Honzík
Vopěnkův princip formuloval Petr Vopěnka a zní takto: Je-li A vlastní třída struktur v daném (množinovém) jazyce, pak existují dvě struktury M a N v A, že M je elementárně vnořitelná do N. Petr Vopěnka navrhl tento princip spíše s představou, že se brzy ukáže jako sporný, nicméně se tak nestalo. Ukážeme, že konzistentní síla tohoto tvrzení je velmi velká; v hierarchii velkých kardinálů se tento princip nachází mezi nejsilnějšími kardinály (např. implikuje konzistenci superkompatních kardinálů). Pozn. Podle obecenstva bude přednáška buď v češtině nebo angličtině.

04/25/2016

Fermat's last theorem and Catalan's conjecture in arithmetics with weak exponentiation
Petr Glivický

Wiles's proof of Fermat's Last Theorem (FLT) has stimulated a lively discussion on how much is actually needed for the proof. Despite the fact that the original proof uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC) - namely, the existence of Grothendieck universes - it is widely believed that "certainly much less than ZFC is used in principle, probably nothing beyond Peano arithmetic, and perhaps much less than that." (McLarty) In this talk, I will present a joint work with V. Kala. We studied (un)provabiliy of FLT and Catalan's conjecture in arithmetical theories with weak exponentiation, i.e. in theories in the language  $L=(0,1,+,\cdot,exp,<)$ where the $(0,1,+,\cdot,<)$-fragment is usually very strong (often even the complete theory $\mbox{Th}(\mathbb N)$ of natural numbers in that language) but the exponentiation satisfies only basic arithmetical properties and not much of induction. In such theories, Diophantine problems such as FLT or Catalan's conjecture, are formalized using the exponentiation exp instead of the exponentiation definable in the $(0,1,+,\cdot,<)$-fragment. I will present a natural basic set of axioms Exp for exponentiation (consisting mostly of elementary identities) and show that the theory $T=\mbox{Th}(\mathbb N)+Exp$ is strong enough to prove Catalan's conjecture, while FLT is still unprovable in $T$. This gives an interesting separation of strengths of the two famous Diophantine problems. Nevertheless, I show that by adding just one more axiom for exponentiation (the, so called, "coprimality" of exp) the theory becomes strong enough to prove FLT, i.e. FLT is provable in T+"coprimality". (Of course, in the proof of this, we use the Wiles's result too.)