[請益] 表示 Reflexive Transitive Closure

[freef1y3 ( )]

請問 Reflexive Transitive Closure 是否能用一階邏輯表示呢？

也就是說，是否能給出一個一階 Theory T 來描述 Relation R 及 R*
使得在所有 T 的 Model 中，R* 都是 R 的 Reflexive Transitive Closure？

Google 了一下好像都說不行
但是我想了一下 (好吧其實想很久) 好像可以這樣表示？

∀x∀y (R*(x,y) <=> ((∃p (R(x,p) Λ R*(p,y))) Ｖ x=y))

也就是說，若 R*(x,y) 成立，要嘛 x=y，
否則就是有一個 p 使得 R(x,p) 和 R*(p,y) 都成立
再繼續追 R*(p,y)，若 R*(p,y) 成立，要嘛 p=y，
否則就是有一個 p2 使得 R(p,p2) 和 R*(p2,y) 都成立
這樣追下去，應該就可以確保：

若 R*(x,y) 成立，
則找的到 p1,p2,...,pi 使得 R(x,p1), R(p1,p2), ..., 一直到 R(pi,y) 都成立
因此 R* 是 R 的 Reflexive Transitive Closure

不知道這樣的論述有什麼問題呢？

--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 140.113.250.41
※ 文章網址: https://www.ptt.cc/bbs/logic/M.1441097707.A.533.html
推 MathTurtle: 問題就在你說的"這樣追下去，應該就可以確保"
→ MathTurtle: 這裡就不是用一階邏輯可以表達的
→ freef1y3: 可是那只是我用來解釋的自然語言，沒有包含在邏輯式內
→ freef1y3: 還是那條邏輯式有用到什麼非一階邏輯的東西呢？
→ freef1y3: 或者是這種可能導致無窮展開的邏輯式就不屬於一階邏輯？
推 MathTurtle: 因為你給的式子不是定義啊 ... R*出現在biconditional
→ MathTurtle: 的兩邊
→ MathTurtle: 要把它弄成定義 你會需要recursion之類的東西
推 turboho: 你給的 sentence 不等價於 R* 是 R 的 ref. trns. clos.
→ turboho: 考慮 R*(x,y) for every x,y and R(x,y) for x=y
推 turboho: 在 stackexchange http://goo.gl/u7X5Iu 有人問過了，下
→ turboho: 面有人回答，你可以去看看
→ freef1y3: 啊 真的耶! 感謝t大解惑~