Talk:Craig interpolation

Same as Craig's theorem?

Hey,

I'm not sure about this, but is Craig Interpolation in mathematical logic the same as Craig's Theorem in philosophical logic? If not wouldn't a page be useful explaining this; rather than a redirector? When looking for help on Craig's theorem this confused me! From what I can understand, the philosophical Craig's Theorem was posited by William Craig, in a paper from the Journal of Symbolic Logic, Vol. 18 (1953), in a paper called "On Axiomatisation within a System" and essentially talks about the possibility of replacing a formal language with theoretical and observational terms with a language with just observational terms. Apologies for wasting time if the two are one-and-the-same. If I end up reading more into Craig's Theorem (philosophical) and it does turn out to be different; I'll write an article. Thanks,

Ed —Preceding unsigned comment added by 131.111.228.48 (talk • contribs)

I am also confused about this page. Could anyone provide more thorough introduction? e.g. the meaning of arrows as in "X -> Y" appear out of the blue. Is that (logical) implication? function? injection? —Preceding unsigned comment added by 130.225.195.132 (talk) 11:58, 10 November 2008 (UTC)[reply]

I expanded it some; is it any better? — Carl (CBM · talk) 14:07, 10 November 2008 (UTC)[reply]

Problems in Lyndon section, with implications for introduction too

I noticed a couple of problems in the Lyndon section, both fixable.

1) "let S ∩ T be the intersection of the two theories; the signature of S ∩ T is the intersection of the signatures of the two theories." The notion of intersecting two theories is not defined here, but if it is intended to mean the intersection of the sets of sentences contained in S and T, then it is the wrong notion for this purpose. Two theories S and T can contain no common sentences, while containing many common symbols. Thus signature(S ∩ T) could be empty even though signature(S)∩signature(T) is not; and it is the latter that is needed in the theorem. (Moreover, it is not mathematically acceptable to stipulate that signature(S ∩ T) actually means the intersection of the signatures, despite what the notation implies!) The "intersection of the two theories" is a concept that plays no role here at all, whatever it means. So I would propose not introducing it, and using signature(S)∩signature(T) instead.

2) The first part of the Lyndon theorem statement says "if S ∪ T is unsatisfiable, then there is a interpolating sentence ρ in the language of S ∩ T that is true in all models of S and false in all models of T." This is identical to the "informal" statement of Craig's theorem in the introduction: "if a formula φ implies a formula ψ then there is a third formula ρ, called an interpolant, such that every nonlogical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ." where S plays the role of φ, T plays the role of ~ψ, and ρ plays the role of ρ. If we replace the ambiguous word "implies" by the somewhat more precise "entails", then the two statements are exactly equivalent, except that the statement in the introduction is readable while the statement in the Lyndon section is not. It seems to me that having two equivalent statements using different notation and language, with no mention that they are identical, is guaranteed to cause problems for most readers.

The logical conclusion is that it would make sense to have a precise statement of Craig's theorem, either before or after the example, followed by a precise statement of the way in which Lyndon's theorem extends Craig's. SR2012 (talk) 19:50, 4 February 2012 (UTC)[reply]

I disagree!

Craig's interpolation theorem is *NOT* a result about the relationship between different logical theories. φ, ρ and ψ are all formulae of *ONE* theory. Perhaps the author was thinking of Lyndon's interpolation theorem? 109.158.6.142 (talk) 14:55, 17 October 2020 (UTC)[reply]

true Staticgloat (talk) 02:03, 15 March 2021 (UTC)[reply]