bnh@wiis.wang.com (Bill Halchin) (08/03/90)
Recently, I have been reading a number of books on mathematical logic, e.g. Kleene's Intro to Metamathematics, Cohen's Computability & Logic. These books take the usual formalist approach of the concept of provability, i.e. pure symbol manipulation involving a recursive set of axioms & a set of rules of inference. However, I have also been reading the book Computability & Logic by Boolos & Jeffrey (Cambridge), which seems to be an excellent book with recent results like Chaitin's work on algorithmic complexity. One thing confusesme though. In Boolos & Jeffrey, the notion of provability is tied to model theory, i.e. it's tied to semantics not syntax. A theory is the set of sentences closed under logical consequence. Logical consequence in their book is a semantical concept, i.e. A -> B iff for every model M of A & B, if A is true, then B must be true. I don't understand the connection between Boolos/Jeffrey concept of a theory(set of theorems) and the usual approach, e.g. Kleene or Goedel? Can somebody please help to understand this?? Thank you. Bill Halchin
hbe@sonia.math.ucla.edu (H. Enderton) (08/07/90)
In article <1990Aug3.162306.29574@wiis.wang.com> bnh@wiis.wang.com
(Bill Halchin) asks about the connection between provability (with
axioms and rules of inference) and logical consequence (defined
semantically).
The remarkable connection between provability and logical consequence
(for first-order logic) is given by the Godel completeness theorem.
(Not to be confused with the Godel incompleteness theorem.) Since you
have Kleene's book, see section 72. The completeness theorem must be
in Boolos & Jeffrey also (which is probably a better place to start).
--hbeweibel@brain.inf.ethz.ch (Trudy Weibel) (08/14/90)
The completeness theorem (Go"del) says that a formal proof (derivation) is equivalent to a semantical proof: |- <=> |= The => direction is called soundness and can be found in Boolos & Jeffrey (2.ed) on p. 126, the other direction <= is the what people often call the completeness and can be found on that book on pff. 131. -- trudy --