 |
| Understanding Constructive Semantics (Spinoza Lecture), ebook, filozofia, spinoza |
 |
|
|
[ Pobierz całość w formacie PDF ] Understanding Constructive Semantics (Spinoza Lecture) Sergei N. Artemov Cornell and Moscow University August 17, 1999 Abstract Is there an alternative mathematics? In particular, does intuitionism yield an essen- tially new approach that cannot be speci¯ed within classical mathematics? The intended informal meaning of intuitionistic logic Int was given in the 1930s by the Brouwer-Heyting- Kolmogorov semantics which understands intuitionistic truth as provability. Moreover, Kolmogorov (and later Godel) suggested interpreting Int via classical provability and thus providing a meaningful semantics for Int independent of intuitionistic assumptions. Natural attempts to formalize this semantics met serious di±culties related to Godel's incompleteness phenomenon. In this lecture we will talk about recent advances in this area that have bridged the incompleteness gap and provided an adequate formalization of the propositional Brouwer-Heyting-Kolmogorov semantics based on classical provability. Plan 1. Brouwer - Heyting - Kolmogorov provability semantics for intuitionistic logic 2. De¯ning intuitionistic logic in classical provability logic 3. Explicit vs. implicit approaches 4. Proof polynomials and Logic of Proofs 5. Solution of Godel's problem and the propositional BHK problem 6. First order case 7. Discussion 1 1 Brouwer - Heyting - Kolmogorov provability semantics for intuitionistic logic According to Brouwer (1907 and 1918), intuitionistic truth means provability. Here is a sum- mary in this issue taken from A. Troelstra and D. van Dalen Constructivism in Mathematics. An Introduction , v. 1 (1988). page 4. \It does not make sense to think of truth or falsity of a mathematical statement indepen- dently of our knowledge concerning the statement. A statement is true if we have a proof of it, and false if we can show that the assumption that there is a proof for the statement leads to a contradiction." In 1931-32 Heyting and Kolmogorov made Brouwer's de¯nition of intuitionistic truth explicit, though informal, by introducing what is now known as Brouwer-Heyting-Kolmogorov (BHK) semantics .Now BHK semantics is widely recognized as the intended semantics for intuitionis- tic logic Int 1 . According to BHK a statement is true if it has a proof, and a proof of a logically compound statement is given in terms of the proofs of its components. The description uses the unexplained primitive notions of construction and proof . It stipulates that ² a proof of a proposition A ^ B consists of a proof of A and a proof of B , B is given by presenting either a proof of A or a proof of B 2 , ² a proof of A _ ² a proof of A ! B is a construction which, given a proof of A returns a proof of B , ² absurdity ? is a proposition which has no proof and a proof of : A is a construction which, given a proof of A , would return a proof of ? . Here are minimal a priori requirements to a formal BHK semantics for intuitionistic logic. 1. It should be based on real proofs in a certain background formal theory (or a class of theories). In particular, 1 In this talk by Int we understand intuitionistic propositional logic also known as IPC . The provability se- mantics problem for Int was central in the papers A. Kolmogoro®, \Zur Deutung der intuitionistischen Logik." - Mathematische Zeitschrift , v. 35 (1932), pp. 58-65 and K. Godel, \Eine Interpretation des intuitionistischen Aussagenkalkuls", Ergebnisse eines mathematischen Kolloquiums , v. 4 (1933), p. 39-40. 2 Nowhere in the original Heyting or Kolmogorov writings could I ¯nd the well-known extra condition on the disjunction: a proof of a disjunction should also specify which one of the disjuncts it is a proof of. This condition is clearly redundant for the usual notion of a proof: since the predicate \ p is a proof of F " is decidable given a proof p we always know which one of the disjuncts p is a proof of. Kreisel (1965) suggested some further modi¯cations of the BHK semantics. In our talk we consider the original BHK formulation by Heyting and Kolmogorov. 2 a) the predicate Proof(p,F) meaning \ p is a BHK proof of F " should be decidable, b) BHK proofs should enumerate theorems of the background theory T , i.e. ` , T F Proof(p,F) for some p 2. It should be non-circular. For example, BHK proofs should not be derivations in a formal system based on Int itself. Until recently there were no sound semantics for Int suggested which met these minimal BHK requirements. Dirk van Dalen in the chapter \Intuitionistic Logic" in Handbook of Philosophical Logic , v. 3. (1986), p. 243, writes: \The intended interpretation of intuitionistic logic as presented by Heyting, Kreisel and others 3 so far has proved to be rather elusive. ... However, ever since Heyting's formal- ization, various, more or less arti¯cial, semantics have been proposed." There is an important distinction between Heyting's and Kolmogorov's descriptions of the BHK semantics. Despite strong technical similarities their approaches had fundamentally di®erent objectives. Presumably, Heyting explained Int in terms of the intuitionistic under- standing of constructions and proofs. Kolmogorov in 1932 (and then Godel in 1933 and 1938) intended to interpret intuitionistic logic on the basis of the usual mathematical notion of proof (problem solution), and thus to provide a de¯nition of Int within classical mathematics in- dependent of the intuitionistic assumptions. For purposes of formalization of BHK semantics it is important to distinguish between Heyting and Kolmogorov - Godel interpretations. We will use the names intuitionistic BHK semantics for the former and classical BHK semantics for the latter. In this talk we will be interested in the classical BHK semantics. Intuitionistically acceptable semantics for the intuitionistic logic was studied by Kreisel, Kripke, Dyson, van Dalen, Leivant, Veldman, de Swart, Dummet, Troelstra, H. Friedman, Visser, and others. Those studies met considerable technical di±culties (cf. D. van Dalen's chapter \Intuitionistic Logic" in Handbook of Philosophical Logic , v. 3. (1986)). To the best of our knowledge none of the suggested interpretations satis¯es the minimal requirements to a formal BHK semantics above. Here is the list of major known classical semantics for intuitionistic logic. 1. Algebraic semantics (Birkho®, 1935) 2. Topological semantics (Stone, 1937; Tarski, 1938) 3. Realizability semantics (Kleene, 1945) 4. Beth models (1956) 5. Dialectica Interpretation (Godel, 1958) 6. Curry - Howard isomorphism (1958) 3 I.e. the BHK semantics. { S.A. 3 7. Medvedev's logic of problems (1962) 8. Kripke models (1965) 9. Kuznetsov - Muravitsky - Goldblatt - Boolos provability interpretation (1976) 10. Categorical semantics (Goldblatt, 1979) Those interpretations have shown to be extremely fruitful for understanding intuitionistic logic. However, none of them may be considered as a BHK type semantics. Semantics1{5,7,8,10arenotconnected to provability. In particular, Kleene realizability provides a computational but not provability semantics of intuitionistic logic 4 . Indeed, the predicate \ x realizes F " is not decidable, Kleene realizers do not enumerate theorems of any formal theory. It is also worth of mentioning that Kleene realizability is not an adequate semantics for Int , i.e. there are realizable propositional formulas not derivable in Int . Curry - Howard isomorphism transliterates natural derivations in Int to the corresponding ¸ -terms. This is a powerful device connecting proofs and programs which may be regarded as a sort of a computational semantics for Int . However, its foundational signi¯cance is rather limited. From the BHK point of view Curry - Howard isomorphism provides the trivial semantics which de¯nes \ F is intuitionistically true" as \ F is derivable in Int " and therefore is obviously circular. Kuznetsov - Muravitsky - Goldblatt - Boolos semantics for Int translates a propositional formula F into F ¡ by pre¯xing all atoms and all implications in F by the modal operator 2 A as \A and Provable(A) " where Provable is the predicate of formal provability in the ¯rst order arithmetic PA . Int is known to be sound and complete with respect to this semantics. This semantics, however, is highly nonconstructive since it appeals to the unrestricted notion of classical truth for arithmetical formulas. For example, it stipulates that A (McKinsey - Tarski translation) and then decodes 2 B is intuitionistically true i® A and B are both classically true and provable in PA . In addition, it has nothing to do with BHK since there are no individual proofs and operations on proofs present whatsoever. An attempt to formalize BHK semantics directly was made by Kreisel in 1962 and 1965 in his theory of constructions. Kreisel's original variant of the theory turned out to be incon- sistent, and the problem occurred already at the propositional level. Goodman (1970) ¯xed that gap but his solution involved a strati¯cation of constructions into levels which ruined the BHK character of this semantics. In particular, a proof of A ^ B was no longer a function that could be applied to any proof of A . A comprehensive account of Kreisel - Goodman theory could by found in the paper by S. Weinstein, \The intended interpretation of intuitionistic logic", Journal of Philosophical Logic, v. 12 (1983), pp. 261-270, which concludes that ! \The interpretation of intuitionistic theories in terms of the notions of proof and construc- tion ... has yet, however, failed to receive a de¯nitive formulation." 4 Kleene himself denied any connection of his realizability with BHK interpretation. 4 In this talk we will demonstrate that the propositional classical BHK semantics admits an exact mathematical formalization, which indeed provides an adequate speci¯cation of Int on the basis of the usual classical notion of proof independent of any intuitionistic assumptions. This solves the problem studied by Kolmogorov (1932) and Godel (1933). Along with the obvious foundational 5 , historical 6 and mathematical 7 motivations for tack- ling this problem, I would like to mention two more. 1. Modal logic and ¸ -terms provide two parallel languages describing provability. Modality permits iterations, ¸ -terms are explicit and more informative. Why don't we try to do both? 2. There is a number of questions in modal logic, typed theories, knowledge representation, constructive semantics, theory of veri¯cation, etc. related to the notion of probability, which have not been addressed by the traditional theory of formal (implicit) provability. 2 De¯ning intuitionistic logic in classical provability logic Perhaps, the ¯rst paper on formal provability semantics for intuitionistic logic was written in 1928 by Orlov in Russian 8 . Referring to Brouwer's papers on intuitionism he suggested pre¯xing all subformulas of a given propositional intuitionistic formula by 2 with the informal reading of F as \ F is provable", and understanding the logical connectives in the usual classical way. His modal axioms for provability coincide with the Godel axioms for the modal logic S4 (1933), though Orlov's system was weaker than S4 because he chose a certain proper fragment of classical logic on the background. Godel in 1933 independently introduced the modal calculus of provability (which turned out to be another axiomatization of one of the Lewis modal systems S4 ) and de¯ned Int in this logic. Godel's provability logic admits all axioms and rules of classical logic and has the modal axioms and rules 2 2 ! F F , 2 ( F ! G ) ! ( 2 F !2 G ), 2 F !22 F , F ` 2 F ( necessitation rule). Godel considered the translation t(F) of an intuitionistic formula F into the classical modal language similar to the Orlov translation: \box each subformula of F ". Both apparently 5 A loophole in the foundations of constructive logic. 6 One of the oldest well-known problems in logic. 7 A challenge: new approaches were needed. 8 I.E. Orlov. \Izchislenie sovmesntosti predlozhenii" Matematicheskii sbornik (i.e. \The calculus of compat- ibility of propositions", Mathematics of the USSR, Sbornik ), v. 35 (1928), pp.263-286 (in Russian). 5 [ Pobierz całość w formacie PDF ] |