ABSTRACT
So far, we have focused on syntax in studying logical systems. We have defined different formal languages and in each language we have defined different types of proof in that language. In doing this, we have given meanings to connectives by way of the rules in which they feature. The starkest example of this is given in natural deduction systems. The introduction and elimination rules for a connective can be thought to give some account of the meaning of that connective. So these largely syntactic procedures have a semantic purpose.
