Extension by definitions (original) (raw)
In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol for the set which has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant and the new axiom , meaning "for all x, x is not a member of ". It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition. More precisely, the new theory is a conservative extension of the old one.
| Property | Value |
|---|---|
| dbo:abstract | In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol for the set which has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant and the new axiom , meaning "for all x, x is not a member of ". It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition. More precisely, the new theory is a conservative extension of the old one. (en) |
| dbo:wikiPageID | 12219849 (xsd:integer) |
| dbo:wikiPageLength | 8157 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1119507864 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Power_set dbc:Proof_theory dbr:Mathematical_logic dbr:Conservative_extension dbr:First-order_logic dbr:First-order_theory dbr:Free_variable dbr:Well-formed_formula dbr:Proof_theory dbr:Group_(mathematics) dbc:Mathematical_logic dbr:Axiom dbr:Set_(mathematics) dbr:Set_theory dbr:Bound_variable dbr:Extension_by_new_constant_and_function_names dbr:Zermelo–Fraenkel_axioms dbr:Logical_axiom |
| dbp:wikiPageUsesTemplate | dbt:Mathematical_logic |
| dct:subject | dbc:Proof_theory dbc:Mathematical_logic |
| rdfs:comment | In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol for the set which has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant and the new axiom , meaning "for all x, x is not a member of ". It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition. More precisely, the new theory is a conservative extension of the old one. (en) |
| rdfs:label | Extension by definitions (en) |
| owl:sameAs | freebase:Extension by definitions wikidata:Extension by definitions https://global.dbpedia.org/id/4jywH |
| prov:wasDerivedFrom | wikipedia-en:Extension_by_definitions?oldid=1119507864&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Extension_by_definitions |
| is dbo:wikiPageDisambiguates of | dbr:Extension |
| is dbo:wikiPageRedirects of | dbr:Definitional_extension dbr:Extension_by_definition |
| is dbo:wikiPageWikiLink of | dbr:Extension dbr:Definable_set dbr:Conservative_extension dbr:Constructive_set_theory dbr:First-order_logic dbr:Extension_by_new_constant_and_function_names dbr:Definitional_extension dbr:Extension_by_definition |
| is foaf:primaryTopic of | wikipedia-en:Extension_by_definitions |