UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Semantic studies of intuitionistic logic Criscuolo, Giovanni 1972

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Notice for Google Chrome users:
If you are having trouble viewing or searching the PDF with Google Chrome, please download it here instead.

Item Metadata

Download

Media
831-UBC_1972_A6_7 C75.pdf [ 3.41MB ]
Metadata
JSON: 831-1.0302122.json
JSON-LD: 831-1.0302122-ld.json
RDF/XML (Pretty): 831-1.0302122-rdf.xml
RDF/JSON: 831-1.0302122-rdf.json
Turtle: 831-1.0302122-turtle.txt
N-Triples: 831-1.0302122-rdf-ntriples.txt
Original Record: 831-1.0302122-source.json
Full Text
831-1.0302122-fulltext.txt
Citation
831-1.0302122.ris

Full Text

CI S E M A N T I C S T U D I E S O P I N T UIT I O N I S T I C L O G I C GIOVANNI CRISCUOLO Laurea i n P i s i c a , U n i v e r s i t y of Naples, I t a l y , 1967 A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OP MASTER OF SCIENCE i n t|re Department of COMPUTER SCIENCE We accept t h i s t h e s i s as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA September,1972 I n p r e s e n t i n g t h i s t h e s i s in p a r t i a l f u l f i l m e n t o f the requirements f o r an advanced degree at the U n i v e r s i t y of B r i t i s h Columbia, I agree tha t t h e L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r reference and s tudy. I f u r t h e r agree t h a t permiss ion f o r ex tens ive copying o f t h i s t h e s i s f o r s c h o l a r l y purposes may be granted by the Head o f my Department o r by h i s r e p r e s e n t a t i v e s . I t i s understock that copying or p u b l i c a t i o n o f t h i s t h e s i s f o r f i n a n c i a l gain sha l l not be al lowed w i thou t my w r i t t e n pe rm iss ion . Department o f Computer Science The U n i v e r s i t y o f B r i t i s h Columbia Vancouver 8, Canada D a t e September 28 , 1972 I I A B S T R A C T This t h e s i s i s a study of i n t u i t i o n i s t i c semantics as presented by Beth ^2 J^ and Kripke JjL2J , using the usual methods of i n v e s t i -gation of c l a s s i c a l informal l o g i c . Beth models and Kripke models are presented i n avujnanner which does not depend upon a p r i o r d e f i n i t i o n of the notion of degree of a formula. I t i s shown that both classes of i n t u i t i o n i s t i c models are a ge-n e r a l i z a t i o n of the concept of c l a s s i c a l models,i.e. they contain c l a s s i c a l models as p a r t i c u l a r case„ and that " branching " i s a necessary condition i n order that i n t u i t i o n i s t i c l o g i c be complete with respect to them. I n t u i t i o n i s t i c s e n t e n t i a l calculus i s complete with respect to the strong Beth model, the i n t e r s e c t i o n of Beth models and Kripke mo-dels.But, i f "by analogy with the c l a s s i c a l case, we extend them to f i r s t order l o g i c we f i n d that they are not adequate because, f o r example, the sentence Vx(B(x) V C) Z> ( 'v'xB(x) V C), where C does not contain x f r e e , i s v a l i d i n these models but not i n -t u i t i o n i s t i c a l l y provable. This observation helps to explain the formal differences between the two classes of models. The s i m p l i f i e d Kripke models and the sim* p l i f i e d Beth models are then introduced and t h e i r equivalence with the Kripke models anff the Beth models, re s p e c t i v e l y , i s proved. I l l The f i r s t ones allow a better notation and a "better understanding of the r e l a t i o n R occurring i n the d e f i n i t i o n of Kripke models. The second ones have the important property that, i f the domain i s f i n i t e , any c l a s s i c a l l y v a l i d sentence i s v a l i d i n them. F i n a l l y a semantic proof of most of the reduction theorems from c l a s s i c a l to i n t u i t i o n i s t i c l o g i c ' i s given. 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 IV TABLE OF CONTENTS Introduction 1 Section 1 - C l a s s i c a l and I n t u i t i o n i s t i c Models f o r f i r s t order l o g i c a l calculus 4 Section 2 - Models f o r s e n t e n t i a l calculus 21 Section 3 — S i m p l i f i e d i n t u i t i o n i s t i c models 32 Section 4 - Reduction theorems from c l a s s i c a l to i n t u i t i o n i s t i c l o g i c 45 Bybliography. 61 V ACKNOWLEDGMENTS I wish to thank professor Paul Gilmore f o r h i s patient guidance during the work f o r t h i s t h e s i s , professors Abbe Mowshowitz and Ray K e i t e r f o r t h e i r moral support during my permanence at the U.B.C. and the Canada Council f o r gram-lring me a scholarship to complete my studies i n Canada 1 INTRODUCTION With the development of modern analysis a d i s t i n c t i o n was drawn "between constructive and non-constructive existence. A constructive existence proof f o r a r e a l number possessing a c e r t a i n property i s an algorithm f o r constructing say a decimal expansion of the number. A non-constructive proof on the other end demonstrates only that the assumption that there are no r e a l numbers with the given property i s contradictory. In the l a s t century disputes arose as to the nature of mathematics "between those advocating a constructive view of r e a l numbers and those taking a broader view. In t h i s century the best known advocates of the constructive view have been L. M. «J". Brouwer, A. Heyting and H. Weyl. B e l l H l J discusses t h e i r point of view as does Beth [j>J . More recently E r r i t Bishop i n £a^J advocates and develops a constru-c t i v e view of mathematics. I t has not been easy i n the past f o r anyone interested, to begin a study of constructive mathematics because of quite widely d i f f e -r i n g ideas as to what i s meant by "constructive" and because of the polemic and- p h i l o s o p h i c a l tone of some of the w r i t i n g . Since i t s formalization by Heyting i n £ 9~J , a formal study of a f i r s t order q u a n t i f i c a t i o n a l l o g i c c a l l e d i n t u i t i o n i s t i c l o g i c has been possible but i t provides l i t t l e i n s i g h t into motivation But with the development of model theories f o r the i n t u i t i o n i s t i c 2 l o g i c by Beth [j?J and Kripke {_12j a person with a c l a s s i c a l ma-thematical t r a i n i n g can study both a semantic- and a l o g i c a l syn-tax f o r i n t u i t i o n i s i c l o g i c simply as a s p e c i a l kind of mathema-t i c a l structures and hope to gain considerable i n s i g h t into a constructive view of mathematics. The importance of such studies f o r anyone interested !±n[ a theore-t i c a l approach to Computer Science should be obvious . The basic concept of Computer Science,that of algorithm or computational procedure,is of course a constructive concept. However the theory of algorithms,or p a r t i a l recursive function theory, i s a c l a s s i c a l theory not a constructive one because of i t s unrestricted use of the excluded middle law? Is t h i s indifference towards the methods pec u l i a r to c o n s t r u c t i -ve mathematics i n Computer Science j u s t i f i e d or not? The only way to answer t h i s question i s a study of the r e l a t i o n s between c l a s s i c a l l o g i c and mathematics and t h e i r constructive counterparts. This i s the motivation f o r t h i s thesis which deals i n p a r t i c u l a r with a w e l l defined t o p i c : a semantic study of i n t u i t i o n i s t i c l o -gic from a purely c l a s s i c a l point of view. In Section 1 c l a s s i c a l models,Beth models and Kripke models are defined i n a manner whieh does not depend upon a p r i o r d e f i n i t i o n of the notion of degree of a formula. In Section 2 i t i s shown that i n t u i t i o n i s t i c s e n t e n t i a l l o g i c i s complete with respect to the strong Beth models,the i n t e r s e c t i o n of Beth models and Kripke models. Moreover an i n t e r e s t i n g p h i l o -3 sophical i n t e r p r e t a t i o n of these models developed by A.G-rzegorczyk In Section 3 ^oth classes of modils are s i m p l i f i e d and contrasted i n order to achieve a better understanding of t h e i r features. With the s i m p l i f i e d Kripke models one can tr e a t i n t u i t i o n i s t i c se-mantics as a ge n e r a l i z a t i o n of c l a s s i c a l semantics simpljr by substituting for -the words "set of signed sentences" the words: " c o l l e c t i o n of sets of signed sentences" and for the c l a s s i c a l r u -l e s .for the l o g i c a l connectives the i n t u i t i o n i s t i c r u l es i n the d e f i n i t i o n of semantic successor. From the other end the s i m p l i f i e d Beth models s a t i s f y the important property that i f the domain i s f i n i t e any c l a s s i c a l ^ v a l i d sentence i s v a l i d i n them. F i n a l l y i n Section 4 the w e l l known reduction theorems from c l a s s i -c a l to i n t u i t i o n i s t i c l o g i c are proved semantically using the sim-p l i f i e d Kripke models. S E C T I O N 1 C l a s s i c a l and i n t u i t i o n i s t i c models f o r f i r s t order l o g i c a l calculus Let £3 be an at most countable non empty set of namesra-^, a^,... Let 9) be an at most countable set of predicate letters:A^»A^»•••• An atomic formula from S andS) i s an expression of the type A(k^,...,k^) where A is an n-place predicate l e t t e r In 3) and f o r each ifn k^ i s eit h e r an element of S or a var i a b l e whose range";iso7" Formulas from S and2) are b u i l t i n the usual way from atomic f o r -mulas : using the connectives &, V,~' , 3 , a n d the qu a n t i f i e r s V,3. A sentence (atomic sentence) i s a formula (atomic formula) without free v a r i a b l e s i n i t . Upper case l e t t e r s B,C,D,... are used to denote sentences,while the l e t t e r A i s reserved to denote only atomic sentences. I f a. ,...,a. , are a l l the names i n the sentence S and'if no eon-fusion can ar i s e from the context, we write B(a) f o r B(a. ,...,a. ) and a £ - 0 f o r "a i c d f o r a l l j ^ n " . A set T* of sentences from S and 2 ) i s any set whose sentences con-t a i n only names i n ^  and predicate l e t t e r s i n 2 ) . A signed sentence i s any expression of the form +B or -B where B i s a sentence. A consistent set of signed sentences i s any set of signed sentences which does not contain +B and -B f o r any sentence B. DEF. 1 - Let f be a set of signed sentences from tT and The semantic successor r w of r with respect to 0 and i s the set of signed sentences +B,B a sentence from "b and f o r which 5 one of the following conditions i s s a t i s f i e d : (1) +B,respectively,is i n I . (2) B i s C & D and each of +C and +DRespectively, one of -C or -D i s i n P . (3) B i s C V D and one of +C or +DRespectively, each of -C anl -D i s i n 1* . (4) B i s ^  C and -C,respectively +C,is i n f . (5) B i s C-^ D and one of -C or +D, respectively, each 3>f +C and -D, i s i n I1 . (6) B i s 3 xC(x) and f o r some a i n O +C(a) i s i n 1 , re s p e c t i v e l y , f o r a i l a i n -C(a) i s i n f . (If B i s tfxC(x) and f o r a l ! a in£ +e(a) i s ij , r e s p e c t i v e l y , f o r some a i n S -C(a) i s i n f . DEP. 2 - Semantic completion of a set T of signed sentences i s the . i j p(n) , H( 0) p , , MCn+l) set I = v£ I where I = and f o r each n<*N J i s the se-TS fn) mantic successor of ) THEOREM 1 - I f P i s any consistent set M signed sentences then f * i s consistent. Theproof i s immediate-and consists i n proving "by induction that f o r each nfN i s consistent. SEE»t3 — A set > of signed atomic sentences from o and i s com-plete i f f o r each A in*3) and f o r each a in cTeither +A(a) or -A(a) is in f*. 6 DEP. 4 - A c l a s s i c a l model f o r cf and 5) i s any consistent and com-plete set of atomic sentences from % and ^ Z) y. I f f i s a c l a s s i c a l model f o r S' and 5), i t s semantic completion i s consistent and complete with respect to the set of a l l the 'Isen-tences from £ and *2) . I t i s of course a tru t h set as defined f o r example hy Smullyan ^13] > where he uses the prefixes T and F instead of our + and - respe c t i v e l y . However t h i s d e f i n i t i o n of t r u t h set does not depend upon a p r i o r d e f i n i t i o n of the degree of a formula. DEF. 5 - A sentence +B from o' and i s c l a s s i c a l l y v a l i d i n the model r f o r $ and © i f +B e f ,respectively. DEF. 6 - A sentence +B i s c l a s s i c a l l y v a l i d f o r any o containing a l l the names i n B, f o r any 2) containing a l l the atomic predica-tes i n B and f o r each c l a s s i c a l model f f o r % and ,respective-i y In order to be able to define i n t u i t i o n i s t i c models we must f i r s t state a few d e f i n i t i o n s . DEF. 7- A tree with o r i g i n p 0 i s a t r i p l e (T,p 0,S) where: T i s a set ,p0£T and S i s an i r r e f l e x i v e r e l a t i o n on T such that: (1) there i s no q i n T such that qSp 0. (2) For each q i n T there i s one and only one p i n T such that pSq. (3) For each q i n 33 p 0S'q 7 (For any p,q i n T pS'q i f and only i f pS nq f o r some neN, where n pS q i f and only i f p=q and f o r each n>0 pS q i f and only i f there i s an r i n T such t h a t p S n and rSq.) Let (T,p 0,S) he a t r e e , pa and q elements of T. I f pSq we say t h a t p i s the immediate predecessor of q or q i s an immediate successor of p. I f pS'q we say t h a t p i s a predecessor of q or q i s a successor of p. Any q i n T having no successor i s c a l l e d an endpoint. DEP. 8 - A t r e e (T,p 6,S) i s f i n i t a r y i f f o r each p i n T the set •i of the immediate successors of p i s f i n i t e . DEF.9 - Let £T,p0,S) be a t r e e . Eor each q i n T a path P through q i s any maximal sequence q^, » • • • »tin» • • • of elements of T such t h a t q =p„ f o r a l l ieN q.Sq. _ , „ . , H l 0 l l + l and f o r some i n t e g e r j q.=q. I f P i s a path through q we a l s o say t h a t q i s i n P. The f i r s t to in t r o d u c e a c l a s s of models f o r i n t u i t i o n i s t i c p r e d i c a t e c a l c u l u s was E.W. Beth ^2J i n 1956. DEF. 10 - An i n t u i t i o n i s t i c Beth model f o r g i v e n S and JD , ab-b r e v i a t e d a B.-model,is a quadruple (T,p0,S,7^) where (T,p 0,S) i s a f i n i t a r y t r e e and iy i s a mapping from T to the set of a l l c l a s -s i c a l models f o r o and such t h a t : (1) f o r a l l p,q i n T +A(a)6rj^(p) and pSq :==>+A(a)£i^(q) 8 ( 2 ) f o r each p i n T , i f f o r each path P through p there i s a q i n P such that +A(a) 6, (q) then +A(a) e ^ (p)» DEP 11- Let (T, p p , ^ )fe B-model f o r b and ® , By analogy with the c l a s s i c a l case, we define the sequence \ > \ , • <'' \ > '' ' of functions i n T i n the following way: V ' ( P ) = ^ ( P ) f o r e& c n p i n T . Having defined , then f o r each p i n I 1^ (p) i s the set of signed sentences +_ B, B a sentence from % and tD , f o r which one of the foll o w i n g conditions i s s a t i s f i e d . to (1) +B, re s p e c t i v e l y , i s i n (p). ( 2 ) B i s C & D and each of +C and +D, respectively,one of -C or -D, i s m (p). (3) B i s C V D and f o r each path P trough p there i s a q i n P such that +C or +© i s i n (q), r e s p e c t i v e l y , f o r some path P trough p and f o r a l l q i n P each of -C and -D i s i n (q). C4)B i s ~" C and f o r each q i n T such that pS'q , -C i s i n i^ Cq.)» r e -spective l y , there i s a q i n T such that p S'q and +C i s i n \ K ) ( q ) . (5) B i s C ^ D and f o r each 'if i n T such that pS'q one of -C or +D i s i n T£ (q), r e s p e c t i v e l y there i s a q i n 1' such that pS'q and +B1 and —D are i n TI (q). (6) B i s 3xC(x) and f o r each path P -trough p, there i s a q i n P such that +C(a) i s i n (q) f o r some a ^ S f respectively, there i s a path P trough p such that f o r a l l q i n P -G(a) i s i n T£ (q) f o r a l l a fc- & » (7) B i s V xC(x) and 4©(a) i s i n ^ (p) f o r a l l a e £ , respectively 9 - G'(a) i s i n 'r^(p) f o r some a e *b . F i n a l l y l e t \^ "be such that f o r each p i n T Let (T, p 0 »S,ij) be a B-model. I t must be noticed that although f o r each p i n T the set i s c o n s i s t e n t , i t i s not i n general a t r u t h set. For example f o r some sentence B i t may contain both - B and ' B . I f + B 4 ^ ( p ) we also say that the point p forces + B respectively, re-l a t i v e to the model* DEF 12— A sentence + B i s v a l i d i n the model(T r p 0, S , ^ ) i f f o r each p i n T +B e 'nj(p) r e s p e c t i v e l y . DEF 13- A sentence + B i s i n t u i t i o n i s t i c a l l y v a l i d i f i t i s v a l i d i n any B-model f o r any set S containing a l l the names i n B and f o r any set % containing a l l the atomic predicates i n B . A B-model can be represented as a tree (T, p 0, S) with a set of sign-ed sentences l a b e l l i n g each of i t s nodbes. I t i s understood "by clauses (1) and (2) i n d e f i n i t i o n 10 of B-models that +A(a)e ^ ( P ) i f a n d only i f +A(a) appears as a l a b e l i n some predecessor of p, i n p i t s e l f , or appears as a l a b e l of some node of each branch trough p. Consider the fo l l o w i n g example with&= (al and 3i =?|A1 : - A ( a ) i f i i s even Here + A(a) i f i i s odd Therefore neither - A ( a ) nor + A(a) are v a l i d while f o r example the sentences - V X ^ A C X ) , + V x'v ~ A ( x ) are v a l i d i n t h i s model. Indeed - ^ A(a) e ^ ( p - ) f o r each i&N, because i f i i s odd then + A(a) i s i n ^ (p: ), i f i i s even then p.S*p.^ and + A(a) &. ^* ( p c + ( ) . Therefore - ^ x ~» A ( x ) and + ~" ~ A(a)' are both v a l i d , hence + V x ^ A ( i s v a l i d . THEOREM 2 - Let(T, p., S,^)be a B-model then f o r each p,q i n Tr +B ^ ^ (p) and pS • q => +B fe (q) -B £ ^* (q) and pS'q => -B e (p) The second proposition of the theorem i s an obvious consequence of the f i r s t i f we note that i f B i s a sentence of degree n, then f o r each p i n T either +B or -B i s i n i ^ C p ) . Therefore we have only to prove by induction that f o r each n<sF and f o r each p,q i n i 1 : 11 R e c a l l i n g close (1) i n d e f i n i t i o n 10 of B-models and the f a c t that pS'q i f and only i f pS q fo r some k&N the i m p l i c a t i o n i s e a s i l y seen to he true when n=0. Suppose i t holds f o r n., then we have 6 cases to consider according to the form of B to prove the i m p l i c a t i o n f o r n+1. B i s C & D +C & D £. ^ ^(p) —> +C 6- ^ '(p) and +B £• \' (p); by the induction i p o -thesys +Ct "^ '(o.) a n ^ +^ fc \°(q.) hence +C & D e '(q). A s i m i l a r proof applies when B i s VxC(x). B i s 3xC(x) + jxC(x)€. 1 ^ (p) => f o r each path P trough p there i s an s i n P such that +C(a)£ (s) f o r some a. e £ t In p a r t i c u l a r t h i s i s true f o r a l l successors of p i n p a r t i c u l a r f o r q hence +lfxC(x)t ^ ^ ( q ) . A s i m i l a r proof applies when B i s C V D , B i s + &\(v) ==> f o r each s i n T such that pS's -C & ( s ) , hence the same i s true f o r each successor of p and,because pS'q;+ a ^  (q). A s i m i l a r proof applies when B i s C^ >D As a consequence of t h i s theorem we have: +B i s v a l i d i n the B-model (T, p o , S, t i ) i f and only i f +B L **(p)» 12 THEOREM 3 - Let (T,p 0,S,^) be a B-model. Then f o r each p i n T, (p) i f and only i f fo: i s a q i n P such that +B6 'rj^Cq). +B i s i n <vj* o r each path P through p there One side of the i m p l i c a t i o n being t r i v i a l by theorem 2, we only have to show by: induction that f o r each p i n T, f o r each neN i f f o r any path P through p there i s a q i n P such that +Bcfn^ (q), then +B6i|n^ (p). The i m p l i c a t i o n i s true when n=0 by clause (2) i n d e f i n i t i o n 10 of B-model. Suppose i t holds f o r n .We give only some cases f o r n+1. B i s VxC(x) and f o r any path P through p there i s a q i n P such that + VxC(x) e, 1^*\q), hence f o r each a6cb, +C (a)& f ^ n ^ (q). Hence f o r each and f o r each path through p there i s a q i n the path such that + C ( a ) ^ n ^ ( q ) , hence by the induction hypothesis + C(a)fcr^ (P) f o r each a 6 , hence + VxC(x)67^ n + 1^ (p). B i s C V D and f o r each path P through p there i s a q i n P such that + C V D 6 ^ n + 1 ^ ( q ) ; then P i s also a path through q, hence there i s an r i n P such that one of +C or +D i s i n V\ ^  (r) .Hence by clause (3)' on d i s j u n c t i o n i n the d e f i n i t i o n of T\ n + 1 ^ ? + C V D • - (n+1), , U xs xn o^/ (p). B i s COD and f o r each path P through p there i s a q i n P such that +C DD i s i n 7 ^ n + " ^ ( q ) . In p a r t i c u l a r t h i s i s true f o r each r i n f such that pS'r. Hence either f o r each path B through r there i s an (n) s i n P such that +D i s i n WiK (s) and therefore by the induction hypothesis ( r ) , or t h i s i s not true. But then there must be some s such that rS's and -C 6 1 ^ ( s ) ; hence -C£ 0| ( r ) . 13 Hence +C ^> D fc (p) because f o r each r or -C ( r ) . The foll o w i n g lemma i s t r i v i a l . LEMMA - Let (T, p c , S,^) be a Be&odel that^«^ep&T ^(p)=T . Then the set of B-model coincides with T ( ry ) such that pS'r ei t h e r +D e. ^ ( r ) / and P a c l a s s i c a l model such v a l i d signed sentences i n the THEOREM 4 - Let (T, p 0 , S, r^) be a B-model f o r S and S> , such that f o r each A i n S> and f o r each a i n §~ eith e r +A(a) or -A(a) i s v a l i d . Then the set of sentences v a l i d i n the B-model i s a t r u t h set f o r o~" and 2) . Indeed l e t f be the c l a s s i c a l model such, t h a t ^ f o r each A i n 2) and f o r each a i n & +A(a) e. V i f jrA(a) i s v a l i d i n the B-model; r e -spec t i v e l y . Then f o r each p i n T (p)= F and the theorem follows from the lemma. In p a r t i c u l a r l e t (T, p o f S,*^ ) be a B-model f or S^and §D with only one path i n i t . Then f o r each A i n ^  and each a i n c\" i f +A(a) ^ ^ ( p 0 ) , then +A(a) i s v a l i d , i f - A ( a ) t ^ (p.) then -A(a) e ^ (p) f o r each p i n T. Indeed i f f o r some p i n T +A(a)er^(p) then +A(&)&t^ (pj by con-d i t i o n (2) i n d e f i n i t i o n 10 of B-model, because there i s only one path P trough po and of course peP . Therefore branching i s a necessary condition i n order to have a B-model not equivalent to a c l a s s i c a l model. 14 We prefer at t h i s point to define another class of models f o r the i n -t u i t i o n i s t i c predicate calculus which has been introduced by S.A.Eripke [l2] i n 1965. We w i l l then be able to discuss both models at the same time . DEF 13 - An i n t u i t i o n i s t i c Eripke model f o r ^ a n d "3D , abbreviated K-model , i s a t r i p l e (E, r , <£> ) where : K i s a non empty set R a r e f l e x i v e and t r a n s i t i v e r e l a t i o n on E a mapping from K such that f o r each p, q i n K (.1) £ (p) i s a c l a s s i c a l model f o r £' and "3) t S S: & ( 2 ) For each A inS) and f o r each a i n 'b x +A(a) € J (p) and pSq=^ +A(a)e dS(q). -A(a) £ (p) and pRq => either -A(a) or +ft(a) i s i n (q) DEF 14 - Let f be a set of (signed) sentences. We say that the (signed) sentence (+)B i s from f i f each name and atomic predicate l e t t e r used i n B- appears i n some sentence of T . DEF 15 - Let (E, R, § ) be a K-model. We want to define by induction T C O ) (.1) a sequence of functions on K, <3 ,<$,..., (P , .. - such that f o r each neN and f o r each p i n E <£> (p) contains only signed sentences from $ (p). Let f o r a l l p i n K $ (p)= $ (p). Having defined <P such that f o r each p i n K V (p) contains only signed sentences from (p), then f i s defined i n the following way. ICK+I) For each p i n E <p (p) i s the set of signed sentences +B, B a senten-15 ce from <fy (p), f o r which one of the following conditions holds:. (1) +B e, }(p), respectively ( 2 ) ' B i s C & D and each of +C and +D al^e i n <£W(p), respectively, one of -C or -D i s i n (p). (3) B i s C M D and one of +C or +D i s i n d) (p), respectively, both TOC) L ' -C and -D are i n Y ( P ) • t ( K ) (4) B i s rj C and f o r each q i n K such that pRq;-C i s i n (q) , r e -spectively^there i s a q i n K such that pRq and +G i s i n <p (q) (5) B i s C 3D and f o r each q i n K such that pRq one of -C or +D i s i n q> (q), respectively, there i s a q i n K such that pRq and each of +C and -D are i n <£ (q) T0<) (6) B i s ixC'(x) and +C(a) i s i n £ (P) forsome sentence C(a) from & (p), r e s p e c t i v e l y , f o r a l l sentences C(a) from (D (p) -C(a) i s m <p (p) (7) B i s \/xC (x) and f o r a l l q such that pRq and f o r a l l sentences K C(a) from ^ (q) +C(a) i s i n ^ (q), respectively, there i s a q i n E such that pRq and f o r some sentence C(a) from ^ (q) -C(a) i s i n f\q.) F i n a l l y l e t f o r each p i n K <£> (p) = w S (p). With t h i s d e f i n i t i o n , f o r each p i n K (p) contains one and only one of +B and -B f o r each sentence B from <j) (p). DEF 16 - A sentence +B i s v a l i d i n a K-model (K y R, f> ) i f f o r each p i n K such that +B i s from £ (p), +B t (p) respe c t i v e l y . 16 DEF 17- A sentence + B i s v a l i d i f i t i s v a l i d i n a l l K-models. DEF 18 - A K-model (K, R, |) ) i s a countermodel f o r the sentence + B i f there i s a p i n K such that T B e |>* (p) res p e c t i v e l y . THEOREM 5 - For each K-model (K, R, £ ) there i s a K-model (K,R, $ ) where R i s a p a r t i a l order r e l a t i o n and f o r each p i n K there i s a p i n K such that f o r any sentence B Y + B €. § (p) i f and only i f + B e $> (p) res p e c t i v e l y . Let (K, R, $ ) he a K-model f o r $ and . From condition (2) i n d e f i -n i t i o n 13, we have that f o r each p,q i n K i f <£> (p) i s a c l a s s i c a l model f o r S and 3) and <|> (q) a c l a s s i c a l model f o r "cS" and and pRq then S i S" and i f +A(a) t |> (p) then +A(a)6^>(q). I f therefore we also have qRp then 6^fS"and + A(a)€.^(p) i f and only i f + ACa)<s£ Cq) hence (p) = <£> (q). Moreover pRq and qRp => ±B e$>(p) i f and only i f £Be<j?\q) r e s p e c t i v e l y . Indeed the two sets: | r / pRrJ and qRsj are equal from the t r a n s i -t i v i t y of R; and by d e f i n i t i o n 15 f o r each p i n K the sign of a sentence i n |> (p) depends only on p and i t s successors. Let therefore f o r each K-model (K,R, and f o r each p i n K, p be the set: ^ g/ pRq and qRpJ , and consider the model (K rR, ^  ) where: K = [ p / VeKJ For each p,q i n K pRq i f and only i f pRq £ (p) = $ (p) f o r each p i n K. This model i s equivalent to the model (K,R,^), i . e . f o r each p i n Kj+Be$*Cp) i f and only i f +B e ^  (p) r e s p e c t i v e l y . 17 But now R i s r e f l e x i v e , t r a n s i t i v e and asymmetric i . e . a p a r t i a l order. From now on we w i l l r e s t r i c t ourselves to K-model (K,R, | ) where R i s a p a r t i a l order. The analogue of theorem 2 f o r B^-models holds f o r K-models as i t i s easy to v e r i f y . Theorem 6 - In any K-model (K,R,<j>), f o r each p rqi i n K: +\B d J)*(p) and pRq. ==> +B a $*(q.) However the second statement of theorem 2 does not hold f o r K-models, due to the f a c t that the c l a s s i c a l models defined "by £ have not i n general the same domain. We give an ; example of a K—model. + ft(0 - A H ) • + ft w > -fU<0 E X A M P L E : 2 From the example i t i s clear that 2> = [ A ] , £ - 1 , 2 , 3 / , . . . V ,p. Bp i f and only i f j } i and + A(n) e£ (p ) i f and only i f + A ( n ) e f (p) k £ j 18 Hence f o r example: <j Cp 4) = j * A ( l ) , +-A(2), - A ( 3 ) } f Cp5 ) = {+A( l ) , + A ( 2 > r + A O ) J etc. Both - v'xACx) and + \/x ~ ^A(x) are v a l i d i n the model. Indeed - VxA(x) 6^*(p- ) f o r each ifcTT "because f o r each i<s-N there i s a j * i such that -A(n) ^  |?*(Pj ) f o r some n. Suppose that f o r some is-N - \/x <~ ~ A(x) 6 Cpu) then there i s a j ^ - i such that f o r some n - ~ ~ A(a) e fy* C P T ) ,hence there i s a k^-j such that +~'A(n}fc £ ( P K ) which i s impossible. Hence +>V* x ~ ~ A(x) & ^ *(.p;) f o r each i<sN. ori-qHp I t must be noticed that t h i s model has only one branch, i . e . pRqV~ f o r each p and q i n K but, unlike the B-models, i t s v a l i d sentences do not constitute a t r u t h set. However, as with the B—models, the K-models confein c l a s s i c a l models as p a r t i c u l a r cases. Indeed f o r any K-model (K,R, \ ) where f o r each p,q i n K $(p)=£>(q), the set of v a l i d sentences i s a t r u t h set. Moreover i t must be noticed that branching i s s t i l l a necessary condition f o r completeness of i n t u i t i o n i s t i c ; l o g i c i n the K-models. For example the sentence C =~~(B V D) 3 (~"^ B V 'Dj i g not i n t u i t i o n i s t i e a l l y pro^able y but +>C" i s v a l i d i n any K-model (K,R, where f o r each p,q i n K either pRq or qRp. Indeed l e t (K,R,^ ) be a model having t h i s property and l e t p i n K such that + ~ ^(B V D)^ $*(p), then f o r each q i n K such that pRq, - ~/(B V D)e|>*(q) therefore there i s an s i n K such that pRs and +B V D e $ * ( s ) ; then either +B or +D are i n * (s).. 1§ Suppose +B e (a) , then + ~ ^  B & <| (p) • I f indeed - ~ ^ B t | " ( , p ) then f o r some r i n K such that pRr + ^ B i s i n $ * ( r ) . But now either rHs or s R r r i n any case one of r or s should force "both + ~B and +B by theorem 6* But then f o r each p i n K i f + ^ ^(B V D)fc f*(p) we have that + (~ ^  B V~^D} i s i n |* (p), hence + ~ ^ (B V D) => ( B V ~ i s v a l i d . The following i s a counter-model f o r ~ ~> (A(l) V k{2)) => ( ~ ^ A(l> V—A(2>) I t i s easy to c&eck that + ~ ^ (A ( 1 ) V A(.2)) fc^*(p,) although ACl) V ~ - ^ A(2)) fc §*Cp, K We close t h i s section with a l a s t d e f i n i t i o n . DEP. 19 — Let f be a set of unsigned sentences , B'» be any sentence. Then I* t B i f B i s proof t h e o r e t i c a l l y deducible from V i n c l a s s i c a l predicate calculus. I-J- B 1 i f B i s proof t h e o r e t i c a l l y deducible from P i n the i n t u i t i o n i s t i c predicate calculus as formalized f o r example by Kleene [ l l j . 20 B i f +B i s v a l i d i n any c l a s s i c a l model f o r which +D i s v a l i d f o r each D i n T . ^ >=. B i f +B i s v a l i d i n any i n t u i t i o n i s t i c model f o r which +D i s v a l i d f o r each D i n f , 21 S E C T I O N 2 Models f o r s e n t e n t i a l calculus DEP. 1 - A p r o p o s i t i o n a l l y atomic sentence i s any sentence of the form VxC(x) or 3xC(x) without names i n i t . Let r "be any c l a s s i c a l model, then f o r any p r o p o s i t i o n a l l y atomic _ . _ _ Let ^ = | A . ) ,A^  ,A3 ,... j Be the c o l l e c t i o n of a l l such sentences. We can consider them as atomic propositions whose inner structure we do not want to analyze further. Any sentence b u i l d up from these using the pr o p o s i t i o n a l connectives w i l l s t i l l be i n T* , f o r each c l a s s i c a l model V , i t s sign depending upon the corresponding rules f o r p r o p o s i t i o n a l connectives* Accordingly : DEF 2 - A c l a s s i c a l model I f o r a set of atomic sentences, i s any complete and consistent set of signed atomic sentences from 3V w are then determined by the corresponding clauses for the p r o p o s i t i o n a l connectives* K-models and B-models f o r s e n t e n t i a l calculus are defined accordingly, DEF 3- A K-model f o r a c o l l e c t i o n 0 f atomic sentences i s a t r i p l e (K,R,<§) where K i s a non empty set, R a p a r t i a l order r e l a t i o n on K and | i s a function with domain K such thfffc f o r each pjq i n K, f o r each A i n (1) $(f)is a c l a s s i c a l model f o r S3 . (2) I f +A i s i n ^ (p) and pRq then +A' i s i n <j? (q) . 22 T O O For each ndN, f o r each p i n K the signed sentences i n cp (p) are determined by r u l e s (1) - (5) i n d e f i n i t i o n 1 - 15. DEF. 4- A B-model f o r i s a quadruple (T,po,S,<^) where (T,p 0,S) i s a f i n i t a r y tree and ^ i s a function whose range i s T and f o r each p,q i n T. and f o r each A i n 3D t (1) ^ ( P ) -*-s a c l a s s i c a l model f o r '2) . ( 2 ) I f + A i s i n or^ (p) and pS»q then + A i s i n ^ ( q ) . (3) I f f o r a l l paths P through p , there i s a q i n B such that + A i s i n t\ (q) then +A i s i n ^ (p). Again f o r each neN, f o r each p i n P the signed sentences i n ^ ( P ) are determined by r u l e s (1) to (5) i n d e f i n i t i o n 1 - 10. Henceforth i n t h i s section the word model must be understood as model f o r sententi a l calculus. We see that i n the s e n t e n t i a l calculus i f (T,p„,S,^ ) i s a B-model f o r and (K,R, <£> ) i s a K-model f o r *2) , then both Vi and £ have the same range : c l a s s i c a l models f o r aJ , DEF. 5- A strong B-model f o r i s a B-model (T,p 0 ,S, f o r S)' such that f o r each p. i n T and f o r any d i s j u n c t i o n B' V C from 3) , +B V C i s i n vy^ (p.) i f and only i f one of +B or +C i s i n ^ (p). Strong B-models are also K—models and consequently the class of strong B-models i s the i n t e r s e c t i o n of the two classes of i n t u i t i o n _ i s t i c models. Let K be a set, p an element of K , R a r e f l e x i v e and t r a n s i t i v e r e l a t i o n on K, and consider the t r i p l e (K,p,S) where : 23 •K i s the set of a l l the f i n i t e sequences , pt , ... , p^ of elements of K where P0 =p and p Rp^ . f o r each i , n^i^-O. p i s the sequence whose only term i s p S i s the i r r e f l e x i v e r e l a t i o n on K such that qSr i f and only i f ^ q i s the sequence obtained from the sequence r by deleting, i t s l a s t element. Then the t r i p l e (K,p,S) i s a tree and^K i s f i n i t e (K,p,S) i s a f i n i t a r y t r e e . F i t t i n g i n [5] shows how to construct ' f o r any sentence B such that B a counter-model (K,R, f o r +B where the set K i s f i n i t e . Therefore i f ^ B then there i s a K-mod.el (K,R, f ) with K f i n i t e such that f o r some p i n K , - B i s i n <j> (p). In correspondence to K, R and p consider the t r i p l e (K,p,S), then (K,p,S) i s a f i n i t a r y tree. Let f o r each q i n K, l ( q ) "be the l a s t element i n the sequence q and define i n K the function such that f o r each q i n K : <^ (.q) = $ ( l Q ) lemma 1- (K,p,S, i s a B-model, Property (1) i n d e f i n i t i o n 4 i s obviously s a t i s f i e d . Moreover f o r each q,r i n K i f +A i s i n ^ Cq) then +A i s i n ^ ( l ( q j ) and i f qS'r then l ( q ) i s an element of the sequence H*, hence l ( q ) R l ( r ) i n K, hence +A1 i s i n <j> (l(r>) = ^ ( r ) F i n a l l y suppose that f o r each path P>through q, there i s an r i n P such that +A i s i n ^ ( r ) . In p a r t i c u l a r t h i s i s then true f o r the path P = P U P, where P. i s the semi-path from p to q and P. i s the sequence of elements of K: q , q ..., q t ... where f o r each n q i s the sequence obtained from q by adding to i t n times l ( q ) . 24 Therefore f o r some r i n P +A i s i n ^ ( r ) . I f r i s i n P4 t h e n r S ' q and +A i s i n ^ ( q ) . I f r i s i n P^ then +A i s i n ^ ( r ) = ^ = = $ ( l ( q ) ) = Moreover i t i s easy to show, see also Kripke ^12j, that f o r each q i n K +C i s i n i^(q) i f and only i f +C i s i n £ ( l ( q ) ) r e s p e c t i v e l y . But then (K,p,S,o^ ) i s a strong B-model and "because -B i s i n 1^ (p) then -B i s i n (p). Hence: THEOREM 1 — The s e n t e n t i a l i n t u i t i o n i s t i c calculus i s complete wi t h respect to the class of strong B-models. Theorem 1 shows that i n the s e n t e n t i a l case the close on tt&disjunction i n the d e f i n i t i o n of a B-model appeaxis to be i n e s s e n t i a l * but we w i l l return to t h i s point i n section 3* In the f o l l o w i n g of t h i s section the quadruple (T, p o , S, vy) w i l l denote a strong B-models The strong B-models are e s s e n t i a l l y those described i n Grzegorczyk ^Yj and j^ 8j , where he points out an i n t e r e s t i n g p h i l o s o p h i c a l i n t e r p r e t a t i o n of them. Any model (T,p o,S, Y^) from a set £D of atomic sentences can be interpreted as an experimental i n v e s t i g a t i o n where the experimental data are the elements of 9)', p 0 represents our actual "state of knowledge" and the elemnts of T future possible states of knowledge. The r e l a t i o n S r w i l l then express temporal succession. The clause that + A £ T ^ ( P ) and pB'q implies +Ae^ (q), simplymeans that once we have e s t a b i l i s h e d A i n our research, we w i l l not r e j e c t 25 i t i n the future, or i n other words we do not forget. Complex sentences are not established "by experiments but by reasoning;. This applies also to negations and i n p a r t i c u l a r to negated atomic sentences, the f i r s t important difference with the c l a s s i c a l case. According to Grzegor&zyk the i n t u i t i o n i s t i c s e n t e n t i a l calculus can be seen as the calculus of strong assertions. A strong assertion has the form: " i n the actual state of knowledge the sentence B must be asserted". We i n t e r p r e t +Bt ^ ( P ) a s 11B 1 3 strongly asserted i n p". Accordingly I must assert the sentence i f and only i f I am sure that never i n the future I w i l l have to assert B» This explains the cloJ3e f o r negation* The same applies f o r i m p l i c a t i o n : I must assert B P C i f and only i f I am sure that I w i l l never f i n d a counter example, that i s i f I can exclude a future s i t u a t i o n i n which I am forced to assert B without being forced to assert C Aniof course I must assert B & C (B Y C) i f and only i f I must assert both of them (I must assert B or I must assert C). Therefore the set of sentences i n t u i t i o n i s t i c a l l y val i d i s according to t h i s i n t e r p r e t a t i o n the set of sentences which must be asserted i n any moment i n any research. Very often however s c i e n t i s t s make hypothesis or weak assertions. having the form: "at the present state of knowledge the sentence B can be admitted n or more weakly "B cannot be rejected". We give the following i n t e r p r e t a t i o n of weak assertions. In any state of knowledge p, either +-B i s i n ^ ( p ) or + ~ ~B i s i n i^Cp ) or both - and -VB are i n ^ ( p ). In the f i r s t case i s strongly asserted hence weakly asserted and B must be r e j e c t e d , 26 i n the second case <~>B must he rejected and B i s weakly asserted, although -B could be i n T ^ ( P ) . F i n a l l y when - *^^B and - ^ B are both i n T ^ C P ) ; then no information i s available, about B, hence both B and^B cannot be rejected and both are weakly asserted i n p. According to t h i s i n t e r p r e t a t i o n the set of sentences weakly admitted i n p canbe contradiptecT_ ' but: THEOREM 2 - The set of sentences c l a s s i c a l l y v a l i d i s the set of sentences which are weakly admitted i n any "state of knowledge". Indeed i f B is; not c l a s s i c a l l y v a l i d , then there i s a c l a s s i c a l model, hence an i n t u i t i o n i s t i c model (T,po , S , «^) where ~>B i s v a l i d , hence f o r each p i n T,B must be rejected and cannot be weakly asserted. I f B i s c l a s s i c a l l y v a l i d then V^ -B, but then ~^ ~~B (for a semantical proof of t h i s statement see theorem 5 of t h i s section). Hence B i s i n t u i t i o n i s t i c a l l y v a l i d , and B i s always weakly asserted* This i n t e r p r e t a t i o n strongly suggests that i n any r fstate of knowledge" the set of sentences strongly asserted i s c l a s s i c a l l y s a t i s f i a b l e . We can easly prove i t as a consequence of the following observations. DEF. 6 - A path P i n a model (Tjp^ » S , ^ ) from2>'is saturated i f f o r any sentence B from 2} there i s a p i n P such that e i t h e r +B or + ~"B i s i n (p). P i s atomically saturated i s f o r any element A i n SD'there i s a p i n P such that either +A or + i s i n (p). Here i s an example of a model with a path which i s not saturated: 27 E X A M P L E 3 Neither + A nor + ^ A i s ever forced along the i n f i n i t e path of the model. DEP.. 7 - Por each integer n, f o r each path P i n a model (T,po,S,>^) l e t 3^ he the set such that: +B i s i n £ i f and only i f f o r some, p i n P +B i s i n (p) —B i s i n c5^  i f and only i f f o r some p i n P +<^ B i s i n ^ ( P ) THEOREM 3 - Let (.Ttpo ,S,^) he a model andttee P a path i n the tree. Then P i s saturated i f and only i f P i s atomically saturated and i L i s a t r u t h set-. Of course P saturated implies P atomically saturated and i t i s e a s i l y seen that S^, s a t i s f i e s a l l the conditions i n the d e f i n i t i o n of a t r u t h set f o r se n t e n t i a l calculus as given by Smullyan jjL3j. Suppose that P i s atomically saturated, and l e t us prove that f o r each integer n and f o r any sentence B of degree n, eith e r +B or -B i s i n The i m p l i c a t i o n i s true by hypothesis when n = 0. Suppose i t i s true f o r n, then i n order to show i t i s true f o r n+1, we have to consider four d i f f e r e n t cases: 28 B i s C & D I f both +C and +D are i n then there are elements p and q i n P such that *C i s i n or^ (p) and +D i s i n ^ (q)' and ei t h e r pS rq or qS'p, hence f o r same s i n P both +C" and +D are i n -r^ °Cs)» then +C & D i s i n C&)1 hence i n e)p „ I f , f o r example -C i s i n , then f o r some p i n P + <-^C i s i n </n+i) too ^ (p), hence f o r each s i n T such that pS's -C i s i n (s) hence -C & D i s i n ^ ( s ) , hence + ^ (C & D) i s i n (p) and therefore -(C & D) i s i n sf^ . B i s C'TD . The proof i s similar- to the previous case. B i s rJ c J? C'"-H"V I f -C" i s i n then f o r some q i n P + i s i n ^ (q) hence + ~C i s i n leefr ; i f instead +C i s i n <=d^> then f o r some q i n P +C i s i n ^ Cq) hence +• C i s i n ^  (q) hence - MT i s i n » B i s C 3 D i f -C or +D i s i n c ) f then f o r some q i n F either + <^ C i s i n ^  (q) or +D i s i n /y^ Cq); i n any case +C >D i s i n ^ (q) hence i n I f both +C and —D are i n o f p , then there are p,q i n P such that +C i s i n 'h'^ Cp) and + ^/D i s i n ^ ^ ( q ) and pS'q or qS'p. Hence f o r some s i n P both +C and are i n on ( s ) , hence f o r each r i n T such that s S r r -(C 3D) i s i n (r) , hence * ^ (C-s D) i s i n (S) and -(C r>D) i s i n I m p l i c i t e l y we have also proved that cf^ i s a t r u t h set . 29 THEOREM 4 - Let (Tjp^ rS, t\) be any model from ^  then f o r each p i n T the set (p) = - | B / +B €. ^ ( P ) ^ i-s c l a s s i c a l l y s a t i s f i a b l e . Let A ,A.,... an enumeration of the elements of.sJ and consider the fol l o w i n g sequence of elements of T: q^ T q( , q^, ...where q = paand f o r each n^-0 q i s obtained as follows.: i f +-/A^  i s i n n (q J l e t q = q ; i f -^A^ i s i n ^  (q ) then f o r some s i n T q S's and +A i s i n n ( s ) , then l e t q = s. l e t P the path through q ,q ,...,q P i s atomically saturated hence i s a t r u t h set, but ^ (p)<jF-=^ , hence i t i s c l a s s i c a l l y s a t i s f i a b l e . For paths P whicW are not saturated the set cfp i s not a t r u t h set and not necessarily an Hintikka set ( Smullyan \JL3j ). Indeed i n example 3, i f P i s the i n f i n i t e path - ^ A i s i n but +-A i s not i n . Of course the set i s s t i l l c l a s s i c a l l y s a t i s f i a b l e because each f i n i t e subset of <^ ,being forced by some q i n P i s c l a s s i c a l l y s a t i s f i a b l e . Let A be any set of sentences, l e t A. denote the set of a l l the sentences of A- precedeed by double negation . We w i l l now prove semantically the following proof t h e o r e t i c a l r e s u l t , see f o r example Kleene ^ l l j : THEOREM 5 - I f B then ~^A^-~~B. Suppose and ~ ^ A ~ ^B,then there i s a model (T,p^,S,/>|) and a p i n T such that f o r any C i n A + ~~-C i s i n ^  (p) and B i s i n m£ (p) ; then there i s some q i n T such that pS'q and + ~"^C i s 30 i n ^ (q) f ov(> a l l C i n A while +a /B' i s i n ^ ( q ) * Let us consider any complete chain P trough q, then the t r u t h set cJ'j> s a t i s f i e s ~^.A and ^B, a contraddiction. Prom the proof of theorem 5, i t i s e a s i l y seen that the foll o w i n g stronger r e s u l t holds: COROLLARY - I f A V 3-B then A'v^-'^B where Ax i s any set of sentences c l a s s i c a l l y equivalent to A . Using strong B-models a t r i v i a l proof can be given of the w e l l known property of i n t u i t i o n i s t i c s e n t e n t i a l calculus. THEOREM 6 - I f I — B V C then t — B or \—C. x x x JEet indeed B V C be a v a l i d sentence and suppose neither B nor C i s v a l i d . Then there are models (T^,p o,S (, /* ( ) and (Ti,qo,S_l,, t^J) such that -B i s i n 0 ^ (p 0) and -C i s i n ^  (q<>). Consider the model (T,s e ,S, n^) where: T = T'( U T^  U j^s,j Por each p,q i n T. pS'q i f and only i f pS( q or pS^q, moreover s^ Spo and s 0 S q 0 . Por each p i n T - ^  s 0 j ^ (p) = ^  (p) i f p i s i n T,, ^  (p) = \Jiv) i f p i s i n T^  and moreover +A i s i n ^ ( s 0 ) i f and only i f +A i s i n ^  (v0 ) and i n ^  (q 0 ). I t i s immediate that f o r a l l sentences D from SO' i f -D i s i n * (p^) or i n ^ (^o) then -D i s i n 0^ ( s 0 ) . 31 Therefore "both -B and -C are i n ^(s„) hence +B V C would not be v a l i d i n t h i s model. To be precise the model so constructed i s a K-model but not a B-model because i t f a i l s to s a t i s f y condition (3) on d i s j u n c t i o n i n d e f i n i t i o n 1-11. However i t can be transformed i n an equivalent strong B-model according to Lemma 1. 32 S E C T I O N 3 SIMPLIFIED INTUITIONISTIC MODELS C l a s s i c a l l y i n d e f i n i t i o n 1-1 of semantic: successor, the clauses (6) and (7) f o r the e x i s t e n t i a l and the universal q u a n t i f i e r do not d i f f e r from clauses (3) and (2) f o r d i s j u n c t i o n and conjunction r e s p e c t i v e l y . Sentences l i k e ^xC(x) and 3xC(x) are c l a s s i c a l l y interpreted simply as a conjunction or a d i s j u n c t i o n , although possibly i n f i n i t e . In section 2 we have seen that i n t u i t i o n i s t i c s e n t e n t i a l calculus i s complete with respect to a subclass common to the E—models and the B—models: the strong B-models. By analogy with the c l a s s i c a l case l e t us extend the strong B-ntodels to f i r s t order l o g i c by introducing clauses f o r the un i v e r s a l and the e x i s t e n t i a l q u a n t i f i e r , i n the d e f i n i t i o n of ^  , analogus to the clauses f o r conjunction and d i s j u n c t i o n r e s p e c t i v e l y . DEF* 1- A strong B-models f o r £ and *sb i s a quadruple (T.p 0,S,^> where (T,p 6,S) i s a tree a n d s a t i s f i e s c o n d i t i o n ( l ) and (2) i n d e f i n i t i o n 1-10 of B-models . For each keN and f o r each p i n f, ^ (p) i s defined as i n the B-models except that clauses (3) and (6) are replaced by the follo w i n g : C31) B i s C V "B and one of +(T or +D i s i n n (p), respectively. 00 L each of -C and -D are i n ^  Cp). 33 (6 , : ) Bi i s JxC'(x) and +CT(a) i s i n ir\ (p> f o r some a i n d , respectively^ each of -CT(a) i s i n ^ (p) f o r a l l a i n © . Kowever t h i s class of models i s not adequate f o r i n t u i t i o n i s t i c moJe-Jba-; Let indeed CT "be any sentence, B(x) be any formula contain_ ing only x f r e e and consider the sentence: D = V x(C Y B(x)) o (C Y V xB(x)) Then +D i s v a l i d i n any strong B-model, although D i s not i n t u i t i o n _ i s t i c a l l y provable. Let indeed(r«p , S , Y J ) "be a strong B-model f o r given S and c3l> and y ° * * suppose +VxCCT ¥; B'(x) }e "n^  (p) f o r some p i n T, then +<T V B(a)t o^(p) f o r each a i n $ ; hence eit h e r +C"e. t^CpJ or +B(a)fe (p) f o r each a i n £ ,therefore +C V V xB(x)£ ^ (p) and +D i s v a l i d i n the model. The clause (3) on d i s j u n c t i o n i n the d e f i n i t i o n of the B-models i s therefore e s s e n t i a l f o r f i r s t order i n t u i t i o n i s t i c fL'ogi© and cannot be substituted by clause (31) as i n the s e n t e n t i a l case. I t i s therefore c l e a r that the class of models f o r i n t u i t i o n i s t i c l o g i c must be larger than the class of strong B—models now described and i n order to give a counter model f o r +T>, i t must d i f f e r from these e i t h e r i n the clause r e l a t i v e to the u n i v e r s a l q u a n t i f i e r or i n the clause r e l a t i v e to d i s j u n c t i o n and consequently i n that r e l a t i v e to the e x i s t e n t i a l q u a n t i f i e r . The f i r s t way has- heen followed by Kripke, the second by Beth. This c l e a r l y explain, we think, the formal differences between the two classes of models. The strong B-models were f i r s t introduced by Grzegorezyk i n i n an equivalent form and i t has been proved, see f o r example S. Gornermann 34 In ^6 f that the f i r s t order calculus obtained by adding to the i n t u i t i o n i s t i c v 8 . 2 r i . O E S , the asiom schema D i s complete with respect to these models.. Is we did i n the se n t e n t i a l case, we w i l l now si m p l i f y both classes of models i n order to achieve a better understanding of t h e i r features. Let f 'any set of signed sentences and l e t T+ , r*_ f. be so defined: r + = ( + B / + B £ r j = ^ B / +-B £ f or -B € r j DEF. 3 - Let ^  be any non empty c o l l e c t i o n of sets of signed sentences from <Tand . £ n a t u r a l l y indaces on i t s e l f the fo l l o w i n g p a r t i a l order r e l a t i o n R: f o r each T , A i n ^ ,f*RA i f and only i f /}_£-A+and each name used i n some sentence of P i s also used i n some sentence of A . We also say-that R i s the p a r t i a l order r e l a t i o n associated with •€ DEF. 4 — l j e^^ be any non empty c o l l e c t i o n of sets of signed sentences from £ and2) and R i t s associated p a r t i a l order r e l a t i o n . The semantic successor of ^  > ^^ie c°ll e c" ti° n °f sets of signed sentences ^ = ( ? / ^ 6 %\ where f o r each T i n ^  i i s the set of signed sentences +B from Y such that one of the follo w i n g conditions holds: (1) +B" i s i n T , res p e c t i v e l y . ( 2 ) B i s C & D and each of +C and +D are i n T , r e s p e c t i v e l y , one of -C or -D i s i n T . 15 (3) B i s C V D and one of +C or +D i s i n T ,respectively, both -C' and -D are i n P . (4) B i s ~ C and f o r each A. i n J such that f RA -C i s i n A , res p e c t i v e l y , there i s a A i n ^  such that P R A and +C i s i n A . (5) B i s CD D and f o r each A i n | such that f R A one of -C or +3) i s i n A » re s p e c t i v e l y , there i s a A i n | such that f1 R A and each of +C and -D are i n A • (6) B i s ^ xC(x) and f o r some sentence C(a) from P , +C(a) i s i n V , re s p e c t i v e l y , f o r a l l sentences C(.a) from P -C(a) i s i n f . (7) B i s VxC(x) and f o r each A i n ^ . such that /*RA and f o r a l l the sentences C(a) from A , +C(a) i s i n A , re s p e c t i v e l y , there i s A i n such- that J* R A. and f o r some sentence C(a) from A , -C'Ca) i s i n A . DEP. 5 ~ A c o l l e c t i o n ^  of sets o^ signed sentences i s consistent, i f f o r each P i n £ , /* i s consistent. THEOREM 1 - I f ^  i s any consistent non empty c o l l e c t i o n of sets a (O of signed sentences then Jf i s consistent. I t i s immediate from the d e f i n i t i o n of semantic successor that i f i s inconsistent then there i s a f i n £ which i s inconsistent. THEOREM 2 - Let ^  be any non empty c o l l e c t i o n of sets of signed sentences and R the r e l a t i o n associated with i t , ^  i t s semantic successor, and R . the r e l a t i o n associated with i t . Then f o r each f , A i n ^ : p RA i f and only i f r(,)Rc'; Af'; 36 Because f o r each P i n ^ p £ ; F 0 ) and each sentence i n Pauses only names used i n P , i t remains to prove: f1 R A and +B"fe r°;=> +B €. A t 0 I f +B^r* then +BdA hence +BeA C 0 . Suppose +B€.(r^'-r); we give only some case: B i s C & D then both +C and +D are i n P and because I*+£ A + b o t h are i n A hence +C & D i s i n A . B i s then f o r each .TL such that F R Q -C i s i n n . ; but PR A and by the t r a n s i t i v i t y of R f o r each JQ. such that A RfL -C i s i n O- , hence + i s i n Ac'^  . B i s VxC(x) then f o r each SI. such that p R £L and f o r a l l sentences C'Ca) from H-+C(a) i s i n O-, hence again from T RA by the t r a n s i t i v i t y of R f o r each n. such that A R U and f o r a l l sentences C(a) from XI +C(a) i s i n I i - , hence + VxC(x) i s i n A 0 ) . DEF'.. 6 — Let ^  be any non empty c o l l e c t i o n of sets of signed sentences from ^ "and^ . The semantic compliteon o f i s the c o l l e c t i o n o ~rThJ d where < - v and f o r each neN i s the semantic successor o f ^ . DEF. 7 — A s i m p l i f i e d K-model, abbreviated s.K-model, f o r ^ a r i d S i s any c o l l e c t i o n ^ such that f o r each /I i n ^ } P i s a c l a s s i c a l model f o r 2) and a subset S~ of cT. The following theorem i s an obvious gen e r a l i z a t i o n of theorms 1 and 2 37 THEOREM 3 - Let ^ be any s. K-model and R the r e l a t i o n associated with i t . Then i t s semantic compliteon i s consistent and i f R i s i t s associated r e l a t i o n then, f o r each f , A i n ^  : f R A i f and only i f F*R*A* Therefore i f ^  i s a*,s. k-model we w i l l use R as the r e l a t i o n associated with ^  and by analogy with the c l a s s i c a l case we w i l l c a l l ^ A a t r u t h c o l l e c t i o n . Of course any s. K-model^ i s equivalent to the Kripke model ( ^  ,R,<£> ) where R i s the p a r t i a l order r e l a t i o n associated withjf and f o r each f i n J #f) = V . Moreover i t i s easy to show that f o r each K-model (K,R, (|> ), where K i s an enumerable set, there i s an equivalent s. K-model. The r e s t r i c t i o n to enumerable set i s i n - e s s e n t i a l because i n t u i t i o n i s t i c l o g i c i s complete ;'vdth;: .N respect to the class of K-models with an enumerable K. See f o r example the completeness proof i n Emitting £5^ . Let (K,R, $ J be a K-model f o r 3 ) and £~with an enumerable K; l e t p , Vti •••» V^i ••• be an emumeration of the elements of K, and (3 = |bj , b^, ..., b^, .. .J be a set of names equipotent to K and such that \> £ £ f o r each j i n N. Let f be a function from K to <Tsuch that f o r each p^ . i n K, f ( P j ) i s a name used i n (]D) . Then i f Pj^P^ f( p ) i s also a name used i n <t> (p- ). Por each p. i n K, i f cj) (p^ ) i s a c l a s s i c a l model f o r S' and 3D , & £ & l e t ^ be the subset of |3 such that: ^ = Pj.RPt-J a n d l e t f. be the set of signed atomic sentences ±A(c) from S V $• and such that: (1) ± A(cj) i s i n >^ (p^), r e s p e c t i v e l y . 38 ( 2 ) ± A ( G . ' ) , r e s p e c t i v e l y , i s i n ^ (P^)> where A ( . £ ' ) i s obtained from A(c) by s u b s t i t u t i n g each element b i n B. appearing i n £ with f ( P j ) . Then TL i s a c l a s s i c a l model f o r S'U ^ and (S'v fc) £ (h U^) . Moreover i f i ^  j then either V'JftVj ° r PjJ*Pc 5 1 1 ? P(/^Pj- ^ e n \ 1 S a name used i n P; but not i n P_ , i f p J?p. then b i s a name used i n )j but not i n ; i n any case i f i / j then J\_ ^  Tj . The c o l l e c t i o n ^ =| f. / i 6 ^ J i s then ans. K-model f o r § U j3 and 3 ) . THEOREM 4 - Let (K,R,«| ) be a K-model f o r S a n d S ) , with an enumerable K, and l e t £ be the corresponding s. K-model constructed, as above, with R as i t s associated r e l a t i o n . Then: (1) For each p. ,p^ _ i n K: p. Rp i f and only i f f- R fl (2) For any sentence B from a n d , l e t B' be the sentence from S and *£> obtained by s u b s t i t u t i n g each element b^ . of |3 i n B with f(Pj)» Then: For each ieN ±B € P* => tB'e (p-) We w i l l now prove statement (.1). Let ^ (p^ )°s. c l a s s i c a l model f o r ^  and 2) , £ 5" f and |) (Pj) he a c l a s s i c a l model f o r and Then Pt i s a c l a s s i c a l model from <^,^^ and J^ . a model from ^j-^fj» Suppose T^Fj then ( ^ O p - ^ C ^ l J ^ hence c, Moreover i f +A(c) i s i n & (p- ) then +A(c) i s i n Jj and f-RPr implies + A(c) i s i n J* , hence by d e f i n i t i o n of Jl_ +A(c) i s i n 0> ( p r ) . Therefore Jj R JJ. => pc Rpj. Suppose P ^ P j » "then S i 5j a n d |3. £ £>_ f o r the t r a n s i t i v i t y of R 39 because: £• = \ b / kfeN, p.Hp.V , 9T = )b /. M , p,Rp.l and p.Rp. Hence ( f ; U ^ C ^ O ^ ' ^ ^ ' J Moreover i f ' +A(c> i s i n f;, then +A(c_*} i s i n (p,) by d e f i n i t i o n , hence +A(c_r) i s i n <^> "because pJRp_., therefore +A(c_) e fj- , and T; R T_ . Having e s t a b l i s h e d the f i r s t statement of the theorem, _the second one i s an obvious consequence of i t . I t can be e a s i l y proved by induction that f o r each integer n and for e3)©h fc i n § , •> ±B£ l- L r=^±B'6 tp(p ±) The i m p l i c a t i o n i s true by d e f i n i t i o n when n= 0. We give only two cases i n proving the induction step. B i s <^ C and e >: tthen f o r each l _ such that \,- R U , -C i s Ij but then by the induction hypothesis and (1) -C i s i n i n  a) (p.) f o r egjjc-h p. i n K such that p.Rp.» hence +~'C i s i n p (p.) Suppose -wC i s i n J- , then there i s an element )_ of \t such that /.- R/r and +C i s i n i ; but then p.Rp. i n K and +Cr i s i n •jt>) J J 1 i d) ( p j by the induction hypothesis, hence - ^ C i s i n <P (p.) B i s \^xC(x) and + VxC(x) i s i n ^  \hence f o r each T i n ^ such that and f o r any sentence C(c) from V- , +C(c) i s i n J . In p a r t i c u l a r +C(a) i s i n >j f o r each a i n Oj , hence by (1) and by the induction hypothesis f o r each p i n K such that p..Rp. +(c»(a))is i n 0 (p.) f o r each a i n ^ T , therefore +(VxC»(x) i s i n (Pj^/* Suppose - VxC (x) i s i n J- , then f o r some Jj i n y such that and f o r some sentence C(c) from Jr , i s i n J .By (1) and by the induction hypothesis f o r s d -C(c) ome p. 40 such that p.Rp., - ( C ( c ) ) ' i s i n <p (p.) hence i n d> (p.) By theorem 4 and the the completeness theorem of i n t u i t i o n i s t i c l o g i c with respect to K—models , one can immediately conclude that the i n t u t i o n i s t i c l o g i c i s i n p a r t i c u l a r complete with respect to one subclass of the K-models. the s i m p l i f i e d K-models. I f indeed (K,R,^ ) i s a countermodel f o r the sentence ± B, then there i s a p .. i n K such that B i s i n fo* (p.) r e s p e c t i v e l y . But then , because i n t h i s case B* = B.+Bf'respectively must be i n the corresponding 1^  i n ^ and ^ i s a countermodel f o r ±B. With the s* K-models we have s i m p l i f i e d the notation by eli m i n a t i n g any reference to an external structure and reduced the concept of an i n t u i t i o n i s t i c model ^ to that of a c o l l e c t i o n of c l a s s i c a l models p a r t i a l l y ordered "by the r e l a t i o n defined i n d e f i n i t i o n 3» We w i l l now subject the B-models to a simple transformation i n order to bring out an important prop^erty of these models . DEP. 8 - A s i m p l i f i e d B-model i s a B-model (T.p ,S /*) where the o 'I fo l l o w i n g holds,; f o r each q i n T , i f q i s not an endpoint and p i s i t s immediate predecessor i n T then ^ Cp) / ^ C l K A s i m p l i f i e d B-model (T,p ,S,7i ) i s therefore one such that f o r 41 each p,q i n T , i f pSq then eit h e r q i s an endpoint or there i s an atomic sentence A(a) such that -A(a) i s i n O (p)< and +A(a) i s i n <|(qK In any theory i f the domain £f i s f i n i t e , then we can obviously r e s t r i c t ourselv"es to a f i n i t e £D too,because the set of r e l a t i o n s on 5 i s f i n i t e i f £ i s f i n i t e . Accordingly one important property of the s. B-models i s the following 5 LEMMA 1 - I f (T rp o,S,^) i s a s i m p l i f i e d B—model with & and 5) f i n i t e then the tree (T,po,S)' i s f i n i t e . The s. B-models are a subclass of the Beth models. In the next theorem we show how to construct f o r each Beth countermodel to a sentence irB, ans. B-model which i s a countermodel f o r ± B. Hence the i n t u i t i o n i s t i c l o g i c i s complete with respect to t h i s subclass of the B-models. THEOREM 5 - Let (T,p o,S f^)be a B-model f o r % and "5) and l e t A Q he an atomic unary predicate not i n ^ ) then there i s a sim-p l i f i e d B-model (T,p o,S,i^) f o r S and | A o ] * 0 n ^ h < 3 s a m e ' f c r e e structure (T,p , S j , such that f o r any sentence B from & and 5) and fo r each p i n Ts 1" B i s i n ^  (p) i f and only i f ±B i s i n (p). Let p , p n , p„, ... be an enumeration of the elments of T ,a ,a„,... o 1 2 o 1 42 be an enumeration of the elements of <b t then for each p.. i n T,, lr\ (p „) i s the c l a s s i c a l model f o r % and 3) O J A ^ J defined as fo l l o w s : f o r each A in ^ D and a i n £ i A ( a ) i s i n ^ ( P j ) ^ a n d o n l y ^ ± A(a), r e s p e c t i v e l y , i s i n ir\ (p.); f o r each a., i n b +A (a.) i s i n % (p.; i f and only i f p,S*p, -A (a.) 1 i s i n 4\ ( p . ) otherwise. I t i s immediate that (T,p^,S,^) i s a s i m p l i f i e d B-model f o r which theorem £ holds.. The reason we have introduced these models i s the f o l l o w i n g : i t i s w e l l known, see f o r example ^13 of Kleene ^ l l j , that i n t u i t i o n i s t s r e j e c t the excluded middle law only when dealing with i n f i n i t e domains. Por when the domain i s f i n i t e then there i s at l e a s t i n p r i n c i p l e a procedure to v e r i f y f o r each sentence B i f B or ^ B holds. Accordingly when dealing with f i n i t e domains there should be no difference between c l a s s i c a l and i n t u i t i o n i s t i c v a l i d sentences. This i s exactly what happens i n the s. B-models with a f i n i t e domain THEOREM 6 - Let ( T J P ^ J S , be any s. B-model f o r % and (2) ,where 5 and are f i n i t e . Then each sentence + B - c l a s s i c a l l y v a l i d i s v a l i d i n the model. Kleene i n j ^ l l j § ^9 gives a f o r m a l i z a t i o n of i n t u i t i o n i s t i c and 43 c l a s s i c a l l o g i c such that both have the same deduction r u l e s and c l a s s i c a l l o g i c i s obtained by i n t u i t i o n i s t i c l o g i c by adding one more axiom schema:-^ ^ B ^ B , which i s equivalent to the excluded middle la.w. Therefore i n order to prove the Theorem we have to show that i n any s. B-model (T,p j S , ^ ) with f i n i t e S and *3D, f o r any sentence B from o and 2) + ( ^ ^ B^B) i s i n m (p ). Suppose f o r some sentence B — ^ B ^ B ) i s i n ^ ( P ^ » then there i s a p i n T such that p^'p and both of + ^ ^B and -B are i n Tj^Cp). By theorem 3^-1, there must be a path P through p such that -B i s i n 'V^  (q) f o r each q i n P. By Lemma 1, beeause o and are f i n i t e . P i s f i n i t e r l e t r be i t s endpoint.. Then pS*r and by theorem 1—2, f w v / B i s i n ( r ) , hence - ^ B i s i n ( r ) , which implies that f o r s i n T such that rS's +B i s i n T ^ " ( S ) . But r i s an endpoint some \ hence +B i s i n /y\ (r) , a contradiction. Theorem 6 Soes not hold i n the K-models. Consider the following example: here f i n i t e but +(^ ^ A$a) o A (a)) i s not v a l i d . C l e a r l y t h i s difference comes from the d i f f e r e n t clauses i n the two models about dEs-junctive sentences. R e c a l l i n g the i n t e r p r e t a t i o n which has been given i n Section 2, 44 about these models, the difference could be explained i n the f o l l o w i n g way. In the s. B-models i t i s assumed that, being i n a given "state of knowledge", a f t e r a f i n i t e amount 6f time ei t h e r we w i l l jump i n a new state by e s t a b l i s h i n g a new atomic proposition or our research w i l l be terminated, i n which case the set of v a l i d sentences i s a t r u t h set; but the p o s s i b i l i t y i s admitted, i f the domain i s i n f i n i t e , , of continuing i n d e f i n i t e l y our research without never reaching an endpoint. In the s. K-models instead also i f the domain i s f i n i t e , one can progress from a given "state of knowledge" to another one, but may also remains stuck f o r ever without never being able to "complete" the set of established sentences. S E C T I O N Reduction theorems from c l a s s i c a l to i n t u i t i o n i s t i c l o g i c In t h i s section some other properties of i n t u i t i o n i s t i c models are discussed and the reduction theorems from c l a s s i c a l to i n t u i -t i o n i s t i c l o g i c , proof t h e o r e t i c a l l y demonstrated i n Kleene jJLl] £ 81, w i l l he proved now semantically. Por t h i s purpose we w i l l use the s i m p l i f i e d K—models of d e f i n i t i o n 7 — 3 throughout t h i s section, both f o r t h e i r simple notation and f o r t h e i r i n t e r e s t i n g i n t u i t i v e meaning. Because of the completeness of these models, no d i s t i n c t i o n w i l l be made between the notation A h—- B and A B. DEP. 1 - Let be an s. K-model for % and and R i t s asso-c i a t e i r e l a t i o n . Achain C i n j through V is any i n f i n i t e sequen-ce P^, P f n,... df elements of ^  such that:-P^ = ? , f o r each integer i P j ? and i f f o r some integers n and p V = V then there i s no A i n <f , A £ P > such that -P R 4 ' n+p 1 n a n 1 1 Of course i f a model v has an i n f i n i t e chain C where a r- 1 l + l for each i then the domain o i s i n f i n i t e . I n f i n i t e chains i n an s. K-model, l i k e the i n f i n i t e paths i n the B-models, represent the p o s s i b i l i t y of always acquiring new i n -formation without ever being able to reach an endpoint. Their pre-sence i n the modelaexpresses the constructive attit u d e towards 46 i n f i n i t y of i n t u i t i o n i s t s i n contrast to the ontologieal p o s i t i o n of the c l a s s i c a l mathematician. They therefore play a key role i n the f o l l o w i n g theorems. DEP. 2 - Fof any chain C i n an s.K-model, l e t cf "be the set of signsd sentences such that +B i s i n $ i f and only i f f o r some T . i n C, +B i s i n T ., -B i s i n i f and only i f f o r some f. 1 H * 1 c 1 i n C,+<*B i s i n I l DEF. 3 - Let C he any chain i n an s.K-model ~jj f o r & and C i s complete i f f o r each f ^ i n C and f o r each sentence B from f . either +B or -B i s i n C i s atomically complete i f f o r each 1 . i n C and f o r each atomic sentence A from f . either +A or -A i s i n of „. l C The analogue. - of theorem 4-2 does not hold i n f i r s t order l o g i c . Indeed i n example 2 of Section 1 the set of v a l i d sentences i s i t s e l f c l a s s i c a l l y u n s a t i s f i a b l e because both +^^xA(x) and + V x ~ ~ / A ( x ) are v a l i d . Of course any contrad a c t i o n disappears when q u a n t i f i e r s and connectives are interpreted i n t u i t i o n i s t i c a l l y . Indeed to assert t / x ^ ^ A ( x ) simply means that we have an e f f e c t i v e method such that, whenever an element a1 of the domain i s delivered to us, we can prove the absurdity of the absurdity of A(a),while to assert ^ ^xA(x) simply means that i t i s absurd that we can have a method to assert A(a) whenever an element a i s delivered to us. 47 DEF. 4 - Let ^  be any model and C any chain i n i t . C i s an cj -complete chain i f f o r any formula B(x) from ^ ? £ when +B(a) i s i n ^ f o r every name a i n ^  then + ^ xB(x) i s i n S , o o o Also theorem 3-2 i s not v a l i d i n f i r s t order l o g i c . Consider indeed the i n f i n i t e chain C i n the following: example 6 EXAMPLE 5 Then C i s atomically complete because +B(n) and -A(n) are i n <~f f o r each neN, but i t i s not complete because neither + 3xA(x) nor - l! xA(x) i s i n c f _ . C J? Moreover C i s w-incomplete because + ^ A ( n ) i s i n <=3 f o r a l l neN but + V x ^ A ( x ) i s not i n ^ n. + ^  V x rsyA(x) i s i n c^n» hence cf is< not c l a s s i c a l l y s a t i s f i a b l e . Only a weaker r e s u l t holds. r. THEOREM 1 - Let <f he any s.K-model and C aa y chain i t . I f C i s atomically complete and cJ-complete then C i s complete. Moreover s a t r u t h set. 48 We have to prove that f o r each integer n, f o r each sentence +B of degree n from some Y . i n Cj eith e r +B or -B i s i n ofn-The i m p l i c a t i o n i s true by hypothesis when n = 0. Suppose i t i s true f o r n and l e t us prove i t i s true f o r n+1. The p r o p o s i t i o n a l case are treated as i n theorem 3-2. B i s .3xD(x) and f o r some sentence D(a) from some Y. i n C, +D(a) i s i n c i c , hence +D(a) i s i n some P* and + 3xD(x) i s i n I . hence i n $ . Otherwise by the induction hypothesis -D(a) i s i n ^  f o r any Sentence D(a) from some ) . i n C. Because C i s GO-complete, then +Vx^D(x) i s i n ^ hence there i s a T . i n C such that + V x ^ D ( x ) i s i n r . , hence f o r each A i n 5 s u c n t n a _ f c and 3 . * A *" f o r each sentence D(aO from A +~,D(a) hence -D(a) i s i n A , wdch implies that -3xD(x) i s i n A * ; therefore +^3xD(x) i s i n hence -zixD(x) i s i n ^q* B i s VxD(x) and f o r each P i n C and f o r each sentence D(a) from T ., +D(a) i s i n ^  >hence, because C i s Q— complete + VxD (x) i s if i n <J . Otherwise by the induction hypthesis f o r some sentence D(a) from some J . i n G, -D(a) i s i n hence +'vyD(a) i s i n some I*-/ it X" ] i n C. Hence -D(a) i s i n A f o r each A such that P ^ R A ,hence - VxD(x) i s i n 4*> hence + ^  V xD(x) i s i n Y * and - VxD(x) i n cf , 3 0 THEOREM 2 - Let ^  be any s.K-model gor S" and S) , Y any element of , then-there i s a complete chain C through ^ . Let indeed ~B , B , B be an enumeration of a l l sentences and ^ and C = f P „ , . . . , / .... be a chain defined 0 1 ' 2 n 49 as follows: T 0 i s i n P . Assume \ , defined. Then l e t B , he the f i r s t sentence i n the n given enumeration such that: B , i s from | , a n d neither + B , H * K nit  k nor +^ B, i s i n I _. Then — B , i s i n J , consequently f o r some n-1 k n-1 A i n j such that ^ A » + : B k i s i n A . Then l e t / n~i» I f there i s no such sentence B , then f i s / k n n-1 I t i s clear that C i s a complete chain through f . The difference with the s e n t e n t i a l calculus l i e s i n the f a c t that not necessarily there i s a complete and ti-complete chain through each f . , hence not necessarily the set J B / + B £ J \ ^ i s c l a s s i -c a l l y s a t i s f i a b l e , i . e . the converse of theorem 1 does not Hold. In the example 2 of Section 1 i s represented a model without CJ -complete chains. Indeed i f C i s any chain i n that model then C i s complete, +A(n) i s i n ef f o r each neN, but - VxA(x) i s i n cf' Enlarging the d e f i n i t i o n of p r o p o s i t i o n a l l y atomic sentences (def. 1-2) to a l l the atomic sentences and a l l the sentences of the form VxB (x) and dxB(x) we can conclude that i f C i s any complete chain i n a model, then to the set there corresponds a Boolean evaluation on the set of a l l the p r o p o s i t i o n a l l y ato-mic sentences J which not necessarily i s a f i r s t order evaluation. This happens i f and only i f the complete chain i s also cV-complete. The following theorem and c o r o l l a r y are an obvious consequence of theorem 5-g.. 50 THEOREM 3 - Let A be any set of sentences and l e t " ^ A be obtained from A by adding a double negation i n front of each of the sentences of . Let B be c l a s s i c a l l y provable from _A "by using only modus ponens as deduction r u l e , then ^ ~ A h ^^B. I Let = be the prop o s i t i o n a l connective f o r equivalence, then: COROLLARY 1 - Let B be c l a s s i c a l l y provable from A by using only modus ponens." Then K^" B where A* is obtained from A hy sub-s t i t u t i n g each sentence $ i n A with any sentence D such that D = D 1 i s a tautology. Let C be any complete chain i n a model. The set cf t, has been c a l l e d by F i t t i n g jj>J an almost t r u t h set. An almost t r u t h set cjf c d i f f e r s from a t r u t h set as defined by Smullyan JJL3J only i n the claiuse r e l a t i v e to the uni v e r s a l q u a n t i f i e r . I f indeed f o r some formula B(x), + \/xB(x) i s i * 1 ^ then +B(a) i s i n cf f o r each name a used i n ^  , but the converse does not c c hold. Therefore: LEMMA 1 - I f B i s any sentence without u n i v e r s a l q u a n t i f i e r s i n i t , and B i s i n every t r u t h set then B i s i n every almost t r u t h set. DEF. 5 - Let B be any sentence, then: i s the sentence obtained from B by replacing each part 51 of B of the form VxD (x) with ^ 3 x ^ D ( x ) . B + i s the sentence obtained from B by replacing each atomic formula i n B with i t s double negation. B° i s the sentence obtained from B by replacing each part of B of the form 3xD(x) with ^\/x^D(x) and each part of the form D V E with ^ ( ^ D & ^ E ) . ++ + B i s l i k e B except that the replacement of an atomic f o r -mula A by ~ A i s not made when A i s preceeded by a negation. B i s l i k e B except that an atomic formula A i s replaced by ~«^A only when i t i s alone, or immediately w i t h i n the scope of an & or a V , o r i t i s the second part of the scope of an 3 . B"* i s l i k e B except without the replacements i n the se-cond part of the scope of an 3 . B' i s obtained from B by replacing: each part of the form D oE with ^ ( D & ^ E ) , each part of the form i3xD(x) with ~ VX/-^D (x) and each part of the form D V E with ^/(^D & ^ E ) . The next theorem e a s i l y follows from Lemma 1; i t i s together with theorem 3 the equivalent of theorem 59 h) £ 81 of Kleene JJLZLJ . THEOREM 4 - I f A B then A \ ~ B~ . c 1 Suppose indeed that /\ !•—B but ~ ~» ~ ^ B. C I 52 Then there i s a model ^  with a f i n i t such t h a t + <^ D^ i s i n f * f o r each D i n A and - ~ ^ B i s i n f1 *. Therefore there i s an i n such that: and + ^  i s i n f o r each D i n Z\. together with+<-^B. By theorem 2 there i s a complete chain through . Let C be any syph chain,then +D i s i n f o r each D i n _A_ while -B i s i n c f . This i s impossible because +B hence +33 i s i n any t r u t h — A — set containing +D f o r eacja D i n A , but B i s without u n i v e r s a l q u a n t i f i e r s , hence by lemma 1 i t must also be i n any almost t r u t h set containing +D for each D i n 2) . - II — ~T \» COROLLARY 2 - I f A * — B then A hr- ~ ~> B where A i s obtained from A by replacing each sentence D i n A with a sentence D'1 such that D = D , r i s a tautology. LEMMA 2- I f B i s any sentence from O and without the connecti-3 + + i n i t then ^ ~ ^ B • The lemma w i l l be proved by induction on the degree of B. I f deg. B = 0 then B i s an atomic sentence A(a) and B + = ^ ^ A ( a ) . Suppose there i s a j i n a model -v f o r 0 and „ such that but - ^ /-v ft (a) i s i n J , then there i s a A i n ^  such that f R A and + ~ ^ ~"^A(a) and + ^ A ( a J i s i n Z \ * • But by theorem 2 there i s a complete chain C through A . Then cf would correspond to a Boolean evaluation where A(k) i s f a l s e and A(a) i s true. 53 Suppose the theorem true when cleg. B^n. Let B he such that deg.B= =n+l. B i s D & E . Suppose there i s a I i n a model 3/ f o r o and •3) such that _ , _ and - ( D + & E +) i s i n / , then either T1 ^  -D + OE - E + i s i n / , but by the induction hypothesis both + + + + r* ^  + + ^ ^ D O D and + / ~ ^ E D E are i n I ,, hence either — or — respectively i s i n / . Therefore there i s a 4 i n / such that P H A and + (D + & E + ) i s i n A * and either +^D + or +^E ,respectively, i s i n /\ . Let G be any complete chain through A , then c/ would not be a Boolean evaluation on the set of the p r o p o s i t i o n a l l y atomic sentences. B i s r^yj) . Suppose there i s a P i n a model such that + ^ ^ ^ D i s i n * and - MD i s i n / , then there i s a A i n ^ such that and +<^^^J) and +D would be botlsldn A * . But then i f C i s any complete chain through A the set cJ would not correspond to a Boolean evaluation. B i s D3E. Suppose there i s a f i n a model such that-.-tr/~"v (D+'2> E + ) i s i n V and - ( D +D K +) i s i n ^ . Thenthere i s i n ^  such that f1 R A and each of + A / ^ ( D + D E + ) , +D+and - E + EW^ J i n J\ , but by the induction hypothesis + ( ^ ^ 3 E + ) i s i n A * , hence — i s i n A * . B u t then there i s an X I i n ^ such that A R . Q . and each of + A/A/ (D+ d E + j ^ + D + a n a + ^ E + i s i n £1*. I f C i s any complete chain through then the set <~J would not eorrepond to a Boolean 54 evaluation. B i s VxD(x) . Suppose there i s a / in a model U such that + t/xD+(x> i s in r * and - VxD +(x) i s i n F*. Then there i s a such that f R.A and for some sentence D +(a) from^A , -D +(a) i s i n A* to-gether with + ^ ^ V x D + ( x ) . But. by the induction hypothesis + A W D ( a ) o D (a) is in A , hence (a) i s in A . Then there i s an CI i - n ^ such that Js. TlSX and both + v^xD+(x) and are m hence there i s a ® i n ^  such that and both + V*D + ( x ) and +^D +(a) are i n v v . Let C be any complete chain through 0 , then the set ^  would not be an almost truth set. L EMMA 3 - Let -y be any model and C any complete chain i n i t . Then fmr any sentence B, +B i s i n i f and only i f +B0^ i s i n , The lemma i s obviously true when deg. B = 0 because then B = A for some atomic sentence A, B = A and B 0 + = ~"^A. Indeed i f in the Boolean evaluation corresponding to S' A i s true also ^ " ^ A i s true and viceversa. Suppose the lemma be true when deg.B^n and suppose deg.B =n+l. B i s D & E then B i s D & f and B 0 + i s D 0 + & E 0 + . If + D & E i s i n ^ n then; both +37 and +E are in o „ hence both ? C +D0 + and a+E0 + are in >D by the induction hypothesis, hence + D 0 + & E°+ i s i n ^  . Similarly i f + D°* ¥~E°+ i s in then + D & E i s in . 55 B i s D V E then B i s D ! E and B°+ i s r^(«sV°+ & ^ E 0 + ). If + if V E i s in cfn then either +D OE +E i s i n of , hence either +D0+ or +E 0 + i s c/ by the induction hypothesis. Because d i s + an almost truth set then +^(^T)o & ^ E 0 + ) i s i n C9 Similarly i f +^(<-^D°+ & ^ E 0 + ) i s i n c/ then D V E i s i n ^  . Ms ^D, then B i s D and B°+ i s M30 + . If + <~D i s i n c/ then -D i s i n , hence by the induction hypo-} J ? thesis -D 0 + i s i n cy hence + ^ B 0 + i s i n c/_. 0 J? - J7 Similarly i f + ~"D° + i s i n z) then i s in oJ . B i s D 3 E then B i i D D E and B°+ i s D°+j E 0 + . If + DDE i s i n then either +Dor -E i s in <v , hence by the ' Jp c induction hypothesis +D°+ or - E 0 + i s in therefore + D 0 + 3 S ° + i s 0 C i n ^ . Similarly i f + D°+3 E 0 + ; i s Indfg then + ELD E i s i n B i s 3xD(xi> then B i s iJxDtx) and B 0 + i s ^ ^ x ^ D 0 + (x). If +HxtT(x) i s i n c / c then for some sentence D(a) from c / , +D(a) i s i n C^Q» hence by the induction hypothesis +D°+(a) i s in c^. Because C i s complete one of - \/x^D 0 +(x) or +Vx^<D 0 +(x) i s in c2 . If + \/x <~T)0+(x) i s i n c f , then because cf i s an almost truth set + <-/D0 + (a) would be incv ^ . This i s impossible, there-fore - Vx' v /D 0 +(x) i s i n ^  hence +^Vx^<D 0 + (x) i s i n c | , Suppose + < ~ V x ^ D o + ( x) i S i n <<7 then - \/ x~D°+"<jx) i s in ^  . If there i s a sentence D 0 +(a) from c? such that +D 0 +(a) i s i n cf then by the induction hypothesis +D(a) i s in cf hence +£?xD(x) J? i s i n O ^. If + ~ Vx^-D°+(x) i s in cf and for a l l sentences D 0 +(a) f r o m ^ , o 56 -D° + (a) i s in cJ l e t us suppose, being C complete, that -3xD(x) i s i n ^ T h e n there i s a f in the chain C such that both + '*<i?xD (x) and +~ ,Vx^D 0 + (x) are in V * then -Vx<VD°+( 'x) i s in I *. Hence for some /\ in -jj, such that f R A and for some sentence D°+(a) from A , both -^D 0 + (a) and + ~ 3 x D ( x ) are in A . But then there is an Q. in | such that A. R o l a n d both + ^ j xD(x) and +D°'+(a) are in !vL . L e t C* be any complete chain through £T1 , then both +-*^ -?xD(x) and +D°+(a) are i n of , hence by the induction hypothesis +D(a) i s in n* a n d because S „. i s an almost truth set + '3xD(x) i s i n J o f C 1. ,a contradiction. C B i s VxDCx), then B i s ^ 3 x^D(x) and B 0 + i s VxD0+(x). Suppose + ^ " 3 x^D(x) i.s^ «if then -3x<VD(x) i s in . hence -P 0 — J 7 C because i s an almost truth set -^D(a) i s in <u n for each sentence D(a) from C/\ , hence +D(a) i s in of for each sentence _ J? G c D(a) fromCV c < Suppose - V x ^ ^D°+(x) i s in d^,, then for some i n C, both + /^3-Xs©(xJ- and + ^  Vx^^D°+(x) ,hence - V x ~^D° + (x)', are i n I Therefore there i s a A in -j? such that f1 R A and + x^Dfx) A* ^ together with -'v^D 0+(a) for some sentence D 0 +(a) ffom A . Then there i s an £l in M. such that A E ^ l and both + ~ 3 x ^ D ( x ) and +^D 0 +(a) are in ±L . Let C* be any complete chain through then both -3x'~D(x) and -D°+(a) are in of . By the induction hypothesis -D(a) i s in , hence, being v an almost truth — 9 Zj — -r set, +^D(a) i s - i n c J p i hence + J x ^ D ( x ) i s in <0 , a contradiction. Therefore -pc^ ^ D 0 + (x> i s not in o) n and, being C complete + Vx^^Do+Cx) i s in <^n. 57 Suppose now that + (x) i s i n <3 , then there i s a I i n C such that both + V x A / ^ D 0 + ( x ) and +/v + ( x ) aredn I , then (x) i s i n | . Therefore there i s ^ A i n $ such that + V x ^ ^ D 0 + ( x ) i s i n A together with -D 0 +(a) f o r some sentence D 0 +(a) from A . But then + ^ D ° + (a) and - D 0 + (a> are both i n A * , hence - ( A / ^ D 0 + (a)OD 0 + (a)) i s i n A * . This i s impossible because by lemma 1 +^rVD0 + (a.) 3 D 0 + ( a ) i s v a l i d , being D°*(a) a sentence without disjunctions or e x i s t e n t i a l q u a n t i f i e r s i n i t . Therefore i f +~3fxM)(x) i s i n ^ ? , being C complete + VxD 0 + (x) must be i n c/^. F i n a l l y i f +VxD 0 +(x) i s i n ^  then +D 0 +(a) i s i n f o r any JP — sentence D 0 + ('a) from c/^, hence by the induction hypothesis +D(a) i s i n „ f o r each sentence D(a) from <^„. Suppose + J X ^ D ( X ) i s i n O then f o r some sentence D(a) from £) , +~D(a;), hence -D(a) i s i n ^ ni a contradiction. Hence, being C complete, - 3 x ^ D ( x ) i s i n ^ n -Let A he any set of sentences and /\ 0 + be obtained from /\. by replacing each sentence D i n A with D 0 +. THEOREM 5 - I f A'r B then A 0 + f — B 0 + . ° I I t i s enough to prove that A 0 + £=- ~"~B0 +. Indeed by d e f i n i t i o n 5 B° i s a sentence without the connective V and the q u a n t i f i e r , hence by lemma 2 fe" ^^3°+ 3 B 0 + , hence i f A 0 +1= . ~ ~ £ 0 + . then J- x A 0 + ^ B0+ and &.°+tpB° + f o r the completeness of £iituiti oni-s t i c l o g i c with respect to these models. 58 Suppose there i s a f in a model such that + D 0 + is i n F * for each D in /s, , hut - ^ ^ B ^ i s in V . Then there-is an such that f U£L and + D 0 + i s in dlTfor each D iri A together with + ~B° + . By theorem 2 these i s a complete chain through Q. , Let C he any such chain. +D0 + i s i n S for each D i n A and +^B 0 + i s in c/^, hence by lemma 3 + ^ B i s i n $ together with +D for each D i n A • But i f /\ B then A t"^- ^ "^B by corollary 2 , hence + ^ —'B i s in contradiction. c a Recalling def. 5 we can deduce that for any sentence B, B + + i s obtained from B + by replacing each expression of the form in B + where A i s an atomic formula, with ^ A. It i s t r i v i a l tha't ^.r^^^Ao^A and t= ^  A ^ w^^A, for any atomic sentence A. Therefore: j. COROLLARY 3- If B then Z\.°++^B°++. Indeed i f /A B then by theorem 5 A i 0+H-B 0 + . By the previous observation i t i s clear that for any sentence E and for any f i n a model , +E 0 + i s i n Y i f and only i f + E 0 + + i s i n I , hence the corollary follows. THEOREM 6 - I f A ^ B then ^ °+++ t_B°++ +. It i s clear from definition 5 that B 0 + + + i s obtained from B 0 + + by replacing each part of the form ~ , < ^ A D D 0 + + with A D D ° + + , 59 moreover "by lemma 2 t= ~ ^ D 0 + J > D ° + . 1 ^ J?, It i s enough therefore to prove that for any I in a model and for any sentence E from V and for any atomic sentence A from I , i f + ^ ^ E O E i s i n J then A3E and ^ / ^ A ^ E have the same sign i n Y . Prom thfcs ) i t follows that for any sentence P +P 0 + + i s in r ^r ji "X" i f and only i f +p;0+++ i s i n I and by theorem 5 our theorem i s proved. Suppose both + ^ ^ E ^ E and +~^A -3 E are i n F1 If — ADE.is i n P , then thereis an in such that P R _C1 and each of +^^ADE and -E arre in , hence both - and+A are in S.*- , a contradiction. • \. Suppose both + ^ ^ E ^ E and + A o E are in P^hut - ^ ^ A ^ E i s i n P* . Then there i s an XV i n such that f H^l and each of + ^ ^A, -E, + AoE and + ~ ^ E ^ E aa?e-in XI* , hence - ~~<E i s in Thenfore there i s a $ i n such that X\_ R © and each of + ^ 'v/A, + A^E, + ~/E i s i n By theorem. 2 there i s a complete chain through W . Let C be any such chain. Then +A, + A =>E and -E are i n of which i s implossible because <zf i s a Boolean evaluation^ on the set of a l l the propo-Bitionally atomic sentences from ^ . THEOREM 7 - I f A h r B then / f I B* ' . Indeed i f A ^ B then ( A + + + ) 1 f-^-(B+++) », hence by theorem 6: [(A + + + ) ^ ] °* +* h^-]CB + + +)*J 0^^ + >. But from definition 5 we can deduce that for each sentence E : (E + + +)» o + + + = ( E + + + ) ' l j n e n c e 60 The theorem follows i f we prove that f o r any sentence E and f o r any | i n a model M +E i s i n / i f and only i f +(E ) i s i n / I f deg.E = 0 t h i s i s obvious because then E*'=(E + + +)' . Suppose i t i s true when deg.E = n, l e t deg.E = n+1. But then by d e f i n i t i o n 5 the only difference between (E ) and E i s that each part of the form ¥=> A i n E , where A i s an atomic formula, i s replaced by /->(P*' & <-^A) i n EK' and b y ^ ( ( P + + + ) ' S:^^^ i n ( E + + + ) ' . By the induction hypothesis F*'and ( F + + + )' have the same sign i n T f o r any f i n a model . The same i s obviously true f o r ^ k and ~ ~* ^  A . Prom t h i s the theorem follows. 61 BIBLIOGRAPHY 1 ; E.T.BELL The development of Mathematics > 2nd Ed.. New York 1945 2 E.W. BETH Semantic construction of Intu i t i o n i s t i c Logic (Medelingen der Kon. Ned. Akad. vs, Wet.., new series vol. 19 no 11) Amsterdam 1956 E.W. BETH She foundations of Mathematics North Holland 1959 E. BISHOP Foundations of constructive analysis Me Graw H i l l , 1967 M.C. FITTING Intuitionistic Logic, Model Theory and Forcing North Holland, 1969 S. GORNEMANN A. GRZEGORCZYK A logic stronger than intuitionism Journal of Symbolic Logic vol. 36 no 2 June 1971 A philosophically plausible formal inter-pretation of i n t u i t i o n i s t i c logic Indagationes Mathematicae 26,1964 62 8 A. GRZEGORCZYK 9 A. HEYTING 10 A. HEYTING 11 S.C. KLEENE 12 S.A. KRIPKE 13 R.M. SMULLYAN Assertions depending on time and corresponding logical c a l c u l i in:Logic and Foundations of Mathematics Wolters-Noordhoff Publ. Groningen,1968 Die formalen Regeln des intuitionistischen Logik S.B. Berlin, Phys.-math Kl., 1930 Intuitionism. An introduction North Holland, 1966 Introduction to metamathematics Van Nostrand 1952 Semantical Analysis of Intuitionistic Logic - I in:Formal Systems and Recursive Functions Ed. Crossley and Dummet North Holland, 196^ F i r s t Order Logic Springer-Verlag,1968 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            data-media="{[{embed.selectedMedia}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0302122/manifest

Comment

Related Items