제가 정수론을 배우면서 느낀 건데요,

1차 논리는 프로그래밍으로 치면 기계어처럼 너무 저수준이라서,

기계어로 코딩하지 않듯이 1차 논리를 바로 쓰는 것 같지는 않아보입니다.

그러나 1차 논리의 좋은 성질을 쓰기 위해서,

우리가 이룬 정의와 정리와 증명을 어떻게 해야 1차 논리로 컴파일해야 되는지가 궁금합니다.

(1) '유한수열은 어떻게 1차논리의 언어로 컴파일 되는지'와

(2) '귀납적으로 정의된 수열은 어떻게 1차논리의 언어로 컴파일 되는지'조차

모르는 저에게 책을 추천해주셔도 감사하고요, (1)과 (2)의 답을 해주셔도 감사하겠습니다.

정수론의 논의 영역은 ZFC의 논의 영역과 다르기 때문에 재귀정리를 쓰면 위험할 것 같아서요.

실은 제가 증명보조기를 만드는 게 꿈인데,

그 증명보조기의 문법을 고안하기 위해 정수론 노트 정리를 하다가,

"내가 만들 증명보조기가 1차 논리만 다룬다면 안 돌아가네"라는 걸 깨달아서 드리는 질문입니다.

읽어주셔서 감사합니다.