1.2.6 Valid Arguments
More on valid arguments.
Now, validities are clearly logical in a certain sense; they are descriptions featuring a cast-iron guarantee of satisfiability. But logic has traditionally appealed to the more dynamic notion of valid arguments, a movement, or inference, from premises to conclusions.
Valid arguments.
Suppose 
, and 
are a finite collection of first-order formulae. We then call the argument with premises 
and conclusion a valid argument if and only if the following is true for this argument: Whenever all the premises are satisfied in some model using some variable assignment, then the conclusion is also satisfied in the same model using the same variable assignment. The notation
means that the argument with premises 
and conclusion is valid.
Terminology.
There is an extensive terminology when it comes to talking about valid arguments, allowing us for example to refer to as a valid inference from the premises , or to as a logical consequence of .
Note that if the premises and the conclusion are all sentences the definition of valid arguments can be rephrased as follows: an argument is valid if whenever the premises are true in some model, the conclusion is true as well. In a nutshell: the truth of the premises guarantees the truth of the conclusion.
Proof Theory.
Validity and valid arguments are the fundamental logical concepts underlying the notion of inference. Both concepts are semantically defined (that is, they are defined in terms of models and variable assignments). The subject of proof theory is to define them in terms of syntax. We will cover this in Chapter 7.
Proof Systems
Syntactic calculi for inference may even be employed in computational implementation: Various proof systems have been developed, and we will see in in this course how the syntactic method of first order tableaux can be implemented in Prolog.