Epsilon calculus (original) (raw)
Operátor výběru je v logice operátor nad formulemi zavedený Davidem Hilbertem vracející term, pro který formule platí. V logice prvního řádu například platí . Formalismus podporující operátor výběru se nazývá ε-kalkulus. Operátor výběru lze použít k eliminaci kvantifikátorů, neboť platía.Term ve druhé ekvivalenci reprezentuje imaginární prvek, pro který formule platí, platí-li pro celé universum. V tomto smyslu je ekvivalentní Henkinovým svědkům pro univerzální kvantifikaci:
| Property | Value |
|---|---|
| dbo:abstract | Operátor výběru je v logice operátor nad formulemi zavedený Davidem Hilbertem vracející term, pro který formule platí. V logice prvního řádu například platí . Formalismus podporující operátor výběru se nazývá ε-kalkulus. Operátor výběru lze použít k eliminaci kvantifikátorů, neboť platía.Term ve druhé ekvivalenci reprezentuje imaginární prvek, pro který formule platí, platí-li pro celé universum. V tomto smyslu je ekvivalentní Henkinovým svědkům pro univerzální kvantifikaci: (cs) Hilbert's epsilon calculus is an extension of a formal language by the epsilon operator, where the epsilon operator substitutes for quantifiers in that language as a method leading to a proof of consistency for the extended formal language. The epsilon operator and epsilon substitution method are typically applied to a first-order predicate calculus, followed by a showing of consistency. The epsilon-extended calculus is further extended and generalized to cover those mathematical objects, classes, and categories for which there is a desire to show consistency, building on previously-shown consistency at earlier levels. (en) L'Epsilon de Hilbert est une extension d'un langage formel par l'opérateur epsilon, où celui-ci se substitue aux quantificateurs dans le langage en tant que méthode conduisant à une preuve de la cohérence pour l'extension du langage formel. L'opérateur epsilon et la méthode de substitution epsilon sont généralement appliqués à un calcul de prédicats, suivis par une démonstration de la cohérence. Le calcul des prédicats étendu par l'opérateur epsilon est ensuite étendu et généralisé pour couvrir les objets mathématiques, les classes et les catégories pour lesquelles on veut montrer la cohérence, en s'appuyant sur la cohérence déjà montrée à des niveaux antérieurs. (fr) |
| dbo:wikiPageID | 11027904 (xsd:integer) |
| dbo:wikiPageLength | 4871 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1122391089 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:David_Hilbert dbr:Quantification_(logic) dbc:Proof_theory dbr:Ordered_pair dbr:Axiom_of_Choice dbc:Systems_of_formal_logic dbr:First-order_logic dbr:Nicolas_Bourbaki dbr:Cardinal_assignment dbr:Formal_language dbr:Formal_system dbr:Hilbert's_program dbr:Modus_ponens dbr:Axiom_of_replacement dbr:Consistency_proof |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Reflist dbt:Cite_SEP dbt:Cite_IEP |
| dct:subject | dbc:Proof_theory dbc:Systems_of_formal_logic |
| gold:hypernym | dbr:Extension |
| rdf:type | dbo:Software yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:Logic105664069 yago:Method105660268 yago:PsychologicalFeature100023100 yago:System105661996 yago:WikicatSystemsOfFormalLogic |
| rdfs:comment | Operátor výběru je v logice operátor nad formulemi zavedený Davidem Hilbertem vracející term, pro který formule platí. V logice prvního řádu například platí . Formalismus podporující operátor výběru se nazývá ε-kalkulus. Operátor výběru lze použít k eliminaci kvantifikátorů, neboť platía.Term ve druhé ekvivalenci reprezentuje imaginární prvek, pro který formule platí, platí-li pro celé universum. V tomto smyslu je ekvivalentní Henkinovým svědkům pro univerzální kvantifikaci: (cs) Hilbert's epsilon calculus is an extension of a formal language by the epsilon operator, where the epsilon operator substitutes for quantifiers in that language as a method leading to a proof of consistency for the extended formal language. The epsilon operator and epsilon substitution method are typically applied to a first-order predicate calculus, followed by a showing of consistency. The epsilon-extended calculus is further extended and generalized to cover those mathematical objects, classes, and categories for which there is a desire to show consistency, building on previously-shown consistency at earlier levels. (en) L'Epsilon de Hilbert est une extension d'un langage formel par l'opérateur epsilon, où celui-ci se substitue aux quantificateurs dans le langage en tant que méthode conduisant à une preuve de la cohérence pour l'extension du langage formel. L'opérateur epsilon et la méthode de substitution epsilon sont généralement appliqués à un calcul de prédicats, suivis par une démonstration de la cohérence. Le calcul des prédicats étendu par l'opérateur epsilon est ensuite étendu et généralisé pour couvrir les objets mathématiques, les classes et les catégories pour lesquelles on veut montrer la cohérence, en s'appuyant sur la cohérence déjà montrée à des niveaux antérieurs. (fr) |
| rdfs:label | Operátor výběru (cs) Epsilon calculus (en) Epsilon de Hilbert (fr) |
| owl:sameAs | freebase:Epsilon calculus yago-res:Epsilon calculus wikidata:Epsilon calculus dbpedia-cs:Epsilon calculus dbpedia-fr:Epsilon calculus https://global.dbpedia.org/id/4jx8b |
| prov:wasDerivedFrom | wikipedia-en:Epsilon_calculus?oldid=1122391089&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Epsilon_calculus |
| is dbo:knownFor of | dbr:David_Hilbert |
| is dbo:wikiPageDisambiguates of | dbr:Calculus_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Epsilon_operator dbr:Epsilon_substitution_method dbr:Epsilon_terms |
| is dbo:wikiPageWikiLink of | dbr:David_Hilbert dbr:Richard_Zach dbr:Dynamic_syntax dbr:Index_of_philosophy_articles_(D–H) dbr:Epsilon dbr:Choice_function dbr:Epsilon_operator dbr:Gödel's_incompleteness_theorems dbr:TLA+ dbr:Calculus_(disambiguation) dbr:List_of_things_named_after_David_Hilbert dbr:Hilbert_operator dbr:Epsilon_substitution_method dbr:Epsilon_terms |
| is dbp:knownFor of | dbr:David_Hilbert |
| is foaf:primaryTopic of | wikipedia-en:Epsilon_calculus |