함수 술어

형식논리와 수학의 관련 분기에서 기능적 술어 또는 함수 기호는 다른 목적어 용어를 생성하기 위해 목적어 용어에 적용될 수 있는 논리적 기호다.기능 술어는 때로 매핑이라고도 하지만, 그 용어는 수학에서 추가적인 의미를 가지고 있다.모델에서 함수 기호는 함수에 의해 모델링될 것이다.

구체적으로, 공식 언어의 기호 F는 해당 언어의 객체를 나타내는 기호 X가 주어진 경우 F(X)가 해당 언어의 객체를 나타내는 기호인 경우 기능 기호다.형식 논리학에서, 형식 T의 객체를 나타내는 기호 X가 주어진 경우 F는 도메인 타입 T와 코도메인 타입 U의 함수 기호로, F(X)는 형식 U의 객체를 나타내는 기호다. 하나 이상의 변수의 함수 기호를 유사하게 정의할 수 있으며, 0 변수의 함수 기호는 sim이다.상수 기호를 긋다

이제 [T]와 [U]로 모델링한 형식 언어의 모델과 [T]의 요소 [X]로 모델링된 T형식의 각 기호 X를 고려해 보십시오.그런 다음 F는 세트로 모델링할 수 있다.

[F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \},

단순히 도메인 [T]과 코도메인[U]이 있는 기능이다.[X] = [F(Y)]일 때마다 [F(Y)] = [X] = [Y]라는 일관된 모델의 요구사항이다.

새 기능 기호 소개

새로운 술어 기호를 도입할 수 있는 술어 논리학의 처리에서, 새로운 기능 기호를 도입할 수 있기를 원할 것이다.함수 기호 F와 G를 고려할 때, 모든 X에 대해 만족(F ∘ G)(X) = F(X)인 F와 G의 구성인 새로운 함수 기호 F ∘ G를 도입할 수 있다.물론 이 방정식의 오른쪽은 F의 도메인 유형이 G의 코도메인 유형과 일치하지 않는 한 타이프 논리에서는 이치에 맞지 않기 때문에 이것은 구성을 규정하기 위해 필요하다.

또한 특정 기능 기호를 자동으로 얻는다.유형화되지 않은 논리에는 모든 X에 대해 ID(X) = X를 만족하는 ID 술어 ID가 있다.형식 논리학에서 T형식이 주어지면 도메인 및 코드체인 T형이 있는 ID 술어 ID가_T 있으며, T형식의 모든 X에 대해 ID_T(X) = X를 만족한다.마찬가지로, T가 U의 하위 유형인 경우, 동일한 방정식을 만족하는 도메인 유형 T와 코도메인 유형 U의 포함 술어가 있다. 오래된 유형에서 새로운 유형을 구성하는 다른 방법과 관련된 추가적인 함수 기호가 있다.

또한 적절한 정리를 입증한 후에 기능 술어를 정의할 수 있다.(정리를 입증한 후 새로운 기호를 도입할 수 없는 공식적인 시스템에서 일하고 있다면, 다음 절에서와 같이 관계 기호를 사용하여 이 문제를 극복해야 할 것이다.)구체적으로 모든 X(또는 특정 유형의 모든 X)에 대해 어떤 조건 P를 만족하는 고유한 Y가 존재한다는 것을 증명할 수 있다면 함수 기호 F를 도입하여 이를 나타낼 수 있다.P 자체는 X와 Y를 모두 포함하는 관계 술어가 될 것이라는 점에 유의한다.따라서 그러한 술어 P와 정리가 있다면 다음과 같다.

T형식의 모든 X에 대해, U형, P형(X,Y)의 일부 고유 Y에 대해,

그런 다음 다음과 같은 조건을 만족하는 도메인 유형 T의 함수 기호 F와 코도메인 유형 U를 소개할 수 있다.

T형식의 모든 X에 대해, U형식의 모든 Y에 대해, Y = F(X)일 경우에만, P(X,Y)형식의 모든 Y에 대해.

기능 술어 없이 수행

술어 논리학의 많은 치료는 기능 술어를 허용하지 않고 관계 술어만을 허용한다.예를 들어, 이것은 금속 이론적 이론(Gödel의 불완전성 이론과 같은)을 증명하는 맥락에서 유용하다. 여기서 사람들은 새로운 기능적 기호(또는 그 문제에 대한 어떤 새로운 기호도)의 도입을 허용하지 않는다.그러나 기능적 기호를 전자가 발생할 수 있는 모든 곳에 관계적 기호로 대체하는 방법이 있다. 더욱이 이것은 알고리즘적이기 때문에 결과에 대부분의 금속 이론들을 적용하기에 적합하다.

구체적으로는 F가 도메인 타입 T와 코도메인 타입 U를 가지고 있는 경우, 타입(T,U)의 술어 P로 대체할 수 있다.직관적으로 P(X,Y)는 F(X) = Y를 의미한다. 그러면 F(X)가 문장에 나타날 때마다 U형의 새로운 기호 Y로 대체하고 다른 문장 P(X,Y)를 포함할 수 있다.동일한 추론을 하려면 다음과 같은 추가 제안이 필요하다.

T형식의 모든 X에 대해, U형, P형(X,Y형)의 일부 고유 Y에 대해.

(물론 이것은 앞의 절에서 새로운 함수 기호를 도입하기 전에 정리로서 증명되어야 했던 것과 같은 명제다.)

기능적 술어의 제거는 어떤 목적에도 편리하고 가능하기 때문에, 형식논리의 많은 처리는 기능적 기호만을 명시적으로 다루지 않고 오히려 관계적 기호만을 사용한다. 이것을 생각하는 또 다른 방법은 기능적 술어가 특별한 종류의 술어, 특히 그 제안을 만족시키는 술어라는 것이다.위쪽의기능 술어 F에만 적용되는 제안 스키마를 지정하려는 경우 이는 문제가 될 수 있다. 어떻게 제안 스키마가 해당 조건을 충족하는지 미리 알 수 있는가?스키마의 등가 공식화를 얻으려면 먼저 F(X) 형식의 모든 것을 새로운 변수 Y로 대체한다.그런 다음 해당 X가 도입된 직후(즉, X가 정량화된 후 또는 X가 자유로운 경우 문장의 시작 부분에서) 각 Y에 대해 보편적으로 정량화하고 P(X,Y)로 정량화를 보호한다.마지막으로, 위의 기능적 술어에 대한 고유성 조건의 중요한 결과로 전체 문장을 만든다.