Seminars
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Calendar
Search
Add a seminar

RSS
Forthcoming seminars




Seminars "Proof Theory" and "Logic Online Seminar"
November 22, 2021 18:30, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + Zoom
 


Interpreters as consistoids

A. Visser

Utrecht University
Video records:
MP4 359.2 Mb

Number of views:
This page:206
Video files:35
Youtube:



Abstract: Harvey Friedman shows that, over Peano Arithmetic as base theory, the consistency statement for a finitely axiomatised theory can be characterised as the weakest statement that, in combination with the base interprets the given theory. Thus, we have a coordinate-free characterisation of these consistency statements modulo base-theory-provable equivalence.

Let us call a base theory that, in analogy to Peano Arithmetic, has such weakest extensions: Friedman-reflexive. We call such a weakest statement the interpreter of the finite theory. Interpreters are not always consistency statements, but they are still consistency-like or ‘consistoids’.

Which theories are Friedman-reflexive and what more can we say about their consistoids and the associated provability-like notion? We will sketch some preliminary insights. (E.g., all complete theories are Friedman-reflexive.)

A very weak theory, Peano Corto, is Friedman-reflexive. We do not get the usual consistency statements here, but bounded, cut-free or Herbrand consistency statements. We show that Peano Corto as a base theory has many additional desirable properties. In a sense, Peano Corto is, as far as current knowledge goes, the best choice for a base.

We discuss a characterisation of Friedman-reflexive sequential theories. Their interpreters generally are number-system-hopping bounded consistency statements. We have an example to show that some essential hopping may really happen.

The interpreter logic of a finitely axiomatised theory over a Friedman-reflexive sequential base contains at least Löb's logic. A fortiori, we do have an interpreter version of the second incompleteness theorem for the sequential case. (E.g., the interpreter analogue of G2 fails over finitely axiomatised, complete bases.)

Language: English
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024