 The characterization of the (classical first-order) consequence relation given above was semantic, in that we described it in terms of the consequence operation Th ○ Mod which invokes the structures for the language and what is true in them. A proof system for first-order logic provides a direct syntactic account of when φ is a consequence of Γ, in terms of derivability using rules (and perhaps axioms) sensitive only to the form of the formulas involved. We could discuss the properties of sentence connectives in terms of such quantified languages (in which open as well as closed sentences can be their arguments) but to avoid extraneous complications prefer the setting of the propositional languages with which we began. And, as in the discussion to this point, we will generally just say “connective”, rather than “sentence connective”.