Sebuah
kalimat A adalah:
•
satisfiable jika S | = A untuk beberapa struktur S;
•
(logis) yang valid, dinotasikan | = A, jika S | = A untuk setiap struktur S;
•
difalsifikasi, jika tidak logis valid, yaitu jika memiliki counter-model.
Satisfiability
dan validitas dari setiap formula orde pertama
Sebuah
orde pertama formula A adalah:
•
A adalah satisfiable jika S, v | = A untuk beberapa struktur S dan beberapa
tugas variabel v di S.
•
(logis) yang valid, dinotasikan | = A, jika S, v | = A untuk setiap struktur S
dan setiap tugas v variabel dalam S.
•
difalsifikasi, jika tidak logis valid.
Misalkan
A = A (x1, ..., xn) berupa orde pertama Formula semua variabel bebas yang
berada di antara x1, ..., xn.
Kalimat
∃x1 ... ∃xnA (x1, ..., xn) adalah penutupan eksistensial dari A;
kalimat ∀x1 ... ∀xnA (x1, ..., xn) adalah penutupan universal A.
Klaim:
•
A (x1, ..., xn) adalah satisfiable IFF ∃x1
... ∃xnA (x1, ..., xn) adalah satisfiable.
•
| = A (x1, ..., xn) IFF | = ∀x1
... ∀xnA (x1, ..., xn).
Pertama-order contoh formula proposisional
Setiap substitusi seragam orde pertama formula untuk variabel proposisional dalam formula A proposisional menghasilkan formula orde pertama, yang disebut orde pertama contoh A.
Contoh: mengambil formula proposisional
A = (p ∧ ¬q) → (q ∨ p).
Seragam substitusi (5 <x) untuk p dan ∃y (x = y2) untuk q di A hasil dalam contoh pertama-order
((5 <x) ∧ ¬∃y (x = y2)) → (∃y (x = y2) ∨ (5 <x)).
Perhatikan, bahwa setiap orde pertama instance dari tautologi adalah logis valid. Jadi, misalnya,
| = ¬¬ (x> 0) → (x> 0)
dan
| = P (x) ∨ ¬p (x).
Satisfiability dan validitas kalimat: contoh
• ∃xP (x) adalah satisfiable: model adalah, misalnya, struktur bilangan bulat Z, di mana P (x) diartikan sebagai x + x = x.
• Namun, kalimat yang tidak valid: counter-model, struktur A, dimana P (x) diartikan sebagai himpunan kosong.
• Kalimat ∀x (P (x) ∨ ¬p (x)) adalah valid.
• Kalimat ∀xP (x) ∨ ∀x¬P (x) tidak valid, tetapi satisfiable. Menemukan model dan countermodel a!
• Kalimat ∃x (P (x) ∧ ¬p (x)) tidak satisfiable. Mengapa?
• Kalimat ∃x∀yP (x, y) → ∀y∃xP (x, y) adalah valid.
• Namun, kalimat ∀y∃xP (x, y) → ∃x∀yP (x, y) tidak valid. Cari countermodel a!
konsekuensi logis dalam logika urutan pertama
Kami memperbaiki sewenang-wenang bahasa orde pertama L.
Mengingat satu set L-rumus Γ, L-struktur S, dan tugas v variabel dalam S, kita menulis
S, v | = Γ
mengatakan bahwa S, v | = A untuk setiap A ∈ Γ.
Sebuah formula A secara logis dari satu set formula Γ, dinotasikan
Γ | = A,
jika untuk setiap struktur S dan variabel tugas v: VAR → S:
S, v | = Γ menyiratkan S, v | = A.
Perhatikan bahwa ∅ | = A IFF | = A
konsekuensi logis: contoh
• Jika A1, ..., An, B adalah prop. formula seperti itu A1, ..., An | = B, dan A0, B0 adalah orde pertama kasus A1, ..., An, B diperoleh dengan substitusi yang sama, maka A.
Sebagai contoh: ∃xA, ∃xA → ∀yB | = ∀yB.
• ∀xP (x), ∀x (P (x) → Q (x)) | = ∀xQ (x).
Catatan bahwa ini bukan sebuah contoh dari konsekuensi logis proposisi.
• ∃xP (x) ∧ ∃xQ (x) 6 | = ∃x (P (x) ∧ Q (x)).
Memang, struktur N0 diperoleh dari N dimana P (x) diartikan sebagai 'x bahkan' dan Q (x) diartikan sebagai 'x aneh' adalah kontra-Model:
N0 | = ∃xP (x) ∧ ∃xQ (x), sedangkan N0 6 | = ∃x (P (x) ∧ Q (x)).
konsekuensi logis: beberapa sifat dasar
kesetaraan logis dalam logika orde pertama memenuhi semua sifat-sifat dasar dari konsekuensi logis proposisi.
Secara khusus, berikut adalah sama:
1. A1, ..., An | = B.
2. A1 ∧ ··· ∧ An | = B.
3. | = A1 ∧ ··· ∧ An → B.
4. | = A1 → (A2 → ··· (An → B) ...).
Selanjutnya, untuk setiap orde pertama formula A dan t jangka yang bebas untuk substitusi untuk x di A:
1. ∀xA | = A [t / x]. 2. A [t / x] | = ∃
Pertama-order konsekuensi logis:
sifat yang lebih mendasar
1. Jika A1, ..., An | = B maka ∀xA1, ..., ∀xAn | = ∀xB.
2. Jika A1, ..., An | = B dan x tidak terjadi bebas dalam A1, ..., An kemudian A1, ..., An | = ∀xB.
3. Jika A1, ..., An | = B dan A1, ..., An adalah kalimat, maka A1, ..., An | = ∀xB, dan karenanya
A1, ..., An | = B, dimana B adalah salah penutupan universal B.
1. Jika A1, ..., An | = B [c / x], di mana c adalah simbol konstan tidak terjadi di A1, ..., An, kemudian A1, ..., An | = ∀xB (x ).
2. Jika A1, ..., An, A [c / x] | = B, di mana c adalah simbol konstan tidak terjadi di A1, ..., An, A, atau B, maka A1, ..., An, ∃xA | = B.
Pengujian konsekuensi logis dengan sistem deduktif
Pertama-order konsekuensi logis dapat dibangun menggunakan sistem deduktif untuk orde pertama logika.
Secara khusus, ekstensi dari Proposisi Semantic Tableau dan Pengurangan Alam, dengan aturan tambahan untuk bilangan, dapat dibangun yang sehat dan lengkap untuk logika orde pertama. Demikian juga, metode Resolusi dapat diperpanjang untuk suara dan sistem pemotongan lengkap untuk logika orde pertama.
Berbeda halnya proposisional, tidak ada metode ini dijamin untuk mengakhiri pencarian untuk derivasi, bahkan jika derivasi seperti itu ada. Hal ini terjadi, misalnya, ketika sebuah konsekuensi logis orde pertama gagal, tapi countermodel harus terbatas.
Bahkan, hal itu dibuktikan dengan Alonso Gereja pada tahun 1936 bahwa masalah apakah diberikan kalimat pertama-order berlaku (dan akibatnya, jika konsekuensi logis yang diberikan memegang) tidak algoritme dipecahkan.
Oleh karena itu, tidak ada suara, lengkap, dan selalu mengakhiri sistem deduktif untuk logika urutan pertama dapat dirancang.
Refrensi ;
http://www2.imm.dtu.dk/courses/02286/Slides/FirstOrderLogic%20-%20SatisfiabilityValidityLogicalConsequenceTrans.pdf
http://www2.imm.dtu.dk/courses/02286/Slides/FirstOrderLogic%20-%20SatisfiabilityValidityLogicalConsequenceTrans.pdf
