CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Inductively generated formal topologies

Thierry Coquand ; G. Sambin ; Jan Smith (Institutionen för datavetenskap) ; S. Valentini
Annals of Pure and Applied Logic (0168-0072). Vol. 124 (2003), 1-3, p. 71–106.
[Artikel, refereegranskad vetenskaplig]

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined.

Nyckelord: inductive definitions, formal topology, predicative systems

Denna post skapades 2013-02-15. Senast ändrad 2014-04-14.
CPL Pubid: 173697


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU) (GU)
Institutionen för datavetenskap (2002-2004)


Data- och informationsvetenskap

Chalmers infrastruktur