"p(x) is true for all x which are x∈A."
이 문장은 그냥
∀x∈A → p(x)
이렇게 써도 되는건가요? 잘못된 부분이 있는건가요?
∀x∈A: p(x) 이렇게만 쓰면 :가 such that 이니까 하나의 완성된 명제가 아니라
"for all x which are x∈A and makes p(x) true, ~~"
이런 조건문 앞에 붙는 조건으로써만 기능하게 되는 것 같아서요.
(수정)
찾아보니 ∀x∈A, p(x). 이렇게 중간에 쉼표 넣으면 오해 여지 없이 저렇게 해석 된다네요
이 문장은 그냥
∀x∈A → p(x)
이렇게 써도 되는건가요? 잘못된 부분이 있는건가요?
∀x∈A: p(x) 이렇게만 쓰면 :가 such that 이니까 하나의 완성된 명제가 아니라
"for all x which are x∈A and makes p(x) true, ~~"
이런 조건문 앞에 붙는 조건으로써만 기능하게 되는 것 같아서요.
(수정)
찾아보니 ∀x∈A, p(x). 이렇게 중간에 쉼표 넣으면 오해 여지 없이 저렇게 해석 된다네요
∀x ∈ A 뒤에는 잘세운식[well-formed formula]이 와야 되는데, → p(x)는 후건만 있고 전건이 없는 조건문이라서 ∀x ∈ A 뒤에 올 수 없어요. 전 메타매스(Metamath)처럼 쉼표 없이 ∀x ∈ A p(x)와 같이 쓰는데, 린(Lean)은 쉼표를 써요.
와 감사합니다!!
그리고 메타매스에서는 ∀x ∈ A φ → ψ가 (∀x ∈ A φ) → ψ를 가리키는 반면에, 린에서는 ∀x ∈ A, φ → ψ가 ∀x ∈ A, (φ → ψ)를 가리켜요. 교재나 컴퓨터 언어마다 정량어와 논리 연결어 중 무엇이 더 우선하는지가 달라요.
궁금한 점 또 생기면 여기서 질문해 주세요!