A rule \phi_1, ..., \phi_k / \psi is admissible in a (nonclassical) propositional logic L if the set of L-tautologies is closed under substitution instances of the rule. We are particularly interested in the set-up with parameters (constants), which are required to be preserved by substitutions. In this talk, we shall study basic properties of admissibility with parameters in a class of well-behaved transitive modal logics (i.e., extensions of K4). The main goal is a classification of the computational complexity of admissibility (and the closely related problem of unifiability) with parameters based on semantic properties of logics.
Logic seminar
usually takes place each Monday at 16:00 in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.
Complexity of admissible rules with parameters
Emil Jeřábek
Institute of Mathematics
Monday, 27. May 2019 - 13:00 to 14:30
Propositional proofs and monotone computations
Pavel Pudlák
Mathematical Institute
Monday, 20. May 2019 - 13:00 to 14:30
One of the major discoveries of Stephen Cook is that lower bounds on the lengths of proofs in the propositional calculus can be used to prove independence results. This stimulated research into proving lower bounds for various propositional proof systems. Later it was shown that one can use lower bounds on the size of monotone circuits to prove lower bounds on propositional proofs. New models of monotone computations have been proposed recently that potentially may give us lower bounds for more propositional proof systems that we have so far. In this talk we will survey some results that connect lower bounds on monotone computations in various models with lower bounds on the lengths of proofs in proof systems.
Feasible incompleteness
Martin Maxa
Charles University
Monday, 13. May 2019 - 13:00 to 14:30
We will present finite counterparts to the well-known theorems that are connected to the foundations of mathematics such as Godel's incompleteness theorems or Lob's theorem. Their finite versions go already beyond famous open problems in computational theory, for example P != NP. Beside the finite version of Godel's second incompleteness theorem, we will present also the finite version of Godel's first incompleteness theorem and we will prove that they are equivalent. We will also state a conjecture that could be called a finite version of Lob's theorem.
Consistency of circuit lower bounds
Jan Bydžovský
Vienna Technical University
Monday, 29. April 2019 - 13:00 to 14:30
Let T be a strong enough universal theory in language L (containing the symbol '<') and let A(x) be a Sigma^b_2 L-formula. What are the sufficient and possibly useful conditions to derive that 1) T+"A(x) fails for some x" is consistent, 2) T+"A(x) fails for infinitely many x" is consistent, 3) T+"A(x) fails for all but finitely many x" is consistent? I will prove a theorem giving such conditions and use the conditions for 1) and 2) respectively to prove that two formalization of the statement
"for every natural number k, there is a polynomial-time computable Boolean-function which is not computable by circuits of size O(n^k)"... more