수리논리 Robinson Arithmetic Q 질문

[익명(45.33)]

'Q에서 모든 x에 대해, 0+x=x가 증명불가능하다'를
증명하는 과정에서 자연수집합하고 a,b를 놓는데 왜
Sa=a야??
기초 model theory라는데 읽으면 도움될 책있을까

[러셀(salvaveritate)]

어느 책에서 Sa=a라고 설명함? 이런 질문을 할 때는 전문을 전부 옮겨주거나 출처를 명시해 주자

[러셀(salvaveritate)]

S에 대한 통상적인 정의상 Sa=a인 건 말이 안 되는 소리인데…

[익명(220.117)]

Peter Smith의 Introduction to Godel Theorem 2의 Chapter 10입니다. 사진도 곧 첨뷰하겠습니다

[익명(45.33)]

사진은 2번째거 1번째거 순서입니다

[러셀(salvaveritate)]

아.. 말 그대로 model theory 관련 책 하나를 찾아서 ‘unintended interpretation’에 관한 단락을 찾아보면 이해가 될 것 같네요! 또는 löwenheim-skolem theolem에 관해 다루는 글들을 찾아봐도 될 것 같아요.

[러셀(salvaveritate)]

저기에서 S*는 원래 계승 함수 S와 달리, 임의의 (어쩌면 수가 아닌) 존재자 a, b를 도메인에 포함해서 S*a=a를 내는 그런 함수로 도입된 건데, 그래서 Q 하의 모든 0+x=x꼴의 문장은 참이지만 ∀x(0+x=x)는 참이 아니게 하는 그런 해석 함수가 있다는 얘기인데요,

[러셀(salvaveritate)]

이게 문제인 건, ∀x(0+x=x)가 Q의 공리이고(따라서 참이고), ⊨는 진리 보존적이므로 Q ⊨ ∀x(0+x=x)인데, Q(즉, 산BA의 구문론)만으로는 ∀x(0+x=x)임을 보여줄 수 없다는 얘기네요.. BA의 구문론에서 소개되는 도식들로 이걸 증명 못 한다는 말인가봐요.

[러셀(salvaveritate)]

*도식이 아니라 추론 규칙, 산BA가 아니라 BA

[익명(45.33)]

역시 믿고보는 러셀좌 감사합니다!!

[김민성태팬클럽회장(thecoqproofassistant)]

[김민성태팬클럽회장(thecoqproofassistant)]

훌륭한 설명의 표본이네요 :)

[익명(121.181)]

Q에서 '모든 x에 대해서 x+0 = x'는 공리 아님?