술어 펑터 논리

수학 논리학에서 술어 펑터 논리(PFL)는 순수 대수적 수단, 즉 정량화된 변수를 사용하지 않고 1차 논리(일명 술어 논리학)를 표현하는 여러 가지 방법 중 하나이다. PFL은 조건별로 작동하는 술어 펑터(또는 술어 수식어)^[1]라고 불리는 소수의 대수적 장치를 사용한다. PFL은 대부분 논리학자, 철학자 윌러드 콰인의 발명품이다.

동기

이 조의 출처뿐만 아니라 이 조의 대부분의 출처는 Quine(1976년)이다. Quine은 PFL을 1차 논리 대수화 방법으로서 Boolean 대수학에서 명제 논리학을 대수화하는 방법과 유사한 방법으로 제안했다. 그는 PFL을 아이덴티티와 함께 1차 로직의 표현력을 정확히 갖도록 설계했다. 따라서 PFL의 변광성은 정확히 해석된 술어 문자가 없는 1차 논리학의 변광성이다. 두 로직 모두 건전하고 완전하며 해석할 수 없는 것이다. Quine은 그의 인생의 마지막 30년 동안 논리와 수학에 대해 출판한 대부분의 작품들은 어떤 식으로든 PFL을 건드렸다.^{[citation needed]}

Quine은 친구 Rudolf Carnap의 글에서 "functor"를 취했는데, 이 글을 철학 및 수학 논리에 가장 먼저 채용하여 다음과 같이 정의하였다.

"functor라는 단어는 수입에서는 문법적으로, 서식지에서는 논리적으로... 주어진 문법적 종류의 표현을 하나 이상 붙여서 주어진 문법적 종류의 표현을 만들어 내는 기호다.(Quine 1982: 129)

1차 논리학을 대수화하는 PFL 이외의 방법에는 다음이 포함된다.

• 알프레드 타르스키와 그의 미국 학생들의 원통형 대수학. 버네이스(1959)에서 제안된 단순화된 원통형 대수학으로 Quine은 "predicate functor"라는 문구의 첫 번째 용어가 포함된 논문을 쓰도록 했다.
• 폴 할모스의 폴리아디치 대수학. 경제적 원리와 공리 때문에 이 대수학은 PFL과 가장 유사하다.
• 관계 대수학은 3개 이상의 정량자의 범위에 놓여 있는 원자 공식이 없는 공식으로 구성된 1차 논리학의 파편을 대수화한다. 그러나 그 단편은 Peano 산술과 자명한 집합 이론 ZFC에 충분하다. 따라서 PFL과 달리 관계 대수학은 비완전하다. 1920년경부터 관계 대수학에 관한 대부분의 작업은 타르스키와 그의 미국 학생들이 했다. 관계 대수학의 힘은 PFL에 관한 세 가지 중요한 논문, 즉 베이컨(1985년), 쿤(1983년), 콰인(1976년) 이후 출판된 모노그래프 타르스키와 기반트(1987년)가 되어서야 명백해졌다.
• 결합 논리학은 다른 결합기 또는 함수인 도메인이 다른 결합기 또는 함수인 상위 순서 함수 및 아직 다른 결합기 범위를 기반으로 한다. 따라서 결합논리는 집합이론의 표현력을 갖음으로써 1차 논리의 범위를 넘어서게 되는데, 이것은 결합논리를 역설에 취약하게 만든다. 반면에 술어 펑터는 술어(용어라고도 함)를 술어로 간단히 매핑한다.

PFL은 거의 틀림없이 이러한 형식적 표현들 중에서 가장 단순하지만, 또한 가장 적게 쓰여진 형식이기도 하다.

Quine은 러시아 논리학자 Moses Schönfinkel의 설립논리학 논리의 반 헤이제노르트 (1967)에 의한 번역에 대한 소개로 증명된 전투논리에 평생 매료되었다. Quine이 본격적으로 PFL에 착수했을 때, 1959년, 콤비네이션 논리는 다음과 같은 이유로 일반적으로 실패로 간주되었다.

• 다나 스콧이 1960년대 후반에 결합논리의 모델론을 쓰기 시작할 때까지, 거의 하스켈 카레와 그의 제자들, 벨기에의 로버트 페이즈만이 그 논리학을 연구했다.
• 만족스러운 전투논리의 자명한 공식은 오는 것이 더디었다. 1930년대에는 일부 형식적인 결합 논리가 일관성이 없는 것으로 밝혀졌다. Curry는 또한 투쟁적 논리 특유의 Curry 역설도 발견했다.
• 결합논리와 같은 표현력을 가진 람다 미적분은 우월적 형식주의로 비쳤다.

쿤의 공식화

이 절에서 설명하는 PFL 구문, 원시성 및 공리는 대부분 스티븐 쿤(1983)의 것이다. 펑커스의 의미론은 Quine's(1982년)이다. 이 항목의 나머지 부분에는 베이컨(1985)의 일부 용어가 포함되어 있다.

구문

원자 용어는 I와 S를 제외하고 대문자 라틴어 문자로, 그 뒤에 그 정도라고 불리는 숫자 위첨자 또는 인수 목록으로 알려진 통합된 소문자 변수에 의해 이루어진다. 용어의 정도는 술어 문자에 따른 변수의 수와 동일한 정보를 전달한다. 원자 용어 0은 부울 변수 또는 진실 값을 의미한다. 나는 항상 2의 정도여서 그렇게 표기되지 않는다.

"합성"(이 단어는 Quine's)의 술어인 functors는 모두 단음절이며 PFL에 특유한 것으로 Inv, inv, +, +, p 용어는 원자용어 또는 다음의 재귀적 규칙에 의해 생성된다. 만약 τ이 용어라면, Inv,, inv,, ∃τ, +τ, pτ은 용어다. 위첨자 n, n 자연수 > 1을 가진 펑터는 해당 펑터의 연속 적용(반복)을 의미한다.

공식은 용어 또는 재귀 규칙에 의해 정의된다: α와 β가 공식이라면 αβ와 ~(α)도 마찬가지로 공식이다. 따라서 "~"는 또 다른 단음이의 functor이며, 결합은 유일한 dynadic 술어 functor이다. Quine은 이 functor들을 "알레틱"이라고 불렀다. ~의 자연적 해석은 부정이다; 결합의 해석은 부정과 결합되었을 때 기능적으로 완전한 결합의 집합을 형성하는 결합이다. Quine이 선호하는 기능적으로 완결된 세트는 접속사와 부정이었다. 따라서 결합된 용어는 결합된 것으로 간주된다. 표기법 +는 베이컨(1985)이고, 다른 표기법은 모두 퀴네(1976; 1982)이다. PFL의 음극 부분은 Quine의 부울 용어 스키마타(1982)와 동일하다.

잘 알려진 바와 같이, 두 개의 알레르딕 펑터는 다음과 같은 구문과 의미론을 가진 단일 다이오드 펑터로 대체될 수 있다: α와 β가 공식이라면, (αβ)는 의미론이 "not (α 및/또는 β)"인 공식이다(NAND와 NOR 참조).

공리와 의미론

Quine은 PFL에 대한 공리화나 증명 절차를 제시하지 않았다. 쿤(1983년)에서 제안된 두 가지 중 하나인 PFL의 다음과 같은 공리화는 간결하고 설명하기 쉬우나 자유 변수를 광범위하게 사용하므로 PFL 정신에 완전한 정의를 내리지는 못한다. 쿤은 자유 변수와 함께 분사하는 또 다른 공리화를 주지만, 그것은 설명하기 어렵고 정의된 펑터를 광범위하게 사용한다. 쿤은 그의 PFL 공리화 두 가지 모두 건전하고 완전하다는 것을 증명했다.

이 구간은 원시 술어 펑커와 몇 가지 정의된 술어를 중심으로 만들어졌다. 음의 functors는 음과 itives 또는 ∨ 중 하나인 송신 논리에 대한 공리 집합에 의해 공리화될 수 있다. 마찬가지로, 모든 보초적 논리의 토폴로지는 공리로 간주될 수 있다.

각 술어에 대한 Quine의 (1982) 의미론은 추상화(set builder 표기법) 측면에서 아래에 명시되어 있으며, 쿤(1983년)의 관련 공리 또는 Quine(1976년)의 정의가 그 뒤를 따르고 있다. 표기법${\displaystyle }${ ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle n_{}}$: ${\displaystyle F}$ x ${\displaystyle {1\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle n_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle \{x_{1}\cdots x_{n}:$$Fx_{1}\cdots x_{n}\}\}}$은(는) 원자 공식 F ${\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle x_{}}$ .${\displaystyle Fx_{1}\cdots x_{n}$을(를) 만족하는 n-tupet 집합을 의미한다$$.$}$

• ID I는 다음과 같이 정의된다.

${\displaystyle IFx_{1}x_{2}\cdots x_{n}\좌우타로우 Fx_{1}{1}x_{1}\cdots x_{n}\좌우타로우 Fx_{2}x_{2}\cdots x_{n}.}$

아이덴티티는 반사성(Ixx), 대칭성(Ixy→Iyx), 전이성((Ixy∧Iyz) → Ixz)이며 대체 속성에 순응한다.

${\displaystyle (Fx_{1}\cdots x_{n}\land Ix_{1}y)\오른쪽 화살표 Fyx_{2}\cdots x_{n}.}$

• 패딩 +는 인수 목록의 왼쪽에 변수를 추가한다.

${\displaystyle \ +F^{n}\\\overset {\underset {\mathrm {def}{}}{}}{}}\{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle +Fx_{1}\cdots x_{n}\좌우타로우 Fx_{2}\cdots x_{n}.}$

• 자르기, ∃은 인수 목록에서 가장 왼쪽 변수를 지운다.

${\displaystyle \exists F^{n}\\\overset {\underset {\mathrm {def}{}}{}}{}}\{x_{2}\cdots x_{n}}\exists x_{1}}}\exists x_{1}}F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle Fx_{1}\cdots x_{n}\오른쪽 화살표 \exists Fx_{2}\cdots x_{n}.}$

자르기 기능을 통해 두 가지 유용한 정의 펑커:

• 반사, S:

${\displaystyle SF^{n}\\\overset {\underset {\mathrm {def}{}{}}{}}{}}\{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}}\cdots x_{n}\}.}$

${\displaystyle SF^{n}\좌우타로우 \exists IF^{n}.}$

S는 어떤 유한도 이상의 모든 용어에 대한 반사성의 개념을 일반화한다.N.B:S와 혼동해서는안 된다 결합자 S는 결합논리의 원시.

• 데카르트 제품, $\times {\displaystyle }$ ${\displaystyle \time}$;

${\displaystyle F^{m}\time G^{n}\왼쪽 오른쪽 화살표 F^{m}\exists ^{m}G^{n}}}$

여기서만, Quine은 카르테시안 제품에 대한 이 infix 표기법이 수학에서 매우 잘 확립되어 있기 때문에 infix 표기법을 채택했다. 데카르트 제품은 다음과 같이 재충전 접속이 가능하다.

${\displaystyle F^{m}x_{1}\cdots x_{m}G^{n_{1}\cdots x_{n}\{n}\cdots x_{n}\time G^{n}}x_{1}\cdots x_{1}\cdots x_{n}.}$

중복 변수 쌍을 맨 왼쪽으로 이동하도록 연결된 인수 목록을 다시 정렬한 다음 S를 호출하여 중복을 제거하십시오. 이것을 필요한 만큼 반복하면 길이 max(m,n)의 인수 목록이 나온다.

다음 세 개의 functor는 임의로 인수 목록을 재정렬할 수 있다.

• 주요 반전인 Inv는 인수 목록의 변수를 오른쪽으로 회전시켜 마지막 변수가 첫 번째 변수가 된다.

${\displaystyle \operatorname {Inv}F^{n}\\overset {\underset {\mathrm {def}{}}{}}{}}\{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}x_{1}\cdots x_{n-1}\}.}$

${\displaystyle \operatorname {Inv}Fx_{1}\cdots x_{n}\좌우 이동 Fx_{n}x_{1}\cdots x_{n-1}.}$

• 사소한 반전, inv는 인수 목록의 처음 두 변수를 교환한다.

${\displaystyle \operatorname {inv}F^{n}\\overset {\underset {\mathrm {def}{}}{}}{}}}{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.}$

${\displaystyle \operatorname {inv}Fx_{1}\cdots x_{n}\cdots x_{n}\좌우타로우 Fx_{2}x_{1}\cdots x_{n}.}$

• 순열 p는 인수 목록의 두 번째에서 마지막 변수를 왼쪽으로 회전시켜 두 번째 변수가 마지막 변수가 된다.

${\displaystyle \pF^{n}\\overset {\underset {\mathrm {def}{}}{}}{}}\{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.}$

${\displaystyle pFx_{1}\cdots x_{n}\왼쪽 화살표 \operatorname {Inv} \operatorname {inv}Fx_{3}\cdots x_{n}x_{2}.}$

n개의 변수로 구성된 인수 목록이 주어진 경우 p는 마지막 n-1 변수를 자전거 체인처럼 암묵적으로 처리하며 각 변수는 체인의 링크를 구성한다. 하나의 p 적용은 하나의 링크에 의해 체인을 진전시킨다. k 연속 적용 p to F는ⁿ k+1 변수를 F의 두 번째 인수 위치로 이동시킨다.

n=2일 때 Inv와 inv는 x와₁ x만₂ 교환한다. n=1일 때는 효과가 없다. 따라서 p는 n < 3일 때 아무런 효과도 없다.

쿤(1983년)은 메이저 역전과 마이너 역전을 원시적인 것으로 받아들인다. 쿤의 표기법 p는 inv에 해당한다; 그는 Permutation과 유사성이 없기 때문에 그것에 대한 공리가 없다. Quine(1976년)에 이어 p가 원시적, Inv와 inv는 +, ∃, 반복 p의 비종교적 조합으로 정의될 수 있다.

다음 표는 펑거스가 그들의 주장의 정도에 어떻게 영향을 미치는지 요약한 것이다.

표현	정도
${\displaystyle p;\operatorname {Inv};\operatorname {inv};\lnot ;\I}$	잔돈 없음
${\displaystyle +F^{n-1};\exists F^{n+1};\ SF^{n+1}.$	n
${\displaystyle \알파 ^{m}\베타 ^{n};\F^{m}\times G^{n}}}}$	max(m, n)

규칙.

술어 문자의 모든 예는 유효성에 영향을 미치지 않고 같은 정도의 또 다른 술어 문자로 대체될 수 있다. 규칙은 다음과 같다.

• 모드스 폰스;
• α와 β를 x ${\displaystyle {1\mathrm{}}_{}}$ ${\$}가 나타나지$$ 않는 PFL 공식으로 한다. 그런 다음${\displaystyle }$(${\displaystyle \alpha }$ α ${\displaystyle \wedge }$ F ${\displaystyle x}$ ${\displaystyle {1\mathrm{}}_{}}$.${\displaystyle }$.${\displaystyle }$. . ${\displaystyle {}_{}}$ ${\displaystyle n_{}}$)${\displaystyle }$→ ${\displaystyle \beta }$ ${\displaystyle (\alpha \land Fx_{1}...$$x_{n}\rightarrow \beta }}$은$({\displaystyle \alpha }$ theorem ${\displaystyle \mathrm{\exists }}$ F ${\displaystyle {x\mathrm{}}_{}}$ 2${\displaystyle }$.${\displaystyle }$. x ${\displaystyle n_{}}$) →${\displaystyle \beta }$ ${\displaystyle (\alpha \land \exist Fx_{$$2$}...$x_{n}\rightarrow \beta }$도 마찬가지로 PFL 정리다$$.

유용한 결과

PFL을 공리화하는 대신, Quine(1976)은 후보 공리로서 다음과 같은 추측을 제안했다.

$\displaystyle \exists I}$

n-1 연속적인 p 반복은 현상유지를 복구한다.

${\displaystyle F^{n}\왼쪽 오른쪽 화살표 p^{n-1}F^{n}}}}$

+와 ∃는 서로를 섬멸한다.

${\displaystyle {\displaysty}F^{n}\오른쪽 화살표 +\exists F^{n}\\F^{n}\왼쪽 화살표 \exists +F^{n}\end{case}}}}$

부정은 +, ∃, p에 걸쳐 분포한다.

${\displaystyle {\begin{case}+\lnot F^{n}\왼쪽 화살표 \lnot +F^{n}\\lnot \loth F^{n}\p\lot F^{n}\lot F^}\loteflot PF^{n}\n}}}}}}}:{n}}}}}}}}}}}}}}}}}}}}}}}오른쪽 화살표 왼쪽 화살표 왼쪽 화살표 \lothroward}}}}}}}}}}}}}$

+ 및 p는 접속사를 통해 분배된다.

${\displaystyle {\begin}+(F^{n}G^{m})+왼쪽 화살표(+F^{n}+G^{m})\p(F^{n}G^{m})\왼쪽 화살표(p^{n}pG^{m}}\case}}}}}}}}}}}}}}}}$

정체성은 다음과 같은 흥미로운 암시를 가지고 있다.

${\displaystyle IF^{n}\오른쪽 화살표 p^{n-2}\exists p+F^{n}}$

Quine은 또한 이 규칙을 추측했다. α가 PFL 정리라면 pα, +α, ${\displaystyle \mathrm{\neg }\mathrm{}\alpha }$ ${\displaystyle \lnot \exists \lnot \alpha }$도 마찬가지다$.$

베이컨의 작품

베이컨(1985)은 조건부, 부정, 아이덴티티, 패딩, 메이저와 마이너 역전을 원시, 그리고 정의된 대로 크로핑을 취한다. 위와 다소 다른 용어와 표기법을 채택한 베이컨(1985)은 PFL의 두 가지 공식에 대해 설명한다.

• 프레더릭 피치 스타일의 자연 공제 공식. 베이컨은 이 제형이 건전하고 완전하다는 것을 증명한다.
• 베이컨이 주장하지만 증명하지는 않는 자명적인 공식으로, 앞의 공식과 동등하다. 이러한 공리들 중 일부는 베이컨의 표기법에서 재조명된 퀴네 추측일 뿐이다.

베이컨 또한:

• Sommers의 용어 논리(1982)에 대한 PFL의 관계를 논의하고, Lockwood의 Sommers 부록에서 제안된 구문을 사용하여 PFL을 다시 작성하면 PFL을 "읽고, 사용하고, 가르치기" 쉽도록 해야 한다고 주장.
• Inv 및 inv의 그룹 구성 구조 터치
• 보초적 논리, 단음절 술어 논리, 모달 논리 S5, (무)영원한 관계의 부울 논리는 모두 PFL의 단편이라고 언급한다.

1차 논리부터 PFL까지

다음 알고리즘은 Quine(1976: 300-2)에서 채택되었다. 1차 로직의 폐쇄적인 공식에 따라, 먼저 다음을 수행한다.

• 모든 술어 문자에 그 정도를 나타내는 숫자 첨자를 부착한다.
• 모든 보편적 정량자를 실존적 정량자와 부정으로 번역한다.
• x=y 형식의 모든 원자 공식은 Ixy로 재작성한다.

이제 다음 알고리즘을 이전 결과에 적용하십시오.

PFL에서 1차 로직까지 역번역은 Quine(1976:302-4)에서 논의된다.

수학의 표준적 토대는 자명적인 집합 이론으로, 배경 논리는 정체성을 가진 1차적 논리로 구성되며, 담론의 우주가 전적으로 집합으로 구성된다. 정해진 멤버십으로 해석되는 학위 2의 단 하나의 술어적 문자가 있다. 표준 자명 세트 이론 ZFC의 PFL 번역은 어렵지 않다. ZFC 공리는 6개 이상의 정량화된 변수를 필요로 하지 않기 때문이다.^[2]

참고 항목

• 대수 논리학

각주

참조

• Bacon, John, 1985년 " 술어-functor 논리의 완성도," Journal of Symbolic Logic 50: 903–26.
• 1959년 폴 버네이즈, 헤이팅, A, Ed, Constructivity in Mathics의 "Uber eine naturliche Erweiterung des Reliatenkalkuls". 북 홀랜드: 1–14.
• 쿤, 스티븐 T, 1983년 "Functor Logic의 Axiomization of Predicate Functor Logic," 노틀담 저널 오브 포멀 로직 24: 233–41.
• 1976년 Willard Quine, Wayard Logic and Functicate Functors의 "Ways of Pradiscus and Other Essays"는 확대 편집되었다. 하버드 유니브 프레스: 283–307.
• 윌러드 킨, 1982년 논리학의 방법들, 4번째 에드. 하버드 유니브 45장.
• 소머스, 1982년 프레드 자연언어의 논리. 옥스퍼드 유니브 누르다
• 알프레드 타르스키와 기반트, 1987년 스티븐 변수 없는 집합론의 공식화. AMS.
• 장 반 헤이제노르트, 1967년 Frege에서 Gödel: 수학논리에 대한 출처 책. 하버드 유니브 누르다

외부 링크

• 마츠 달뢰프(Uppsala University, 언어학부)의 술어-functor 논리(원클릭 다운로드, PS 파일)