TEOREMA INTERPOLASI UNTUK LOGIKA PREDIKAT NON-KOMUTATIF FL DAN FLw Bayu Surarso Jurusan Matematika FMIPA UNDIP Jl. Prof. H. Soedarto, S.H, Semarang 50275
Abstract. In 1961 Maehara introduced a proof-theoretical method to prove the interpolation theorem for standard logics. By developing Maehara’s method, we can prove interpolation theorem for some non-standard logics, including the commutative predicate logics Fle dan Fle,w. In the present paper we show that by modifying Maehara’s method we can also prove the interpolation theorem for non-commutative predicate logics FL and FLw. Keywords: Interpolation Theorem, Maehara’s Method, FL.
1. PENDAHULUAN Pembahasan masalah interpolasi melalui pendekatan sintaktik dipelopori salah satunya oleh Maehara pada [5], pada tulisan tersebut, dengan memanfaatkan teorema eliminasi cut teorema interpolasi dibuktikan berlaku pada logika intuisionistik. Metode yang digunakannya pada pembuktian teorema interpolasi tersebut kemudian dikenal sabagai metode Maehara. Dengan melakukan beberapa modifikasi terhadap metoda Maehara, penulis telah membuktikan teorema interpolasi untuk beberapa logika implikasional dan proposisional, antara lain teorema interpolasi untuk logika relevan positip R+, teorema interpolasi untuk beberapa perluasan dari logika implikasi BB’I dan untuk logika proposisi LDBCC dan LDBCK (Lihat [1], [2], dan [3]). Pada [4] penulis dan Marti Lestari mengembangkan metode Maehara untuk membuktikan teorema interpolasi pada logika predikat komutatif Fle, Flec dan Fle,w. Dipihak lain metode Maehara tidak dapat untuk membuktikan teorema interpolasi pada logika predikat nonkomutatif seperti Fl dan Flw, hal ini disebabkan karena tidak adanya aturan exchange pada logika tersebut. Pada tulisan ini ditunjukkan bahwa kegagalan metoda Maehara tersebut dapat diatasi
dengan memodifikasi padanya.
konsep
partisi
2. TEOREMA INTERPOLASI Untuk selanjutnya, notasi, simbol dan konsep yang digunakan pada tulisan ini merujuk pada [4]. Logika predikat FL dan Flw didefinisikan berturut-turut sebagai logika yang diperoleh dari logika predikat komutatif Fle dan Fle,w dengan menghilangkan aturan exchange. Teorema interpolasi menyatakan suatu sifat sebagai berikut: Misalkan formula A ⊃ B terbukti, maka ada suatu formula C, disebut interpolant, sedemikian sehingga: 1. A ⊃ C dan C ⊃ B keduanya terbukti. 2. V (C ) ⊂ [V ( A) ∩ V (B )]. Untuk membuktikan bahwa teorema tersebut berlaku untuk logika predikat komutatif Fle, Flec dan Fle,w., pada [4] metode Maehara dikembangkan sebagai berikut: Pertama didefinisikan partisi dari suatu barisan formula Γ sebagai berikut: Definisi 1. Misalkan Γ1 adalah barisan dari beberapa formula yang terdapat dalam Γ dan misalkan Γ2 adalah barisan dari semua formula yang terdapat dalam Γ kecuali yang terdapat dalam Γ1 . Maka ([Γ1 ], [Γ2 ]) adalah suatu partisi dari Γ .
25
Jurnal Matematika Vol. 11, No.1, April 2008:25-31
Kemudian, teorema interpolasi dibuktikan dengan membuktikan sifat yang lebih umum sebagai berikut: Teorema 2. Misalkan Γ → D suatu sequent yang terbukti, dan misalkan ([Γ1 ], [Γ2 ]) sembarang partisi dari Γ . Maka ada formula C , disebut interpolant dari Γ → D sedemikian sehingga: 1. Γ1 → C dan C , Γ2 → D keduanya terbukti 2. V (C ) ⊂ V (Γ1 ) ∩ [V (Γ 2 ) ∪ V (D )] dimana ekspresi V (Γ) menyatakan himpunan variabel proposisional yang terdapat dalam Γ . Pernyataan ini dibuktikan dengan menggunakan induksi pada banyaknya kemunculan aturan inferensi k yang muncul dalam bukti P tanpa cut dari Γ → D . Sebagai contoh, pada kasus k›0 dan aturan inferensi terakhir adalah (⊃ → ). Pada kasus ini bagian bawah dari bukti P dari sequent Γ → D berbentuk: Γ → A ∆, B, Σ → D (⊃→) , ∆ , A ⊃ B, Γ , Σ → D kasus ini dibagi menjadi 2 subkasus, yaitu a. Partisi dari ∆, A ⊃ B, Γ, Σ berbentuk dengan [∆ 1 , A ⊃ B, Γ1 , Σ1 ],[∆ 2 , Γ2 , Σ 2 ] ), ∆ = ∆ 1 , ∆ 2 , Γ = Γ1 , Γ2 , dan Σ = Σ1 , Σ 2 . Pada subkasus ini perhatikan bagian dari P yang merupakan bukti dari sequent kiri atas, Γ1 , Γ2 → A , berdasarkan induksi hipotesis ada formula C1 sedemikian sehingga 1a. Γ 2 → C1 dan C1 , Γ1 → A keduanya terbukti. 2a. V (C1 ) ⊂ V (Γ2 ) ∩ [V (Γ1 ) ∪ V ( A)] . Kemudian perhatikan bagian dari P yang merupakan bukti dari sequent kanan atas, ∆1 , ∆ 2 , B, Σ1 , Σ 2 → D , berdasarkan induksi hipotesis ada formula C 2 sedemikian sehingga
1b. ∆ 1 , B, Σ1 → C 2 dan C 2 , ∆ 2 , Σ 2 → D keduanya terbukti. 2b. V (C 2 ) ⊂ V (∆1 , B, Σ1 ) ∩ [V (∆ 2 , Σ 2 ) ∪ V (D )]
26
Dari 1a. dan 1b., sequent C1 , Γ1 → A dan terbukti. Dengan ∆ 1 , B, Σ 1 → C 2 menggunakan aplikasi (⊃→) pada kedua sequent tersebut dilanjutkan dengan beberapa aplikasi aturan exchange dan sebuah (→⊃) dapat diperoleh bukti dari sequent . ∆ 1 , A ⊃ B, Γ1 , Σ → C1 ⊃ C 2 Sedangkan dari terbuktinya Γ 2 → C1 dan C 2 , ∆ 2 , Σ 2 → D dengan menggunakan aplikasi (⊃→) pada kedua sequent tersebut dilanjutkan dengan beberapa aplikasi aturan exchange dapat diperoleh bukti dari C1 ⊃ C 2 , ∆ 2 , Γ2 , Σ 2 → D . Dari 2a. dan 2b., dengan sifat komutatif dari operasi ∪ dapat diperoleh sifat V(C1 ⊃ C2 ) ⊂V(∆1, A ⊃ B, Γ1 , Σ1 ) ∩[V(∆2 , Γ2 , Σ2 ) ∪V(D)]
Sehingga pada subkasus ini C = C1 ⊃ C 2 merupakan interpolant dari Γ → D . b. Partisi dari ∆, A ⊃ B, Γ, Σ berbentuk ( [∆ 1 , Γ1 , Σ1 ], [∆ 2 , A ⊃ B, Γ2 , Σ 2 ] ), dimana ∆ = ∆ 1 , ∆ 2 , Γ = Γ1 , Γ2 , dan Σ = Σ1 , Σ 2 . Pada subkasus ini perhatikan bagian dari P yang merupakan bukti dari sequent kiri atas, Γ1 , Γ2 → A , berdasarkan induksi hipotesis ada formula C1 sedemikian sehingga 1a. Γ1 → C1 dan C1 , Γ2 → A keduanya terbukti. 2a. V (C1 ) ⊂ V (Γ1 ) ∩ [V (Γ2 ) ∪ V ( A)] . Kemudian perhatikan bagian dari P yang merupakan bukti dari sequent kanan atas, ∆1 , ∆ 2 , B, Σ1 , Σ 2 → D , berdasarkan induksi hipotesis ada formula C 2 sedemikian sehingga 1b. ∆ 1 , Σ1 → C 2 dan C 2 , ∆ 2 , B, Σ 2 → D keduanya terbukti. 2b. V (C 2 ) ⊂ V (∆ 1 , Σ 1 ) ∩ [V (∆ 2 , B , Σ 2 ) ∪ V (D )] Dari 1a. dan 1b., sequent Γ1 → C1 dan maka dengan ∆ 1 , Σ1 → C 2 terbukti, menggunakan aplikasi (∗→) pada kedua sequent tersebut dilanjutkan dengan beberapa aplikasi aturan exchange dapat diperoleh bukti dari sequent Sedangkan dari ∆ 1 , Γ1 , Σ → C1 ∗ C 2 .
Bayu Surarso (Teorema Interpolasi untuk Logika Predikat Non-Komutatif Fl dan Flw)
terbuktinya sequent C1Γ 2 → A dan C 2 , ∆ 2 , B, Σ 2 → D dengan menggunakan aplikasi (⊃→) pada kedua sequent tersebut dilanjutkan dengan beberapa aplikasi aturan exchange dan sebuah aplikasi (∗→) dapat diperoleh bukti dari sequent C1 ∗ C 2 , ∆ 2 , A ⊃ B, Γ2 , Σ 2 → D . Dari 2a. dan 2b., diperoleh sifat V(C1 ∗ C2 ) ⊂ V (∆1, A ⊃ B, Γ1, Σ1 ) ∩[V(∆2 , Γ2 , Σ2 ) ∪V (D)]
Sehingga pada subkasus ini C = C1 ∗ C 2 merupakan interpolant dari Γ → D . Dengan terbuktinya Teorema 1 maka teorema interpolasi hanyalah sebagai akibat langsung saja, yaitu dengan memilih Γ sebagai barisan formula dengan satu anggota saja, Γ1 = Γ dan Γ2 sebagai barisan kosong.
3. BUKTI TEOREMA INTERPOLASI PADA FL dan FLw Pada logika predikat non-komutatif FL dan FLw pengembangan metoda Maehara seperti pada [4] tidak bisa diterapkan, tidak adanya aturan exchange akan menimbulkan kesulitan dalam membuktikan berlakunya teorema interpolasi, terutama pada kasus k›0 dan aturan inferensi terakhir adalah (⊃ → ). Untuk mengatasi kesulitan tersebut, pertama konsep partisi perlu diubah sebagai berikut: Definisi 3. Misalkan Γ =A1,A2,...,An. Misalkan pula Γ1 = A1,A2,...,Al , Γ2 = Al+1,Al+2,...,Am dan Γ3 = Am+1,Am+2,...,An dengan 0≤l≤m≤n, maka ([Γ2 ], [Γ1 , Γ3 ]) adalah suatu partisi* dari Γ . Contoh: ([A, C ], [A, B, D, C ]) dan ([B, A, C , D ], [A, C ]) adalah partisi* dari Σ = A, B, A, C , D, C , sedangkan ([C, A], [A, B, D, C]) dan ([B, D], [A, A, C, C]) bukanlah suatu partisi dari Σ. Selanjutnya teorema interpolasi pada logika predikat FL dan Flw dibuktikan dengan membuktikan sifat berikut: Teorema 4. Misalkan Γ → D suatu sequent yang terbukti, dan misalkan
([Γ2 ], [Γ1 , Γ3 ])
sembarang partisi* dari Γ . Maka ada formula C , disebut interpolant dari Γ → D sedemikian sehingga: 1. Γ1 → C dan Γ1C , Γ3 → D keduanya terbukti 2. V (C ) ⊂ V (Γ1 ) ∩ [V (Γ1 , Γ3 ) ∪ V (D )] . Perhatikan bahwa sifat tersebut adalah suatu modifikasi dari Teorema 2. Seperti pada [4], sifat ini dibuktikan dengan menggunakan induksi pada banyaknya kemunculan aturan inferensi k yang muncul dalam bukti P tanpa cut dari Γ → D . Pada tulisan ini, ditunjukkan bagaimana kesulitan pada kasus k›0 dan aturan inferensi terakhir adalah (⊃ → ) dapat diatasi dan selanjutnya ditunjukkan pula bagaimana penyelesaian kasus k›0 dan Γ → D adalah sequent bawah dari aturan-aturan quantifiers.
• Kasus k›0 dan inferensi terakhir adalah (⊃ → ). Pada kasus ini bagian bawah dari bukti P dari sequent Γ → D berbentuk: Γ → A ∆, B , Σ → D (⊃→) , ∆ , A ⊃ B, Γ , Σ → D kasus ini dibagi menjadi 6 subkasus, yaitu a. Partisi* dari ∆, A ⊃ B, Γ, Σ berbentuk ( [ ∆ 2 , A ⊃ B , Γ1 ], [ ∆ 1 , Γ2 , Σ ] ) dengan Γ = Γ1 , Γ2 dan ∆ = ∆ 1 , ∆ 2 Pada subkasus ini perhatikan bagian dari P yang merupakan bukti dari sequent kiri berdasarkan induksi atas, Γ → A, hipotesis ada formula C1 sedemikian sehingga 1a. Γ 2 → C1 dan Γ1 , C1 → A keduanya terbukti. 2a. V (C1 ) ⊂ V (Γ2 ) ∩ [V (Γ1 ) ∪ V ( A)] . Kemudian perhatikan bagian dari P yang merupakan bukti dari sequent kanan atas, ∆, B, Σ → D , berdasarkan induksi hipotesis ada formula C 2 sedemikian sehingga 1b. ∆ 2 , B → C 2 dan ∆ 1 , C 2 , Σ → D keduanya terbukti.
27
Jurnal Matematika Vol. 11, No.1, April 2008:25-31
2b. V (C2 ) ⊂ V (∆ 2 , B) ∩[V (∆1 , Σ) ∪V (D)] Dari 1a. dan 1b., sequent Γ1 , C1 → A dan ∆ 2 , B → C 2 terbukti, maka dengan menggunakan aplikasi (⊃→) pada kedua sequent tersebut dilanjutkan dengan satu aplikasi (→⊃) dapat diperoleh bukti dari ∆ 2 , A ⊃ B, Γ1 → C1 ⊃ C2 sebagai berikut
Γ1 , C1 → A ∆ 2 , B → C 2 (⊃→) ∆ 2 , A ⊃ B, Γ1 , C1 → C 2 (→⊃) ∆ 2 , A ⊃ B, Γ1 → C1 ⊃ C 2 sedangkan dari terbuktinya Γ 2 → C1 dan dengan menggunakan ∆1 , C2 , Σ → D aplikasi (⊃→) pada kedua sequent tersebut dapat diperoleh bukti dari sequent ∆ 1 , C1 ⊃ C 2 , Γ2 , Σ → D sebagai berikut
Γ 2 → C1 ∆ 1 , C 2 , Σ → D (⊃→) ∆ 1 , C1 ⊃ C 2 , Γ2 , Σ → D Dari 2a. dan 2b., dapat diperoleh sifat
V(C1 ⊃C2) ⊂V(∆2, A ⊃ B,Γ1) ∩[V(∆1,Γ2,Σ) ∪V(D)] Sehingga pada subkasus ini C = C1 ⊃ C 2 merupakan interpolant dari Γ → D . b. Partisi* dari ∆, A ⊃ B, Γ, Σ berbentuk ( [ ∆ 2 , A ⊃ B , Γ , Σ1 ], [ ∆1 , Σ 2 ] ) dengan
∆ = ∆ 1 , ∆ 2 dan Σ = Σ1 ,Σ 2 Pada subkasus ini perhatikan bagian dari P yang merupakan bukti dari sequent kanan atas, ∆, B, Σ → D , berdasarkan induksi hipotesis ada formula C sedemikian sehingga 1. ∆ 2 , B, Σ1 → C dan ∆1 , C, Σ 2 → D keduanya terbukti. 2. V (C) ⊂V (∆2 , B, Σ1 ) ∩ [V (∆1 , Σ2 ) ∪V (D)] Dengan menggunakan aplikasi (⊃→) pada dapat Γ → A dan ∆ 2 , B , Σ 1 → C diperoleh bukti dari sequent ∆ 2 , A ⊃ B, Γ, Σ1 → C sebagai berikut
28
Τ → A ∆ 2 , B, Σ 1 → C (⊃→) ∆ 2 , A ⊃ B, Γ , Σ 1 → C Dari 2, dapat diperoleh sifat V (C) ⊂ V (∆2 , A ⊃ B, Γ, Σ1 ) ∩[V (∆1 , Σ2 ) ∪V (D)] Sehingga pada subkasus ini C merupakan interpolant dari Γ → D . c. Partisi* dari ∆, A ⊃ B, Γ, Σ berbentuk ( [Γ2 , Σ 1 ], [ ∆ , A ⊃ B , Γ1 , Σ 2 ] ) dengan
Γ = Γ1 , Γ2 dan Σ = Σ1 ,Σ 2 Pada subkasus ini perhatikan bagian dari P yang merupakan bukti dari sequent kiri atas, Γ → D , berdasarkan induksi hipotesis ada formula C1 sedemikian sehingga 1a. Γ 2 → C1 dan Γ1 , C1 → A keduanya terbukti. 2a. V (C1 ) ⊂ V (Γ2 ) ∩ [V (Γ1 ) ∪ V ( A)] . Kemudian perhatikan bagian dari P yang merupakan bukti dari sequent kanan atas, berdasarkan induksi ∆, B, Σ → D , hipotesis ada formula C 2 sedemikian sehingga 1b. Σ 1 → C 2 dan ∆ , B, C 2 , Σ 2 → D keduanya terbukti. 2b. V (C2 ) ⊂ V (Σ1 ) ∩ [V (∆, B,Σ2 ) ∪V (D)] Dari 1a. dan 1b., Γ2 → C1 dan Σ1 → C 2 terbukti, maka dengan menggunakan aplikasi (→∗) pada kedua sequent tersebut dapat diperoleh bukti dari Γ1 , Σ 1 → C 1 ∗ C 2 sebagai berikut Γ2 → C1 Σ1 → C2 (→ ∗) Γ2 , Σ1 → C1 ∗ C2 sedangkan dari terbuktinya sequent Γ1 , C1 → A ∆ , B, C 2 , Σ 2 → D dan dengan menggunakan aplikasi (⊃→) pada kedua sequent tersebut dilanjutkan dengan aplikasi ( ∗ → ), dapat diperoleh bukti dari ∆ 1 , A ⊃ B, Γ1 , C1 ⊃ C 2 , Σ 2 → D sebagai berikut
Bayu Surarso (Teorema Interpolasi untuk Logika Predikat Non-Komutatif Fl dan Flw)
Γ1 , C1 → A ∆, B, C 2 , Σ 2 → D (⊃→) ∆, A ⊃ B, Γ1 , C1 , C 2 , Σ 2 → D (∗ →) ∆, A ⊃ B, Γ1 , C1 ∗ C 2 , Σ 2 → D Dari 2a. dan 2b., dapat diperoleh sifat
V(C1 ∗C2) ⊂V(Γ2,Σ1) ∩[V(∆, A ⊃ B,Γ1,Σ2 ) ∪V(D)] Sehingga pada subkasus ini C = C1 ∗ C 2 merupakan interpolant dari Γ → D . d. Partisi* dari ∆, A ⊃ B, Γ, Σ berbentuk ( [ ∆ 2 ], [ ∆ 1 , ∆ 3 , A ⊃ B , Γ, Σ ] )
dengan
∆ = ∆1 , ∆ 2 , ∆ 3 Pada subkasus ini perhatikan bagian dari P yang merupakan bukti dari sequent kanan atas, ∆, B, Σ → D , berdasarkan induksi hipotesis ada formula C sedemikian sehingga 1. ∆ 2 → C dan ∆1 , C, ∆3 , B, Σ → D keduanya terbukti. 2. V (C ) ⊂ V (∆ 2 ) ∩ [V (∆1 , ∆ 3 , B, Σ) ∪ V (D)] Dengan menggunakan aplikasi (⊃→) pada sequent Γ → A dan ∆ 1 , C , ∆ 3 , B, Σ → D dapat diperoleh bukti dari sequent ∆ 1 , C , ∆ 3 , A ⊃ B, Γ, Σ → C sebagai berikut Τ → A ∆ 1 , C , ∆ 3 , B, Σ → D (⊃→) ∆ 1 , C , ∆ 3 , A ⊃ B , Γ, Σ → D Dari 2, dapat diperoleh sifat V (C) ⊂ V (∆2 ) ∩[V (∆1 , ∆3 , A ⊃ B, Γ, Σ) ∪V (D)] Sehingga pada subkasus ini C merupakan interpolant dari Γ → D . e. Partisi* dari ∆, A ⊃ B, Γ, Σ berbentuk ( [Γ2 ], [ ∆ , A ⊃ B , Γ1 , Γ3 , Σ ] )
dengan
Γ = Γ1 , Γ2 , Γ3 Interpolant dari Γ → D pada subkasus ini dapat diperoleh dengan cara yang sama dengan cara pada subkasus d. f. Partisi* dari ∆, A ⊃ B, Γ, Σ berbentuk ( [Σ 2 ], [ ∆ , A ⊃ B , Γ, Σ1 , Σ 3 ] )
Σ = Σ1 , Σ 2 , Σ 3
dengan
Interpolant dari Γ → D pada subkasus ini dapat diperoleh dengan cara yang sama dengan cara pada subkasus d. • Kasus k›0 dan inferensi terakhir adalah (→ ∃) . Pada kasus ini bukti P dari sequent Γ → D berbentuk: Γ → A(t ) (→ ∃) Γ → ∃zA( z ) Perhatikan bagian dari P yang merupakan bukti dari sequent atas dari aturan inferensi (→ ∃) tersebut, yaitu Γ → A(t ) . Dengan induksi hipotesis ada formula C sedemikian sehingga: 1. Γ2 → C dan Γ1 , C , Γ3 → A(t ) keduanya terbukti. 2. V (C ) ⊂ V (Γ2 ) ∩ [V (Γ1 , Γ3 ) ∪ V ( A(t ))] Dari 1. sequent Γ1 , C , Γ3 → ∃zA( z ) dapat dibuktikan seperti berikut Γ1 , C , Γ3 → A(t ) (→ ∃) . Γ1 , C , Γ3 → ∃zA( z ) Sedangkan V ( A ( t ) ) ⊂ V ( ∃zA ( z ) ) , maka dari 2. dapat diperoleh sifat V (C ) ⊂ V (Γ2 ) ∩ [V (Γ1 , Γ3 ) ∪ V (∃zA( z ))] Jadi pada kasus ini C merupakan interpolant dari Γ → D .
• Kasus k›0 dan inferensi terakhir adalah (∃ →) . Pada kasus ini bukti P dari sequent Γ → D berbentuk: Γ, A(x ), ∆ → D (∃ →) Γ, ∃zA( z ), ∆ → D Kasus ini dibagi menjadi 3 kasus, a. Partisi dari Γ, ∃zA( z ), ∆ ([Γ2 , ∃zA(z ), ∆1 ], [Γ1 , ∆ 2 ])
berbentuk
Perhatikan bagian dari P yang merupakan bukti dari sequent atas aturan inferensi (∃ →) tersebut, yaitu Γ, A(x ), ∆ → D . Menurut induksi hipotesis ada formula C sedemikian sehingga: 1. Γ2 , A(x ), ∆ 1 → C dan Γ1 , C , ∆ 2 → D keduanya terbukti.
29
Jurnal Matematika Vol. 11, No.1, April 2008:25-31
2. V (C) ⊂V (Γ2 , A( x), ∆1 ) ∩[V (Γ1 , ∆2 ) ∪V (D)] Dari 1., Γ1 , ∃zA(z ), ∆ 1 → C terbukti seperti berikut Γ2 , A( x ), ∆ 1 → C (∃ →) , Γ2 , ∃zA(z ), ∆ 1 → C kemudian karena V ( A(x )) ⊂ V (∃zA(z )) , maka dari 2. dapat diperoleh sifat berikut: V (C) ⊂ V (Γ2 , ∃zAz, ∆1 ) ∩[V (Γ1 , ∆ 2 ) ∪V (D)] . Sehingga pada subkasus ini C merupakan interpolant dari Γ → D .
b. Partisi dari Γ, ∃zA( z ), ∆ ([Γ2 ], [Γ1 , Γ3 , ∃zA(z ), ∆ 2 ])
berbentuk
Perhatikan bagian dari P yang merupakan bukti dari sequent atas aturan inferensi (∃ →) tersebut, yaitu Γ, A(x ), ∆ → D , menurut induksi hipotesis ada formula C sedemikian sehingga: 1. Γ2 → C dan Γ1 , C , Γ3 , A( x ), ∆ → D keduanya terbukti. 2. V (C) ⊂ V (Γ2 ) ∩[V (Γ1 , Γ3 A( x), ∆) ∪V (D)] Dari 1., Γ1 , C , Γ3 , ∃zA( z ), ∆ → D dapat dibuktikan seperti berikut Γ1 , C , Γ3 , A( x ), ∆ → D (∃ →) , Γ1 , C , Γ3 , ∃zA( z ), ∆ → D kemudian karena V ( A(x )) ⊂ V (∃zA(z )) , maka dapat diperoleh sifat berikut: V (C) ⊂ V (Γ2 ) ∩ [V (Γ1 , Γ3 , ∃zA(z ), ∆) ∪ V (D)] . Sehingga pada subkasus ini C merupakan interpolant dari Γ → D .
c. Partisi dari Γ, ∃zA( z ), ∆ ([∆ 2 ,], [Γ, ∃zA(z ), ∆1 , ∆ 3 ])
berbentuk
Pada subkasus ini interpolant dari Γ → D dapat diperoleh dengan cara yang sama dengan cara pada subkasus b. yaitu partisi dari berbentuk Γ, ∃zA( z ), ∆ ([Γ2 ], [Γ1 , Γ3 , ∃zA(z ), ∆ 2 ]) • Kasus k›0 dan inferensi terakhir adalah (→ ∀) .
30
Interpolant dari Γ → D pada subkasus ini dapat diperoleh dengan cara yang sama dengan cara pada kasus k›0 dan inferensi terakhir adalah (→ ∃) . • Kasus k›0 dan inferensi terakhir adalah (∀ →) . Interpolant dari Γ → D pada subkasus ini dapat diperoleh dengan cara yang sama dengan cara pada kasus k›0 dan inferensi terakhir adalah (∃ →) . Dengan terbuktinya Teorema 4 maka teorema interpolasi pada Fl dan Flw hanyalah sebagai akibat langsung saja, yaitu dengan memilih Γ sebagai barisan formula dengan satu anggota saja, Γ2 = Γ dan Γ1, Γ3 sebagai barisan kosong.
Akibat 5. Teorema interpolasi berlaku pada logika predikat komutatif Fl dan Flw.
4. PENUTUP Dari pembahasan diperoleh kesimpulan bahwa teorema interpolasi berlaku pada logika predikat non-komutatif FL dan FLw, salah satu metode pembuktiannya adalah dengan memodifikasi konsep partisi pada metoda Maehara. Pada tulisan ini logika-logika yang dibahas tidak memuat konstanta ⊥. Analisisa sintaktik dari logika yang memuat konstanta tersebut dalam banyak hal membutuhkan aturan weakening. Untuk selanjutnya perlu diteliti apakah metode Maehara bisa dimodifikasi untuk membuktikan bahwa teorema interpolasi berlaku juga untuk logika predikat yang memuat konstanta ⊥ tetapi tak memuat aturan weakening.
5. DAFTAR PUSTAKA [1] Bayu Surarso, Teorema interpolasi untuk logika relevan positip R+, Jurnal sains & matematika (1999), Volume 7, Nomor 1, hal.1-6. [2] Bayu Surarso, Interpolation theorem for LDBCC and LDBCK, Jurnal
Bayu Surarso (Teorema Interpolasi untuk Logika Predikat Non-Komutatif Fl dan Flw)
Matematika dan Komputer (2000), Volume 3, Nomor 2, hal. 56-64. [3] Bayu Surarso, Interpolation theorem for Noncommutative standard Extensions of logic BB’I, Jurnal Matematika dan Komputer (2004), Volume 7, Nomor 2, hal. 36-41. [4] Bayu Surarso dan Marti Lestari, Teorema interpolasi untuk logikalogika predikat komutatif, manuskrip, segera diterbitkan pada Jurnal sains & matematika (2008), Volume 16, Nomor 4.
[5] Maehara S., Craig no interpolation theorem (dalam bahasa Jepang), Suugaku (1960/1961), Volume 12, hal. 235-237.
31
