| http://dbpedia.org/ontology/abstract
|
In sequent calculus, the completeness of a … In sequent calculus, the completeness of atomic initial sequents states that initial sequents A ⊢ A (where A is an arbitrary formula) can be derived from only atomic initial sequents p ⊢ p (where p is an atomic formula). This theorem plays a role analogous to eta expansion in lambda calculus, and dual to cut-elimination and beta reduction. Typically it can be established by induction on the structure of A, much more easily than cut-elimination. A, much more easily than cut-elimination.
|
| http://dbpedia.org/ontology/wikiPageID
|
23252771
|
| http://dbpedia.org/ontology/wikiPageLength
|
1031
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
789885599
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://dbpedia.org/resource/Atomic_formula +
, http://dbpedia.org/resource/Category:Theorems_in_the_foundations_of_mathematics +
, http://dbpedia.org/resource/Beta_reduction +
, http://dbpedia.org/resource/Gaisi_Takeuti +
, http://dbpedia.org/resource/Eta_expansion +
, http://dbpedia.org/resource/Helmut_Schwichtenberg +
, http://dbpedia.org/resource/Lambda_calculus +
, http://dbpedia.org/resource/Category:Proof_theory +
, http://dbpedia.org/resource/Cut-elimination +
, http://dbpedia.org/resource/Sequent_calculus +
, http://dbpedia.org/resource/Anne_Sjerp_Troelstra +
|
| http://dbpedia.org/property/wikiPageUsesTemplate
|
http://dbpedia.org/resource/Template:Math +
, http://dbpedia.org/resource/Template:Mathlogic-stub +
|
| http://purl.org/dc/terms/subject
|
http://dbpedia.org/resource/Category:Proof_theory +
, http://dbpedia.org/resource/Category:Theorems_in_the_foundations_of_mathematics +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents?oldid=789885599&ns=0 +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://en.wikipedia.org/wiki/Completeness_of_atomic_initial_sequents +
|
| owl:sameAs |
http://dbpedia.org/resource/Completeness_of_atomic_initial_sequents +
, http://www.wikidata.org/entity/Q5156542 +
, http://yago-knowledge.org/resource/Completeness_of_atomic_initial_sequents +
, http://rdf.freebase.com/ns/m.06619qh +
, https://global.dbpedia.org/id/4hbYr +
|
| rdf:type |
http://dbpedia.org/class/yago/Theorem106752293 +
, http://dbpedia.org/class/yago/Abstraction100002137 +
, http://dbpedia.org/class/yago/Statement106722453 +
, http://dbpedia.org/class/yago/Message106598915 +
, http://dbpedia.org/class/yago/Communication100033020 +
, http://dbpedia.org/class/yago/Proposition106750804 +
, http://dbpedia.org/class/yago/WikicatTheoremsInTheFoundationsOfMathematics +
|
| rdfs:comment |
In sequent calculus, the completeness of a … In sequent calculus, the completeness of atomic initial sequents states that initial sequents A ⊢ A (where A is an arbitrary formula) can be derived from only atomic initial sequents p ⊢ p (where p is an atomic formula). This theorem plays a role analogous to eta expansion in lambda calculus, and dual to cut-elimination and beta reduction. Typically it can be established by induction on the structure of A, much more easily than cut-elimination. A, much more easily than cut-elimination.
|
| rdfs:label |
Completeness of atomic initial sequents
|
