StrongNormalizationMPCS.DVI


Mathematical Problems of Computer Science 28, 2007, 45{50.

Str ong N or malization for Fir st-or der Logic

Tig r a n M. Ga lo ya n

Institue for Informatics and Automation Problems of NAS of RA

e-mail: tigran.galoyan@gmail.com

Abstract

In this paper we discuss strong normalization for the ! 8 - fragment of ¯rst-order
logic. The use of the method of collapsing types to transfer the result concerning strong
normalization (that is, any derivation r is strongly normalizable) from implicational
logic to ¯rst-order logic is illustrated (ref [1]). The considered result is improved by
a complement, which states that for any derivation r and its collapse rc we need the
same number of one-step reductions (the !1 rule) to bring them to their normal forms.

Ou r b a s ic lo g ic c a lc u lu s is t h e ! 8 - fr a g m e n t o f m in im a l n a t u r a l d e d u c t io n fo r ¯ r s t -o r d e r
lo g ic o ve r s im p ly t yp e d la m b d a -t e r m s . Th is r e s t r ic t io n r e g a r d in g t h e m in im a l fr a g m e n t d o e s
n o t m e a n a lo s s in g e n e r a lit y, s in c e t h e fu ll c la s s ic a l ¯ r s t -o r d e r lo g ic c a n b e e m b e d d e d in t h is
s ys t e m b y a d d in g s t a b ilit y a xio m . Th e m e t h o d o f c o lla p s in g t yp e s d e ve lo p e d in [2 ] is u s e d
t o g e t s o m e r e s u lt s c o n c e r n in g t h e s t r o n g n o r m a liz a t io n o f d e r iva t io n s in ¯ r s t -o r d e r lo g ic .

Refer ences

[1 ] S c h wic h t e n b e r g , H .: Normalization. In F.L . B a u e r , e d it o r , L o g ic , A lg e b r a a n d Co m p u -
t a t io n . P r o c e e d in g s o f t h e In t e r n a t io n a l S u m m e r S c h o o l Ma r kt o b e r d o r f, Ge r m a n y, Ju ly
2 5 - A u g u s t 6 , 1 9 8 9 , S e r ie s F: Co m p u t e r a n d S ys t e m s S c ie n c e s , V o l. 7 9 , p a g e s 2 0 1 -2 3 7 .
N A TO A d va n c e d S t u d y In s t it u t e , S p r in g e r V e r la g , B e r lin , H e id e lb e r g , N e w Y o r k 1 9 9 1

[2 ] Tr o e ls t r a , A . a n d va n D a le n , D .: Constructivism in mathematics. A n in t r o d u c t io n . S t u d -
ie s in L o g ic a n d t h e Fo u n d a t io n s o f Ma t h e m a t ic s , V o l. 1 2 1 , 1 2 3 A m s t e r d a m : N o r t h
H o lla n d 1 9 8 8

ÊÇëï ÝáñÙ³Éǽ³ódz ³é³çÇÝ Ï³ñ·Ç ïñ³Ù³µ³ÝáõÃÛ³Ý Ñ³Ù³ñ

î. Ø. ¶³ÉáÛ³Ý

²Ù÷á÷áõÙ

²ß˳ï³ÝùáõÙ áõëáõÙݳëÇñí»É ¿ ËÇëï ÝáñÙ³Éǽ³óÙ³Ý ËݹÇñÁ ³é³çÇÝ Ï³ñ·Ç
ïñ³Ù³µ³ÝáõÃÛ³Ý ! 8 ÏïáñÇ Ñ³Ù³ñ£ ¸Çï³ñÏí»É ¿ ÷Éáõ½íáÕ ïÇå»ñÇ Ù»Ãá¹Ç
ÏÇñ³éáõÙÁ, áñÇ ÙÇçáóáí [1 ]-áõÙ ËÇëï ÝáñÙ³Éǽ³ódzÛÇÝ í»ñ³µ»ñíáÕ ³ñ¹ÛáõÝùÁ (³ÛÝ
¿ª Ï³Ù³Û³Ï³Ý Ã»ñÙ ËÇëï ÝáñÙ³Éǽ³óíáÕ ¿), ëï³óí³Í ÙdzÛÝ ïñ³Ù³µ³ÝáõÃÛ³Ý !
ÏïáñÇ Ñ³Ù³ñ, ï³ñ³ÍíáõÙ ¿ ݳ¨ ³é³çÇÝ Ï³ñ·Ç ïñ³Ù³µ³ÝáõÃÛ³Ý íñ³£ êï³óí»É ¿

4 5



4 6 Strong Normalization for First-order Logic

³é³í»É ³Ù÷á÷ ³ñ¹ÛáõÝù, áñÝ Ç Ñ³í»ÉáõÙÝ åݹáõÙ ¿ ݳ¨ª ó³Ýϳó³Í r ³ñï³ÍÙ³Ý ¨
¹ñ³ ѳٳå³ï³ëË³Ý rc ÷Éáõ½Ù³Ý ѳٳñ ³ÝÑñ³Å»ßï ¿ ÝáõÛÝ ù³Ý³ÏáõÃÛ³Ùµ Ùdzù³ÛÉ
黹áõÏódz, áñå»ë½Ç ¹ñ³Ýù µ»ñí»Ý ÝáñÙ³É Ó¨Ç£