답글 달아주셔서 감사합니다.
답글 달아주신 걸 보고 찾아보니, 제가 각기 다른 보편양화사를 예화할 때 꼭 서로 다른 대체예가 들어가야 한다고 잘못 생각했었습니다. 회사 직장 동료 예시도 그런 생각에서 나왔던 잘못된 반례였던 것 같네요.
(∀x)(∀y)(Rxy & Ryx)로부터는 (∀x)(∀y)(∀z)[(Rxy & Ryz) → Rxz]를 거론할 필요조차 없이 그냥 바로 (∀x)Rxx가 도출되는 것 같습니다.
- (∀x)(∀y)(Rxy & Ryx) (전제)
- (∀y)Ray (1, ∀제거, x:=a)
- Raa (2, ∀제거, y:=a)
- (∀x)Rxx (3, ∀도입)
(혹시 증명에 틀린 부분이 있다면 집어주시면 감사하겠습니다.) 다만 이렇더라도 회슬레가 의도하는 "상호주관성이 반성성을 함축하고 있다"는 생각이 별로 잘 표현되지 않는 것 같습니다. 저 한 진술에서 반성성이 바로 따라나온다면 굳이 이행적인 관계는 왜 필요한가 하는 의문이 남아서요.
한편
말씀대로 대칭성, 이행성에 연쇄성을 추가하니 회슬레 자신이 제시한 버전보다 깔끔한 것 같습니다. 더구나 연쇄성과 더불어 대칭성과 이행성을 모두 사용해야 반성성이 도출된다는 점 때문에 왜 굳이 대칭적이면서도 이행적인 관계가 필요한지도 설명되는 것 같습니다.
1. (∀x)(∀y)(Rxy→Ryx) (대칭성)
2. (∀x)(∃y)Rxy (연쇄성)
3. (∀x)(∀y)(∀z)[(Rxy&Ryz)→Rxz] (이행성)
4.1. (∃y)Ray (2, ∀제거, x:=a)
4.1.1. Rab (4, ∃제거, y=b)
4.1.2. Rab→Rba (1, ∀제거)
4.1.3. Rba (5, 6, →제거)
4.1.4. Rab&Rba (5, 7, &도입)
4.1.5. (Rab&Rba)→Raa (3, ∀제거)
4.1.6. Raa (8, 9, →제거)
4.2. Raa (∃도입?)
5. (∀x)Rxx (10, ∀도입)
좋은 제안 주셔서 감사합니다. 덕분에 회슬레가 무슨 얘기를 하고 싶어했는지 보다 잘 이해하게 된 것 같네요!
Ps. 양화사의 제거와 도입에 대해서는 (원래 조건문과 관련해서 제시된 표기법인) 다음의 표기법을 활용해봤습니다.
Ps. Ps. 보통 양화사를 예화해서 제거한 다음에 도출하려는 식이 나오면 다시 양화사를 도입하는 걸로 알고 있는데, 위처럼 중간에 재도입할 존재양화사가 아예 없어져 버리는 경우는 통상적으로 어떻게 처리하나요? 
알려주시면 감사하겠습니다.