The-discovery-of-E.W.-Beths-semantics-for-intuitionistic-logic.pdf
《The-discovery-of-E.W.-Beths-semantics-for-intuitionistic-logic.pdf》由会员分享,可在线阅读,更多相关《The-discovery-of-E.W.-Beths-semantics-for-intuitionistic-logic.pdf(10页珍藏版)》请在三一文库上搜索。
1、The discovery of E.W. Beths semantics for intuitionistic logic A.S. Troelstra and P. van Ulsen Abstract One of van Benthems predecessors, and the fi rst in line of the Dutch logicians, was Evert Willem Beth. During the last decade of his life he worked on a truly constructive semantics for intuition
2、istic logic, with a corresponding completeness theorem.The result is known as “Beth models”. We try to describe his intents and eff orts, but it is not possible to give a clear story line: the data are too scarce.However, we attempt a reconstruction. For this we not only used published records, but
3、as much as possible also quotes from correspondence. Beth semantics combine trees, tableaus, choice sequences and fans. Intuitionistically acceptable completeness required Beth to avoid certain classical notions, in particular K onigs Lemma. Instead, Beth used Brouwers fan theorem. Contents 1Introdu
4、ction2 2Semantics for intuitionistic logic “before Beth”2 3Beths Indagationes paper from 1947 and the Berkeley lecture in 19523 4On the Paris lecture of 1955 and the tools for constructive semantics4 5The paper from 1956 and afterwards7 1 1Introduction Johan van Benthem occupies a position which was
5、 once held by Evert Willem Beth. Johans 50th birthday seemed a suitable occasion for investigating the work of one of his scientifi c ancestors; so here we take a look at Beths discovery of “Beth semantics” and completeness for “Beth models”. To our regret, we do not have a clear story line: the dat
6、a are too scarce. But we have done our best, and have sketched a reconstruction. For this reconstruc- tion, we used not only published records, but as much as possible also quotes from correspondence. The corrrespondence is preserved at Haarlem (Rijksar- chief in Noord-Holland) with the name of “E.W
7、. Beth Archive”. 2Semantics for intuitionistic logic “before Beth” In L.E.J. Brouwers writings from 1908 onwards there is, more or less implicitly, an informal intuitionistic interpretation of certain logical operators such as “or”, “implies”, and “not”. This interpretation was formulated more preci
8、sely, as an informal interpre- tation of formal logical expressions by A. Heyting, fi rst in Heyting (1931), and later, more completely in the monograph Heyting (1934). A similar interpre- tation was formulated by A. Kolmogorov in a paper which appeared in 1932. Originally Heyting and Kolmogorov reg
9、arded their respective interpretations as distinct, but later Heyting came to regard them as essentially the same. It is for this reason that this interpretation is usually referred to as the Brouwer- Heyting-Kolmogorov interpretation, or BHK-interpretation. Where classical semantics describes how t
10、he truth-value of a logically com- pound statement is determined by the truth-values of its components, the BHK- interpretation describes what it means to prove a logically compound state- ment in terms of what it means to prove the components. In this explanation, “constructive proof”, “constructiv
11、e method” appear as primitive notions. Kol- mogorov interpreted statements as problems, and the solving of the problem associated with a logically compound statement is explained in terms of what it means to solve the problems represented by the components. The connection with Heytings formulation b
12、ecomes clear if we think of “solving the problem associated with statement A” as “proving A”. Because of the vagueness of the notions of “constructive proof”, “construc- tive operation”, the BHK-interpretation has never become a versatile technical tool in the way classical semantics has. Perhaps it
13、 is correct to say that by most people the BHK-interpretation has never been seen as an intuitionistic counterpart to classical semantics. Another approach to semantics for intuitionistic logic started with Jaskowski (1936) who used certain systems of truth-values, special cases of Heyting alge- bra
14、s, for a completeness proof for intuitionistic propositional logic. Stone (1937) does not explicitly state a completeness theorem, but in fact his paper contains a completeness result for intuitionistic propositional logic. Tarski (1938) obtains a completeness result for intuitionistic propositional
15、 cal- 2 culus IPC w.r.t. valuations using open sets in topological spaces (in particular IRn) as values. Tarski also sketches an extension to valuations in a suitable class of lattices (More about this in Troelstra Beth explains at some length the idea of semantics in Tarskis sense. He then turns to
16、 intu- itionism; as its key notion he sees the notion of a spread. He cites Brouwers defi nition and then recasts it in a more formal way.Later Heyting, in his book “Intuitionism, an introduction” gave a simplifi ed and clear presentation of Brouwers notion. Beths reformulation may be seen as a fi r
17、st step in this direction. (This point was appreciated by S.C. Kleene in his review of Beths paper in the Journal of Symbolic Logic in 1948.) Beth also asks whether the spread law could always to be taken to be recursive; he thought not, from an intuitionistic point of view. Recursiveness was to nar
18、row for intuitionistic pur- poses. Beth got his credits, together with Kleene, in Odifreddi (1989), p. 118. But on the whole the content of this paper is quite meager, although it should not be forgotten that Tarskis notion of semantics dating from 1935 was at that time still relatively unfamiliar t
19、o many. There exists a draft in Dutch of this paper, which apparently was sent together with a letter to L.E.J. Brouwer; the letter is dated july 7, 1945. Cu- riously enough, the letter starts with “Herewith I take leave to send you some remarks on non-intuitionistic mathematics .”, while the manusc
20、ript which is supposed to have been sent with this letter almost exclusively deals with 3 intuitionism. So is this a typing error, or do the manuscript and the letter not really belong together? Perhaps neither of these: it probably was a joke, typical for Beths sense of humor, according Dick de Jon
21、gh. Beth returned to spreads, and in particular Brouwers “fan theorem” for fi nitary spreads in the lecture “Compactness proofs in intuitionistic mathemat- ics” at the Mathematics Colloquium at Berkeley (May 15, 1952; ms. in two versions). In this lecture Beth presents a version of Brouwers proof of
22、 the bar theorem and the fan theorem; Beth states that the version is due to a student of Heyting, Pinxter. In the argument as presented by Beth, some subtleties of Brouwers original argument have been swept under the carpet. Beth then pro- ceeds to show that the fan theorem can fulfi ll the role of
23、 classical compactness in intuitonistic mathematics; he discusses in particular how the Heine-Borel covering theorem for the interval may be obtained from the fan theorem. He realizes that the application of the fan theorem is not entirely straightforward, but that one must choose the right sort of
24、spread representation for the inter- val (a fact known to Brouwer). In short, the paper does not contain any new result, but it testifi es to Beths ongoing preoccupation with Brouwers proof of the fan theorem and shows his awareness of the fact that if one wants to fi nd an intuitionistic substitute
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- The discovery of Beths semantics for intuitionistic logic
链接地址:https://www.31doc.com/p-3800879.html