PENGERTIAN DAN CONTOH STATISFIABILITY.VALIDITY DAN LOGICAL CONSEQUNCE

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