Signature (logic)

논리(logic), 특히 수학적 논리(mathematical logic)에서, 시그니처(signature)는 형식적 언어(formal language)의 비-논리적 기호(non-logical symbols)를 나열하고 설명합니다. 보편 대수(universal algebra)에서, 시그니처는 대수적 구조(algebraic structure)를 특징짓는 연산을 나열합니다. 모델 이론(model theory)에서, 시그니처는 두 가지 목적으로 사용됩니다. 그것들은 좀 더 철학적인 논리의 취급에서 거의 명시적으로 만들어지지 않습니다.

Definition

형식적으로, (단일-정렬된) 시그니처는 4-튜플 σ = (S_func, S_rel, S_const, ar)로 정의할 수 있으며, 여기서 S_func와 S_rel은 각각 다음이라고 불리는 임의의 다른 기본 논리적 기호와 애리티(arity)라고 불리는 자연수를 모든 각 함수 또는 관계 기호에 할당하는 함수 ar: S_func $\cup$ S_rel → $\mathbb {N}$ 를 포함하지 않는 서로소 집합(sets)입니다:

함수 기호 (예제: +, ×, 0, 1),
관계 기호 or 술어 (예제: ≤, ∈),
상수 기호 (예제: 0, 1),

함수 또는 관계 기호는 그것의 애리티가 n이면 n-항(n-ary)이라고 불립니다. 일부 저자는 영-항(nullary 또는 0-ary) 함수 기호를 상수 기호로 정의하고, 그렇지 않으면 상수 기호는 별도로 정의됩니다.

함수 기호를 갖지 않는 시그니처는 관계적 시그니처(relational signature)라고 불리고, 관계 기호를 갖지 않는 시그니처는 대수적 시그니처(algebraic signature)라고 불립니다.^[1] 유한 시그니처(finite signature)는 S_func와 S_rel가 유한(finite)임을 만족하는 시그니처입니다. 보다 일반적으로, 시그니처 σ = (S_func, S_rel, S_const, ar)의 카디널리티(cardinality)는 |σ| = |S_func| + |S_rel| + |S_const|로 정의됩니다.

시그니처의 언어(language of a signature)는 논리적 시스템에서 기호와 함께 해당 시그니처에서 기호로 구축된 모든 잘 형성된 문장의 집합입니다.

Other conventions

보편 대수에서, 유형(type) 또는 닮음 유형(similarity type)이라는 단어는 종종 "시그니처"의 동의어로 사용됩니다. 모델 이론에서, 시그니처 σ는 종종 어휘(vocabulary)라고 부르거나, 비-논리적 기호(non-logical symbol)를 제공하는 (일-차) 언어 L로 식별됩니다. 어쨌든, 언어 L의 카디널리티(cardinality)는 항상 무한(infinite)입니다; 만약 σ가 유한이면, |L|은 ℵ₀일 것입니다.

공식적인 정의는 일상적인 사용에 불편하기 때문에, 특정 시그니처의 정의는 종종 다음에서 처럼 비형식적 방법에서 축약됩니다:

"아벨 그룹(abelian groups)에 대해 표준 시그니처는 σ = (+, −, 0)이며, 여기서 −는 단항 연산자입니다."

때때로 대수적 시그니처는 다음에서 처럼 단지 애리티의 목록으로 고려됩니다:

"아벨 그룹에 대해 닮음 유형은 σ = (2, 1, 0)입니다."

형식적으로, 이것은 시그니처의 함수 기호를 f₀ (이는 이항), f₁ (이는 단항), 및 f₂ (이는 영항)와 같이 어떤 것으로 정의하지만, 실제로 보통의 이름이 심지어 이 관례와 연결에서 사용됩니다.

수학적 논리(mathematical logic)에서, 매우 종종 기호는 상수 기호가 영항 함수 기호가 아닌 별도로 취급되어야 하도록 영항이 될 수 없습니다. 그것들은 애리티 함수 ar이 정의되지 않은 S_func에서 서로소인 집합 S_const를 형성합니다. 어쨌든, 이것은 문제를 복잡하게 만들 뿐이며, 특히 추가 사례가 고려되어야 하는 형식의 구조에 걸쳐 귀납법에 의한 증명에서 그러합니다. 그러한 정의 아래에서도 허용되지 않는 임의의 영항 관계 기호는 그것의 값이 모든 원소에 대해 같음을 나타내는 문장과 함께 단항 관계 기호에 의해 에뮬레이트될 수 있습니다. 이 변환은 오직 빈 구조 (종종 관례에 따라 제외됨)에 대해 실패합니다. 만약 영항 기호가 허용되면, 명제 논리(propositional logic)의 모든 각 형식은 일차 논리(first-order logic)의 형식이기도 합니다.

무한 시그니처의 예제는 무한 스칼라 필드 F에 걸쳐 벡터 공간(vector space)에 대한 표현과 방정식을 형식화하기 위해 S_func = {+} ∪ {f_a: a ∈ F} 및 S_rel = {=}를 사용하며, 여기서 각 f_a는 a에 의한 스칼라 곱셈의 단항 연산을 나타냅니다. 이런 식으로, 시그니처와 논리는 단일 정렬로 유지될 수 있으며, 벡터가 유일한 정렬입니다.^[2]

Use of signatures in logic and algebra

일-차 논리(first-order logic)의 문맥에서, 시그니처에서 기호는 역시 비-논리적 기호(non-logical symbols)로 알려져 있는데, 왜냐하면 논리적 기호와 함께 그것들은 두 가지 형식적 언어: 시그니처에 걸쳐 항(terms)의 집합과 시그니처에 걸쳐 (잘-형성된) 형식(formulas)의 집합이 귀납적으로 정의되는 놓여있는 알파벳을 형성하기 때문입니다.

구조(structure)에서, 해석(interpretation)은 함수와 관계 기호를 그것들의 이름을 정당화하는 수학적 대상에 묶습니다: 도메인 A를 갖는 구조 A에서 n-항 함수 기호 f의 해석은 함수 f^A: Aⁿ → A이고, n-항 관계 기호의 해석은 관계 R^A ⊆ Aⁿ입니다. 여기서 Aⁿ = A × A × ... × A는 도메인 A와 자체의 n-겹 데카르트 곱(cartesian product)을 나타내고, 따라서 f는 사실 n-항 함수이고, R은 n-항 관계입니다.

Many-sorted signatures

많은-정렬된 논리에 대해 그리고 많은-정렬된 구조에 대해, 시그니처는 정렬에 대한 정보를 인코딩해야 합니다. 이를 수행하는 가장 간단한 방법은 일반화된 애리티의 역할을 하는 기호 유형(symbol types)을 통한 것입니다.^[3]

Symbol types

S를 기호 × 또는 →를 포함하지 않는 (정렬의) 집합으로 놓습니다.

S에 걸쳐 기호 유형은 알파벳 $S\cup \{\times ,\to \}$ 에 걸쳐 특정 단어입니다: 관계형 기호 유형 s₁ × ... × s_n, 및 함수형 기호 유형 s₁ × ... × s_n → s′, 음의 정수 n과 s₁, s₂, ..., s_n에 대해, s′ ∈ S. (n = 0에 대해, 표현 n = 0은 빈 단어를 나타냅니다.)

Signature

(많은-정렬된) 시그니처는 다음으로 구성하는 세-쌍 (S, P, type)입니다:

정렬의 집합 S,
기호의 집합 P, 그리고
P에서 모든 각 기호에 S에 걸쳐 기호 유형과 결합하는 맵 유형.

Notes

^ Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (September 2007). "Fast nGram-Based String Search Over Data Encoded Using Algebraic Signatures" (PDF). 33rd International Conference on Very Large Data Bases (VLDB). Retrieved 27 February 2019.
^ George Grätzer (1967). "IV. Universal Algebra". In James C. Abbot (ed.). Trends in Lattice Theory. Princeton/NJ: Van Nostrand. pp. 173–210. Here: p.173.
^ Many-Sorted Logic, the first chapter in Lecture notes on Decision Procedures, written by Calogero G. Zarba.

References

Burris, Stanley N.; Sankappanavar, H.P. (1981). A Course in Universal Algebra. Springer. ISBN 3-540-90578-2. Free online edition.
Hodges, Wilfrid (1997). A Shorter Model Theory. Cambridge University Press. ISBN 0-521-58713-1.

External links

Stanford Encyclopedia of Philosophy: "Model theory"—by Wilfred Hodges.
PlanetMath: Entry "Signature" describes the concept for the case when no sorts are introduced.
Baillie, Jean, "An Introduction to the Algebraic Specification of Abstract Data Types."

[FastN-Gram-BasedStringSearch-1] Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (September 2007). "Fast nGram-Based String Search Over Data Encoded Using Algebraic Signatures" (PDF). 33rd International Conference on Very Large Data Bases (VLDB). Retrieved 27 February 2019.

[2] George Grätzer (1967). "IV. Universal Algebra". In James C. Abbot (ed.). Trends in Lattice Theory. Princeton/NJ: Van Nostrand. pp. 173–210. Here: p.173.

[3] Many-Sorted Logic, the first chapter in Lecture notes on Decision Procedures, written by Calogero G. Zarba.

[1]

[2]

[3]