In mathematics, 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 Prawitz (Prawitz 1968) and Takahashi (Takahashi 1967) by a similar technique (Takahashi 1967) - although Prawitz's and Takahashi's proofs are not limited to second-order logic, but concern higher-order logics in general;
* It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Congettura di Takeuti (it)
- Takeuti's conjecture (en)
- Гипотеза Такеути (ru)
|
| rdfs:comment
| - In mathematics, 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 Prawitz (Prawitz 1968) and Takahashi (Takahashi 1967) by a similar technique (Takahashi 1967) - although Prawitz's and Takahashi's proofs are not limited to second-order logic, but concern higher-order logics in general;
* It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F. (en)
- In logica matematica, la congettura di Takeuti è una congettura introdotta dal matematico giapponese . Essa afferma che ogni formalizzazione della nel calcolo dei sequenti gode dell'eliminazione del taglio. Un'estensione naturale di tale congettura richiede che l'eliminazione del taglio valga per ogni formalizzazione nel calcolo dei sequenti di ogni . La congettura di Takeuti è equivalente alla consistenza dell', nonché alla normalizzazione forte del sistema F. (it)
- Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной (яп. 竹内外史; 1926—2017) в 1953 году. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам , непротиворечивости и полноты для широкого класса логик высших порядков, по аналогии с результатом Генцена 1934 года для классического и интуиционистского исчислений предикатов первого порядка. (ru)
|
| dct:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - In mathematics, 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 Prawitz (Prawitz 1968) and Takahashi (Takahashi 1967) by a similar technique (Takahashi 1967) - although Prawitz's and Takahashi's proofs are not limited to second-order logic, but concern higher-order logics in general;
* It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F. Takeuti's conjecture is equivalent to the 1-consistency of second-order arithmetic in the sense that each of the statements can be derived from each other in the weak system PRA. It is also equivalent to the strong normalization of the Girard/Reynold's System F. (en)
- In logica matematica, la congettura di Takeuti è una congettura introdotta dal matematico giapponese . Essa afferma che ogni formalizzazione della nel calcolo dei sequenti gode dell'eliminazione del taglio. Un'estensione naturale di tale congettura richiede che l'eliminazione del taglio valga per ogni formalizzazione nel calcolo dei sequenti di ogni . Per la logica di secondo ordine, la congettura fu dimostrata da nel 1966, sulla base di precedenti lavori di Schütte. La versione generalizzata fu dimostrata indipendentemente da Prawitz nel 1968, e da Takahashi nel 1967. Tutte e tre le dimostrazioni sfruttano tecniche semantiche. Una dimostrazione sintattica fu invece offerta da , nel cui sistema F la congettura risulta essere un corollario del teorema di normalizzazione forte. La congettura di Takeuti è equivalente alla consistenza dell', nonché alla normalizzazione forte del sistema F. (it)
- Гипотеза Такеути — утверждение об устранимости сечений в исчислении секвенций для простой теории типов, построенной (яп. 竹内外史; 1926—2017) в 1953 году. Методологическая важность гипотезы состояла в том, что устранимость сечений для этого исчисления открывает путь к доказательствам , непротиворечивости и полноты для широкого класса логик высших порядков, по аналогии с результатом Генцена 1934 года для классического и интуиционистского исчислений предикатов первого порядка. Первым шагом к подтверждению гипотезы стало доказательство (англ. William W. Tait; род. 1929) устранимости сечений в логике второго порядка в 1966 году. В 1967 году результат был обобщён в работах и (швед. Dag Prawitz; род. 1936), тем самым, гипотеза полностью подтверждена. Позднее устранимость сечений обнаружена и для более широких классов исчислений, в частности, Драгалин установил устранимость сечений для серии неклассических логик высших порядков, а (фр. Jean-Yves Girard) — для системы F. (ru)
|
| gold:hypernym
| |
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)