P가 1차 언어로 표현 가능한 2항 술어라면 "∀x ∃y (P(x, y) ∧ ∀z (P(x, z) → y = z))"을 증명하면
"∀x ∀y (y = f(x) ↔ P(x, y))"을 만족시키는 1항 함수 "f"가 있다고 생각하잖아요.
그런데 제가 궁금한 것은
"이론을 전개할 때 외부에서 주어진 시그니처만을 써야 되는 것으로 아는데, 신규 함수 기호 f를 쓰는 건 정당한가?"
입니다. 2차 논리부터는 함수가 존재함을 표현할 수 있고, ∃-소거 규칙을 씀으로써 이론을 전개할 수 있다고 생각합니다.
그러나 1차 논리에서는 그럴 수가 없기 때문에 이런 해법을 생각해봤습니다:
Q가 1차 언어로 표현 가능한 2항 술어이고 FV(Q(x, y)) = {x, y}이면 Q(x, f(x))를 ∀y (P(x, y) → Q(x, y))로 번역하자!
그런데 귀납적으로 정의된 수열 같은 경우에는 도대체 어떻게 해야 될지 모르겠습니다. 알려주시면 감사하겠습니다.
그리고 이상한 부분 지적해주시면 감사히 받겠습니다.
제가 알기론 그냥 substitution인걸로 압니다
오!! 귀납적으로 정의된 수열은 그러면 어떻게 치환하나요?
Recursion theorem 같은 거 찾는 건가
제대로 정의됐다면 풀어쓸 수가 있어요. 중국인의 나머지정리 x mod a1 = m1이고 x mod a2 = m2인 x가 존재한다 는 mod 풀어서 (x = p1 * a1 + m1인 p1이 존재하고 x = p2 * a2 + m2인 p2가 존재하게끔 하는 x가 존재한다) 이런 느낌으로
귀납적으로 정의된 수열은 귀납형태만 줬다고 되는 게 아니고,기본적으로 괴델수를 써야 됩니다.
https://math.stackexchange.com/a/312915/704490
선생님 ㅠㅠ 정말 감사드립니다. 복 많이 받으시고 항상 행운이 따르시기를 기원합니다.
정말 죄송하지만 제가 읽으면 좋을 책 추천해주실 수 있나요?
첫 번째 질문은 extension by definition에 의해 해결돼요.
https://en.wikipedia.org/wiki/Extension_by_definitions