Path: utzoo!attcan!uunet!mcsun!cernvax!chx400!ethz!neptune!brain!weibel
From: weibel@brain.inf.ethz.ch (Trudy Weibel)
Newsgroups: comp.theory
Subject: Re: Math Logic
Keywords: proof model
Message-ID: <1718@neptune.inf.ethz.ch>
Date: 13 Aug 90 17:53:11 GMT
References: <1990Aug3.162306.29574@wiis.wang.com> <213@kaos.MATH.UCLA.EDU>
Sender: news@neptune.inf.ethz.ch
Reply-To: weibel@brain.inf.ethz.ch (Trudy Weibel)
Distribution: sci.logic
Organization: Departement Informatik, ETH, Zurich
Lines: 11



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 --