About: Completeness of atomic initial sequents

An Entity of Type: Abstraction100002137, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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.

Property	Value
dbo:abstract	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. (en)
dbo:wikiPageID	23252771 (xsd:integer)
dbo:wikiPageLength	1031 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID	789885599 (xsd:integer)
dbo:wikiPageWikiLink	dbr:Beta_reduction dbc:Proof_theory dbr:Gaisi_Takeuti dbr:Anne_Sjerp_Troelstra dbr:Eta_expansion dbc:Theorems_in_the_foundations_of_mathematics dbr:Helmut_Schwichtenberg dbr:Atomic_formula dbr:Lambda_calculus dbr:Sequent_calculus dbr:Cut-elimination
dbp:wikiPageUsesTemplate	dbt:Math dbt:Mathlogic-stub
dcterms:subject	dbc:Proof_theory dbc:Theorems_in_the_foundations_of_mathematics
rdf:type	yago:WikicatTheoremsInTheFoundationsOfMathematics yago:Abstraction100002137 yago:Communication100033020 yago:Message106598915 yago:Proposition106750804 yago:Statement106722453 yago:Theorem106752293
rdfs:comment	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. (en)
rdfs:label	Completeness of atomic initial sequents (en)
owl:sameAs	freebase:Completeness of atomic initial sequents yago-res:Completeness of atomic initial sequents wikidata:Completeness of atomic initial sequents https://global.dbpedia.org/id/4hbYr
prov:wasDerivedFrom	wikipedia-en:Completeness_of_atomic_initial_sequents?oldid=789885599&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Completeness_of_atomic_initial_sequents
is dbo:wikiPageWikiLink of	dbr:Linear_logic dbr:Sequent_calculus
is foaf:primaryTopic of	wikipedia-en:Completeness_of_atomic_initial_sequents