type; fixes #405

Author: rzach

content/first-order-logic/proof-systems/introduction.tex

@@ -21,7 +21,7 @@
 a sequence (or other finite arrangement) of !!{sentence}s or
 !!{formula}s.  Good !!{derivation} systems have the property that any
 given sequence or arrangement of !!{sentence}s or !!{formula}s can be
-verified mechanically to be ``correct.''  
+verified mechanically to be ``correct.''
 
 The simplest (and historically first) !!{derivation} systems for
 first-order logic were \emph{axiomatic}.  A sequence of !!{formula}s
@@ -89,11 +89,11 @@
 useful, but at least they pass that minimal threshold of logical
 usefulness.  For different !!{derivation} systems the specific
 definition of consistency of sets of !!{sentence}s might differ, but
-like $\Proves$, we want consistency to coincide with its semantic
+like~$\Proves$, we want consistency to coincide with its semantic
 counterpart, satisfiability. We want it to always be the case that
 $\Gamma$ is consistent if and only if it is satisfiable. Here, the
-``if'' direction amounts to completeness (consistency guarantees
-satisfiability), and the ``only if'' direction amounts to soundness
+``only if'' direction amounts to completeness (consistency guarantees
+satisfiability), and the ``if'' direction amounts to soundness
 (satisfiability guarantees consistency).  In fact, for classical
 first-order logic, the two versions of soundness and completeness are
 equivalent.