The-discovery-of-E.W.-Beths-semantics-for-intuitionistic-logic.pdf

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 intuitionistic 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 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 1Introduction2 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 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 data 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. 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 precisely, 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 regarded 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 the 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”, “constructive 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 becomes 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 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- bras, 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 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 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 rst 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 narrow 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 to 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 manuscript 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 Jongh. 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 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 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 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 for a classical compactness argument, one needs the fan theorem. It is remarkable that Beth never not in this lecture but also not in his later work referred to Brouwer (1926). There Brouwer presented an intuitionistically acceptable variant of Heine-Borel. 4On the Paris lecture of 1955 and the tools for con- structive semantics Beth made real progress with the semantics of intuitionistic predicate logic only after he had invented the semantic tableaus for classical logic in 1954 (later pub- lished as Beth (1956a). In Beth (1955a), the next step, he tried to formulate a decision method for intuitionistically acceptable formulas, given that they are classically acceptable. He used semantic tableaux, and their deductive tran- formation. Beth (1955b), p. 341342: “I stated the conjecture that semantic tableaux might provide us a decision procedure for intuitionistic validity of clas- sically valid formulas.” Beths hope was destroyed by Kleenes letter of June 7, 1955 (Madison). Kleene gave some counterexamples and fi nished his objections as follows: There can be no decision procedure for the problem let A be a formula which holds classically; does A also hold intuitionistically? . At any rate I do not see how to rule out such possibilities i.e. Kleenes counterex- amples; and so it does not seem implausible that increasing the number of individuals taken into consideration as Beth proposed might give room for a correct proof intuitionistically in place of one correct classically but incorrect intuitionistically. For Beths agreement with Kleene see Beth (1955b), p. 341342. The intuitionistic system G3 in Kleenes “Introduction to Metamathemat- ics” (p. 481), was taken by Beth as the basis for his syntax. Out of this Beth 4 developed his tableaux (trees with attached formulas); or, as Beth said in his “Foundations of mathematics”, p. 450, If read upside down, the above i.e. intuitionistic syntactical rules may also be construed as instructions for the construction of a semantic tableau. Kleene, and his predecessor G. Gentzen, had disjunctive and conjunctive clauses (for the tableaux the conjunctive and disjunctieve splittings). Beth added in- fi nite regression for the branches of his trees; this was produced by cyclic per- mutation of formulas. It is not very clear how Beth discovered his semantics.Correspondence about this topic is of a later date and Beth never gave a precise description of the way he arrived at his ideas. So we use a lot of quotations from sources later than 1956, but a real reconstruction is impossible. On May 3, 1957 Beth sent a letter to Heyting from Baltimore, while he was a visiting professor at Johns Hopkins University. In that letter, written after his discovery, you can fi nd a clue to the beginnings of the intuitionistic use of semantic tableaux: Indeed I start from a classical, hence intuitionistically debatable notion of model; however, my considerations concern classical logic. Moreover, a con- siderable part of the construction is nevertheless intuitionistically accept- able, since the tree construction associated with a logical problem produces a collection of models which can be represented by a fi nitary spread. In the same letter Beth told that he was examined by G. Kreisel: Concerning my construction of intuitionistic logic, I had in Princeton an in- teresting conversation with Kreisel, who seemed rather taken with the idea; he proposed an exam-question, which I was able to answer satisfactorily. In 1955 Beth gave a lecture in Paris on the semantics of intuitionistic logic, in which he sketches the essentials of his semantics. The lecture was published in 1958, only after his more substantial paper on the same topic had appeared in 1956. The lecture of 1955 is a big step forward. Beth sketches the clauses for intu- itionistic validity in his models, and discusses some examples. However, there is still no indication of a completeness proof, and one of the clauses for validity is manifestly inadequate (namely, the clause for the validity of an existential statement). The absence of a completeness proof is not so strange, if you read Beths letter of September 5, 1955 to A. Robinson (italics by the authors): In my paper on intuitionistic logic, I take a non-intuitionistic attitude, and convince myself that, if an intuitionist uses a law of logic not contained in Heytings system, then I can fi nd an intuitionistic counter-example to prove that this law is not acceptable from an intuitionist point of view. For the denumerable case, the lemma of infi nity is not needed, we only need the (metamathematical) principle of the excluded third. As for the classi- cal logic, an entirely constructive completeness proof cannot be given. But the counter-example, the existence of which is proved by non-constructive methods, is in itself constructive. Within a year Beth changed his mind. His next step, in 1956, was the develop- ment of semantics with constructive completeness for intuitionistic logic. For 5 his formulation of validity Beth made use of trees because of their relationship with tableaux. In Beth (1956b), p. 379, he motivates his use of choice sequences as follows (italics by Beth): . the introduction of the notion of a choice sequence brings a subjective element into the situation. But, as Heyting rightly observes, this subjective element is eliminated if we agree to concentrate upon such properties of choice sequences as appear after a fi nite number of choices. This attitude implies, however, a radical change in the semantic notions. The classical rules determine .the validity or non-validity of a formula on each branch separately . These diffi culties vanish, if we agree to determine validity or non-validity, not on individual branches, but collectively on all those branches which have a certain initial element in common, that is, on a subtree. In this passage, he explains his use of “submodel” (bar). Beth had to avoid some classical principles as compactness (ms. E.W. Beth, “Semantische Tafeln f¨ ur die intuitionistische Pr¨ adikatenlogik erster Ordnung”, lecture IV. ¨ Osterr. Mathematikerkongress, Wien, September 1722, 1956): If the construction of tableaux is interpreted as an attempt to construct a counter-model, then just as before we have to use an intuitionistic non- acceptable compactness argument for the proof that for every non-closed semantic tableau a corresponding counter-model actually exists. The original semantic tableaux had been countermodel-constructions. For intu- itionistic purposes these were now transformed into an operation of fi tting in, as witnessed by a letter from Beth to Heyting, dated November 18, 1955 (this letter must have been written after his Paris lectures, but nevertheless he did not modify Beth (1958) in this respect): Let us think of a certain (given) model of the As, and also of a model, as yet undetermined, which is a union of submodels as intended above. Call these models M and N. Now we are going to split M and N ever farther into submodels. Splitting of M yields a conjunctive splitting of the tableau, splitting of N a disjunctive splitting. The construction succeeds, if we have split M into parts, each of which fi ts into some piece of N. The two “truth values” here are “true” and “not yet decided”. The combination is a fan. Beth used Brouwers fan-theorem with its restrictions as a framework for his intuitionistic completeness proof. It is possible to have infi nite branches in a submodel; these are produced by Beths cyclic permutation of formulas. Beth introduced trunks (truncated trees) with a fi nite depth, in order to compare the conjuctive and the disjunctive part of a model up to a certain depth. Beth formulat