This HTML5 document contains 21 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dcterms	http://purl.org/dc/terms/
dbo	http://dbpedia.org/ontology/
foaf	http://xmlns.com/foaf/0.1/
dbt	http://dbpedia.org/resource/Template:
rdfs	http://www.w3.org/2000/01/rdf-schema#
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
wikipedia-en	http://en.wikipedia.org/wiki/
prov	http://www.w3.org/ns/prov#
dbc	http://dbpedia.org/resource/Category:
dbp	http://dbpedia.org/property/
xsdh	http://www.w3.org/2001/XMLSchema#
dbr	http://dbpedia.org/resource/

Statements

Subject Item

dbr:Intuitionistic_type_theory

dbo:wikiPageWikiLink

dbr:Empty_type

Subject Item

dbr:Bottom_type

dbo:wikiPageWikiLink

dbr:Empty_type

Subject Item

dbr:Empty_type

rdfs:label

Empty type

rdfs:comment

In type theory, the empty type or absurd type, typically denoted is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type For any type , the type is defined as . As the notation suggests, by the Curry–Howard correspondence, a term of type is a false proposition, and a term of type is a disproof of proposition P. A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, is also uninhabited for any inhabited type .

dcterms:subject

dbc:Type_theory

dbo:wikiPageID

24027503

dbo:wikiPageRevisionID

1118460201

dbo:wikiPageWikiLink

dbc:Type_theory dbr:Type_theory dbr:Bottom_type dbr:Type_inhabitation dbr:Curry–Howard_correspondence

dbp:wikiPageUsesTemplate

dbt:Reflist dbt:Comp-sci-theory-stub

dbo:abstract

In type theory, the empty type or absurd type, typically denoted is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type For any type , the type is defined as . As the notation suggests, by the Curry–Howard correspondence, a term of type is a false proposition, and a term of type is a disproof of proposition P. A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, is also uninhabited for any inhabited type . If a type system contains an empty type, the bottom type must be uninhabited too, so no distinction is drawn between them and both are denoted .

prov:wasDerivedFrom

wikipedia-en:Empty_type?oldid=1118460201&ns=0

dbo:wikiPageLength

1577

foaf:isPrimaryTopicOf

wikipedia-en:Empty_type

Subject Item

dbr:Up_tack

dbo:wikiPageWikiLink

dbr:Empty_type

Subject Item

dbr:Type_theory

dbo:wikiPageWikiLink

dbr:Empty_type

Subject Item

wikipedia-en:Empty_type

foaf:primaryTopic

dbr:Empty_type