Takeuti's conjecture is the conjecture of Gaisi Takeuti that a sequent formalisation of second-order logic has cut-elimination (Takeuti 1953). It was settled positively: By Tait, using a semantic technique for proving cut-elimination, based on work by Schütte (Tait 1966); Independently by Takahashi by a similar technique (Takahashi 1967); It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F.

PropertyValue
dbpprop:abstract
  • Takeuti's conjecture is the conjecture of Gaisi Takeuti that a sequent formalisation of second-order logic has cut-elimination (Takeuti 1953). It was settled positively: By Tait, using a semantic technique for proving cut-elimination, based on work by Schütte (Tait 1966); Independently by Takahashi by a similar technique (Takahashi 1967); It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F. Takeuti's conjecture is equivalent to the consistency of second-order arithmetic and to the strong normalization of the Girard/Reynold's System F.
dbpprop:hasPhotoCollection
rdf:type
rdfs:comment
  • Takeuti's conjecture is the conjecture of Gaisi Takeuti that a sequent formalisation of second-order logic has cut-elimination (Takeuti 1953). It was settled positively: By Tait, using a semantic technique for proving cut-elimination, based on work by Schütte (Tait 1966); Independently by Takahashi by a similar technique (Takahashi 1967); It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F.
rdfs:label
  • Takeuti conjecture
owl:sameAs
skos:subject
foaf:page
is dbpprop:disambiguates of
is owl:sameAs of