The "logically implies" concept in first-order logic I've been reading about first-order logic (in Enderton, and in Rautenberg) and I've gotten to the point where (I think) I understand what it means for a set of formulas to "logically imply" another formula. I'm a bit confused by one thing though...the absence of words like "axiom" and "theorem". Isn't this stuff supposed to be the definition of what a theorem is? Also, I'd like some clarification on the terms "model theory" and "proof theory". This "logically implies" stuff is presented shortly after the concept of a "model", and uses it in the definition. And I feel that this has to be the stuff that defines what's considered a proof. So this stuff I'm reading...should I think of this as the intersection of model theory and proof theory, or do those terms mean something I still don't get?