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 <math>\emptyset</math> for the set which has no member.

PropertyValue
dbpprop: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 <math>\emptyset</math> 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 <math>\emptyset</math> and the new axiom <math>\forall x(x\notin\emptyset)</math>, meaning 'for all x, x is not a member of <math>\emptyset</math>'. 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.
dbpprop:hasPhotoCollection
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 <math>\emptyset</math> for the set which has no member.
rdfs:label
  • Extension by definitions
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of