Craig interpolation (original) (raw)
In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.
| Property | Value |
|---|---|
| dbo:abstract | In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem. (en) Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen: Es seien und zwei Theorien und der Satz sei ein in ableitbarer Satz. Dann gilt: Es gibt ein , sodass in ableitbar ist, und ist in ableitbar. (de) En logique mathématique, le théorème d'interpolation de Craig dit que si une formule φ en implique une deuxième ψ, et que φ et ψ partagent au moins un symbole non logique en commun, alors il existe une formule ρ, appelée interpolant, telle que : * φ implique ρ ; * ρ implique ψ ; * tout symbole non logique dans ρ apparaît à la fois dans φ et ψ. (fr) 크레이그의 보간 정리(Craig's interpolation theorem, -補間 定理)는 증명 이론의 정리로, 미국의 철학자이자 논리학자인 가 제시하였다. 간단히 말해 다음과 같이 쓸 수 있다. * 어떤 논리식 a에서 다른 논리식 b를 추론할 수 있다고 하자. 그러면, c에서 나타나는 모든 는 a와 b 각각에서도 나타나는 제3의 논리식 c가 존재하여 a에서 c를 추론할 수 있고, 다시 c에서 b를 추론할 수 있다. 이 c를 보간(interpolant)이라 한다. 크레이그는 1957년 이 정리를 일차 논리학에 대해 증명하였다. 미국 수학자 이 일차 논리학에 대한 이 정리의 보다 강한 판본을 1959년 증명하였으므로 이 둘을 합쳐 크레이그-린든 정리라 부르기도 한다. (ko) クレイグの補間定理（英: Craig's interpolation theorem）は論理学における定理であり、論理体系によってその定義が異なる。William Craig が1957年、一階述語論理について証明したのが最初である。クレイグの補題とも。 (ja) Twierdzenie Craiga – twierdzenie logiki, a w szczególności rachunku predykatów pierwszego rzędu. Udowodnione przez (ang.), amerykańskiego logika. (pl) |
| dbo:wikiPageID | 2056790 (xsd:integer) |
| dbo:wikiPageLength | 8193 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1059769235 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Cambridge_University_Press dbr:Modal_logic dbr:Model_theory dbr:Big_O_Notation dbr:Algorithm dbc:Lemmas dbr:Intuitionistic_logic dbr:Robinson's_joint_consistency_theorem dbr:Signature_(mathematical_logic) dbr:Mathematical_logic dbr:Clarendon_Press dbr:Model_checking dbr:Conjunctive_normal_form dbr:Constructive_proof dbr:Subformula_property dbr:Compactness_theorem dbr:Propositional_logic dbr:Specification_language dbr:Amalgamation_property dbr:First-order_logic dbr:Entailment dbr:Logical_connective dbr:Proof_theory dbr:Abstract_algebraic_logic dbc:Mathematical_logic dbr:Theory_(mathematical_logic) dbr:Sequent_calculus dbr:Variety_(universal_algebra) dbr:Non-constructive dbr:Propositional_variable dbr:Mu_calculus dbr:Roger_Lyndon dbr:Non-logical_symbol dbr:Modularity_(programming) dbr:Ontology_(computer_science) dbr:Tautological_implication dbr:Dov_M._Gabbay dbr:William_Craig_(logician) dbr:Consistency_proof dbr:Cut_elimination dbr:Well_formed_formula dbr:Positive_occurrence |
| dbp:wikiPageUsesTemplate | dbt:= dbt:Cite_book dbt:NumBlk dbt:EquationRef dbt:EqNote dbt:Abs |
| dct:subject | dbc:Lemmas dbc:Mathematical_logic |
| gold:hypernym | dbr:Result |
| rdf:type | yago:WikicatLemmas yago:WikicatMathematicalTheorems yago:Abstraction100002137 yago:Communication100033020 yago:Lemma106751833 yago:Message106598915 yago:Proposition106750804 yago:Statement106722453 yago:Theorem106752293 |
| rdfs:comment | In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem. (en) Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen: Es seien und zwei Theorien und der Satz sei ein in ableitbarer Satz. Dann gilt: Es gibt ein , sodass in ableitbar ist, und ist in ableitbar. (de) En logique mathématique, le théorème d'interpolation de Craig dit que si une formule φ en implique une deuxième ψ, et que φ et ψ partagent au moins un symbole non logique en commun, alors il existe une formule ρ, appelée interpolant, telle que : * φ implique ρ ; * ρ implique ψ ; * tout symbole non logique dans ρ apparaît à la fois dans φ et ψ. (fr) 크레이그의 보간 정리(Craig's interpolation theorem, -補間 定理)는 증명 이론의 정리로, 미국의 철학자이자 논리학자인 가 제시하였다. 간단히 말해 다음과 같이 쓸 수 있다. * 어떤 논리식 a에서 다른 논리식 b를 추론할 수 있다고 하자. 그러면, c에서 나타나는 모든 는 a와 b 각각에서도 나타나는 제3의 논리식 c가 존재하여 a에서 c를 추론할 수 있고, 다시 c에서 b를 추론할 수 있다. 이 c를 보간(interpolant)이라 한다. 크레이그는 1957년 이 정리를 일차 논리학에 대해 증명하였다. 미국 수학자 이 일차 논리학에 대한 이 정리의 보다 강한 판본을 1959년 증명하였으므로 이 둘을 합쳐 크레이그-린든 정리라 부르기도 한다. (ko) クレイグの補間定理（英: Craig's interpolation theorem）は論理学における定理であり、論理体系によってその定義が異なる。William Craig が1957年、一階述語論理について証明したのが最初である。クレイグの補題とも。 (ja) Twierdzenie Craiga – twierdzenie logiki, a w szczególności rachunku predykatów pierwszego rzędu. Udowodnione przez (ang.), amerykańskiego logika. (pl) |
| rdfs:label | Craig-Interpolation (de) Craig interpolation (en) Théorème d'interpolation de Craig (fr) 크레이그의 보간 정리 (ko) クレイグの補間定理 (ja) Twierdzenie Craiga (pl) |
| owl:sameAs | freebase:Craig interpolation yago-res:Craig interpolation wikidata:Craig interpolation dbpedia-de:Craig interpolation dbpedia-fr:Craig interpolation dbpedia-ja:Craig interpolation dbpedia-ko:Craig interpolation dbpedia-pl:Craig interpolation https://global.dbpedia.org/id/8Stv |
| prov:wasDerivedFrom | wikipedia-en:Craig_interpolation?oldid=1059769235&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Craig_interpolation |
| is dbo:wikiPageDisambiguates of | dbr:Interpolation_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Craig_Interpolation dbr:Interpolation_(logic) dbr:Craig's_interpolation_lemma dbr:Craig's_interpolation_theorem dbr:Craig_interpolation_lemma dbr:Craig_reduct |
| is dbo:wikiPageWikiLink of | dbr:Dependence_logic dbr:Cut-elimination_theorem dbr:Vampire_(theorem_prover) dbr:Infinitary_logic dbr:Institutional_model_theory dbr:List_of_lemmas dbr:Interpolation_(disambiguation) dbr:Interpolation_theorem dbr:Robinson's_joint_consistency_theorem dbr:Joseph_Sgro dbr:William_Craig_(philosopher) dbr:Craig_Interpolation dbr:Larisa_Maksimova dbr:Craig's_theorem dbr:Johann_Makowsky dbr:Independence-friendly_logic dbr:List_of_theorems dbr:Roger_Lyndon dbr:Interpolation_(logic) dbr:Craig's_interpolation_lemma dbr:Craig's_interpolation_theorem dbr:Craig_interpolation_lemma dbr:Craig_reduct |
| is foaf:primaryTopic of | wikipedia-en:Craig_interpolation |