# 2011: KGRC Mini-Workshop

On Wednesday, April 27 2011, the KGRC will hosted an informal workshop on logic,
taking advantage of the presence of the many logicians who will be in Vienna
for the *New Trends in Logic* conference (April 28 and 29, honoring the
winners of the Kurt Gödel Research Prize Fellowships).

## Program

09:00 – 09:40 | Danko Ilik | Completeness proofs for classical, intuitionistic and one intermediate logic proving Double-negation Shift, based on forcing in Kripke-CPS models. abstract |

09:50 – 10:30 | Maryanthe Malliaris | Regularity and stable graphs |

10:50 – 11:30 | Matteo Viale | Supercompact properties of aleph_2 in models of PFA. abstract |

11:40 – 12:20 | Sean Walsh | Comparing Peano Arithmetic, Basic Law V, and Hume’s Principle. abstract |

Lunch (everyone invited) | ||

14:00 – 14:40 | Kentaro Fujimoto | Axiomatic truths for set theory and subsystems of MK |

14:50 – 15:30 | Giovanni Curi | Independence results in constructive set theory and constructive type theory |

15:50 – 16:30 | Andrey Bovykin | Unprovabilty: templates, indiscernibles and the space of all possibilities. |

16:40 – 17:20 | Federico Aschieri | Realizability, Epsilon Substitution Method and Type Theory. abstract |

17:30 – 18:10 | Sergei Artemov | First-Order Logic of Proofs. (Joint work with T. Yavorskaya.) abstract |

Workshop Dinner (everyone invited) |

## Abstracts

**Sergei Artemov***First-Order Logic of Proofs*(joint work with Tatiana Yavorskaya, Sidon)- The logic of proofs was anticipated by Goedel in the 1930s in connection with provability semantics for intuitionistic logic, which turned out to be rather elusive. The propositional logic of proofs LP, discovered in 1995, provided an explicit proof reading of modal logic S4 and, via Goedel's translation, a Brouwer-Heyting-Kolmogorov (BHK)-compliant semantics for the propositional intuitionistic logic IPC. In this work, we find the first-order logic of proofs FOLP capable of realizing first-order modal logic S4 and, therefore, the first-order intuitionistic logic HPC. We offer two kinds of proof semantics for FOLP: parametric semantics, in which proof objects are interpreted as derivations with parameters, and generic semantics with proof terms interpreted as provably computable functions from parameters to formal derivations. We show that both provide semantics of explicit proofs for first-order S4 and a first-order BHK-style semantics for HPC. FOLP may also be viewed as a general purpose first-order justification logic; it opens the door to a general theory of first-order justification.

**Federico Aschieri***Realizability, Epsilon Substitution Method and Type Theory*- We present a constructive "realizability" semantics for classical Arithmetic. We show how the computational content of classical proofs can be understood in terms of intelligent self-correcting programs, able to make predictions, test them and learn something from every failure. Connections with epsilon substitution method will be explained.

**Danko Ilik***Completeness proofs for classical, intuitionistic and one intermediate logic proving Double-negation Shift, based on forcing in Kripke-CPS models*- I will present a class of models, built from Kripke models and double-negation translation, that is constructively sound and complete for various predicate logics: intuitionistic, classical, and an intermediate one that can prove the Double-negation Shift schema. The composition of the soundness and completeness proofs gives a proof of normalization of thecorresponding logic. Being formalized in constructive type theory, in the Coq proof assistant, one can extract from the proofs explicit normalization algorithms that are purely model-based.

**Matteo Viale***Supercompact properties of aleph_2 in models of PFA*- The talk will expand on the paper submitted to APAL for the Gödel prize.

**Sean Walsh***Comparing Peano Arithmetic, Basic Law V, and Hume’s Principle*- This paper presents new constructions of models of Hume’s Principle and Basic Law V with restricted amounts of comprehension. The techniques used in these constructions are drawn from hyperarithmetic theory and the model theory of fields, and formalizing these techniques within various subsystems of second-order Peano arithmetic allows one to put upper and lower bounds on the interpretability strength of these theories and hence to compare these theories to the canonical subsystems of second-order arithmetic. The main results of this paper are: (i) there is a consistent extension of the hypearithmetic fragment of Basic Law V which interprets the hyperarithmetic fragment of second-order Peano arithmetic, and (ii) the hyperarithmetic fragment of Hume’s Principle does not interpret the hyperarithmetic fragment of second-order Peano arithmetic, so that in this specific sense there is no predicative version of Frege’s Theorem.