Speaker
Mojtaba Mojtahedi
Ghent University
Talks at this conference:
Tuesday, 18:10, J336 
A translation from GLP into GL 
We provide a syntactical translation from polymodal provability logic \(GLP\) to the GödelLöb logic \(GL\). This translation has two parts: first we use a translation similar to the Beklemishev’s translation [1] from \(GLP\) to a subsytem \(J^\) of \(GLP\), in which the monotonicity axiom \([n] A\to[n+1] A\) is replaced by \([n] A\to [n+i] [n] A\). Then we define a translation which makes nested boxes ascending, i.e. if \([n]\) occurs inside some \([m]\), then \(n\geq m\). Finally we provide a simple Kripkestyle semantics for \(J^\) which enables us to reprove arithmetical completeness of \(GLP\). Bibliography
