命題邏輯的語義
稱為一個(gè)推理(sequent)，如果使用Natural Deduction的方式進(jìn)行推導(dǎo)(derivation)鸥拧，可以由
得到
党远，那么這個(gè)推理是有效的。
定義：
- 真值集合為
富弦，T為真沟娱，F(xiàn)為假
- 一個(gè)公式的估值(valuation)或模型(model)是指為公式中的每一個(gè)原子賦一個(gè)真值集合中的值
對于這一公式而言，
僅考慮p和q的真假值腕柜，并不考慮p和q代表什么济似。
soundness和completeness
對于合理的推理，能否在真值表的語義下媳握，保證當(dāng)
為T時(shí)碱屁，
不可能是F。
若中蛾找，當(dāng)全
部成立時(shí)，
也成立赵誓，則稱
語義蘊(yùn)含
打毛。
soundness：若是合理的，則$$
completeness：若俩功，則是
合理的
證明：太長不看
實(shí)際是想說：一個(gè)邏輯系統(tǒng)需要滿足soundness和completeness的一致性幻枉。
一階邏輯
signature：三個(gè)部分
分別是函數(shù)名、常數(shù)名诡蜓、謂詞名
一般省略熬甫，因?yàn)槠淇煽醋鳠o參數(shù)的
一階邏輯的公式中，兩類：
- 項(xiàng)：
蔓罚，用于表達(dá)對象object
- 公式：
一階邏輯的語義：
proof-based logic：給出一個(gè)operative的椿肩，通過Natural Deduction方式的證明
優(yōu)點(diǎn)：一旦找到一個(gè)證明方式成功推導(dǎo)，即可證明
缺點(diǎn)：難以證明豺谈，需要遍歷全部可能的證明方式郑象，才能夠得到結(jié)論
semantic-based logic：通過真值表驗(yàn)證的正確性
優(yōu)點(diǎn)：更容易證明，只要找到一個(gè)左側(cè)為T的assignment茬末，而右側(cè)為F即可
缺點(diǎn)：想要證明更困難厂榛，需要遍歷全部的真值組合。
一階邏輯evaluate的難點(diǎn)：每一個(gè)變量都是一個(gè)可能的具體值的占位符
對，每個(gè)x击奶，
都為真辈双，則最終取值為真
對，找到一個(gè)x0柜砾，
為真湃望，則最終取值為真
如果的結(jié)構(gòu)為
等（解析樹根節(jié)點(diǎn)），那么最終的真值可以按照各謂詞公式的真假局义，遵循命題邏輯中的連接詞運(yùn)算進(jìn)行求解
問題進(jìn)一步轉(zhuǎn)為求解的真值喜爷。對此需要明確謂詞常量的含義和term的含義。
的模型
：
- 非空集合A萄唇，所有可能的具體取值全體集合
- 對每一個(gè)對無參函數(shù)
檩帐，
有一個(gè)A中對應(yīng)的取值
- 對每一個(gè)元數(shù)>0的函數(shù)f，
仲吏，A的n元組集合到A中某元素的映射
- 對每一個(gè)元數(shù)n>0的謂詞常量P领舰，
是
的子集。
例泛源，，R是二元謂詞忿危，F(xiàn)是一元謂詞达箍，
包含：
A={a,b,c}，具體取值的全體
無非0元函數(shù)
-
是
的子集铺厨。
缎玫，則
可為
環(huán)境：將變量映射到具體值的look-up table
對于在l環(huán)境下的滿足性定義：
-
，根據(jù)l字典洼裤，將全部變量換為具體值邻辉，此時(shí)
均在
中
-
：將公式
中的每個(gè)x分別替換為模型A中的具體值，然后在根據(jù)字典腮鞍，將其他變量換為具體值值骇，如果每一次的替換都能滿足，則
- 存在性缕减，類似上條雷客，但對約束變量x的替換只需要找到一個(gè)在A中的具體值即可。
- 或且非蘊(yùn)含的滿足性分別檢查單個(gè)公式的滿足性得到T和F桥狡，再按照命題邏輯聯(lián)結(jié)詞真值表得到T和F搅裙。
給出模型解釋的時(shí)候皱卓，需要使用擴(kuò)展簽名，否則將會出現(xiàn)bug：
用解釋的方式定義：
函數(shù)常量alma部逮，
在解釋空間中取值替換變量y（例如a）娜汁，替換變量：
，此時(shí)出現(xiàn)問題兄朋，
沒有定義掐禁，因?yàn)镮nterpretation的domain必須是
的子集。
于是擴(kuò)展為
颅和，此處的*是abc實(shí)際值的名字傅事，
并且，原有定義下為真峡扩，當(dāng)且僅當(dāng)對所有的
蹭越，
為真
改為：
當(dāng)且僅當(dāng)對所有的，
為真
這一解釋就沒有問題了教届。
Logic in CS中的定義下响鹃，雖然未考慮。對于模型的映射直接是
一個(gè)全局的具體取值A(chǔ)
函數(shù)：一個(gè)value案训，來源于A
謂詞：為真的元組組合买置，元組元素來源于A
其實(shí)是相同的，因?yàn)楹瘮?shù)和謂詞就是signature的組成部分强霎。
檢查任意性和存在性時(shí)忿项，
變量：直接替換為A中的元素，相當(dāng)于隱性定義了對于非signature中的元素城舞，映射的結(jié)果是元素值自身倦卖。
在謂詞邏輯中是重載的，對模型而言表示滿足椿争，對兩個(gè)formula而言表示語義蘊(yùn)含。
for all
一個(gè)模型滿足一個(gè)公式組，當(dāng)且僅當(dāng)這一模型滿足公式組中的每一個(gè)公式掸茅，如果這一公式組的每個(gè)模型都還滿足另一個(gè)公式,那么這個(gè)公式組蘊(yùn)含這一公式椅邓。
存在一個(gè)模型，使得昧狮，則
可滿足
一階邏輯無法表達(dá)傳遞閉包：
能否找到一個(gè)公式景馁，公式中只包含兩個(gè)自由變量u和v，一個(gè)謂詞關(guān)系R逗鸣，通過這個(gè)公式可以表達(dá)：
這樣的R無法找到合住，這樣的公式是無止盡的绰精。
一階邏輯公式的合理性是undecidable的：給定一個(gè)FOL公式，
是否成立透葛？
這個(gè)問題無法解答笨使。
==》FOL的滿足性問題也是undecidable的
證明：是合理的 當(dāng)且僅當(dāng)
是不可滿足的（可滿足：存在一個(gè)interpretation I，
