Re: [其他] 邏輯中的"定義"該怎麼寫？
※ 引述《yueayase (scrya)》之銘言：
: 看了以上的討論, 我不知道type theory和邏輯符號語言之間的差別
type就是把變數分類 像程式語言裡把變數分成int, boolean一樣
標準的數理邏輯裡變數沒有分類
不過也有分類變數的理論 一般通稱做many-sorted logic
沒有type的理論只需要一個universe
有type的理論則每一個基本type都要有一個universe
然後因為還要定義product type, function type等等
所以大部分都還需引入category theory來處理
現在數學基礎的典範是集合論 是一個沒有type的理論
因此只有一個set theoretic universe
而自然數, 實數, ordinal number... 都可以定義成這個universe內的object
當然不認同這個數學基礎的大有人在...
: 因為我也曾經看過像logic set and recursion(http://ppt.cc/PatL)之類的書
: 裡面主要就是在說邏輯符號系統的language structure是怎樣
: 怎樣去interpret這些language意思
: 像之前提到的 A Mathematical Introduction to Logic也是在說這些東西
: 就不是很清楚type theory和這類書籍所說的有什麼差別
: 附帶一提,
: 這些東西又好像和computer science 的 formal language(eg: context-free grammar)
有關係 像語言學裡名詞 動詞 句子等都是一個type
不過搞context-free grammar的人比較喜歡叫他們part-of-speech
categorial grammar (一種更接近數理邏輯的文法) 則多稱之為type
: 或是 computation theory(eg: Turing machine <=> λ-calculus, decidability...)
這裡的確有些有趣的定理
例如 untyped lambda calculus 和 Turing machine 等價
(能計算所有computable function)
Typed lambda calculus 不能計算所有 computable function
但加入 fixed point operator 或允許 recursive type
就跟Turing machine等價了~
有興趣的話找本 programming language theory 的書都會有寫
: 有一些關聯
: 的確, 聽說作Artificial Intelligence的人, 早期好像也在研究logic...
嘖嘖 後來有所謂AI winter 所以現在AI已經不搞邏輯了...
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 128.12.24.136
※ 編輯: recorriendo 來自: 128.12.24.136 (04/18 14:40)
※ 編輯: recorriendo 來自: 128.12.24.136 (04/18 14:46)
→
04/18 15:03, , 1F
04/18 15:03, 1F
→
04/18 15:05, , 2F
04/18 15:05, 2F
→
04/18 15:05, , 3F
04/18 15:05, 3F
→
04/18 15:06, , 4F
04/18 15:06, 4F
→
04/19 02:13, , 5F
04/19 02:13, 5F
討論串 (同標題文章)
本文引述了以下文章的的內容：
完整討論串 (本文為第 5 之 5 篇)：