접지식

Ground expression

수학 논리학에서 형식 시스템의 기본 용어는 변수를 포함하지 않는 용어다.마찬가지로, 접지 공식은 변수를 포함하지 않는 공식이다.

아이덴티티가 있는 1차 논리에서는 문장 Q(a) ( P(b)는 지상식이며, a와 b는 상수 기호로 되어 있다.그라운드 표현은 그라운드 용어 또는 그라운드 공식은 지상식이다.

예

숫자 0에 대한 상수 기호 0, 후속 함수에 대한 단항 함수 기호 s 및 추가에 대한 이진 함수 기호 +를 포함하는 서명 위에 다음 식을 첫 번째 순서로 고려하십시오.

  • s(0), s(0), s(0), ...는 접지 용어,
  • 0 + 1, 0 + 1 + 1, ...은 접지 용어,
  • x + s(1) 및 s(x)는 항이지만 접지 항은 아니다.
  • s(0) = 1 및 0 + 0은 접지 공식이며,

형식 정의

다음은 1차 언어에 대한 공식적인 정의다.C 상수 기호 집합, V (개별) 변수 집합, F 기능 연산자 집합, 그리고 P가 술어 기호 집합과 함께 1차 언어를 제공하도록 한다.

지상 용어

그라운드 항은 변수가 없는 항이다.그것들은 논리적 재귀(공식-재귀)에 의해 정의될 수 있다.

  1. C의 원소는 접지 용어다.
  2. f ∈ F가 n-ary 함수 기호이고 α1, α2, ..., α가n 접지 용어라면 f(α1, α2, ..., αn)는 접지 용어다.
  3. 모든 기본 용어는 위의 두 규칙을 유한하게 적용하여 부여할 수 있다(다른 기본 용어는 없으며, 특히 술어는 기본 용어가 될 수 없다).

대략적으로 말하면, 허브랜드 우주는 모든 지상 용어들의 집합이다.

접지 원자

지상 술어, 지상 원자 또는 지상 문자란 모두 원자 공식이며, 그 논쟁 용어는 모두 지상 용어다.

p ∈ P가 n-ary 술어 기호이고 α1, α2, ..., α가n 접지 용어라면 p(α1, α2, ..., αn)는 접지 술어 또는 접지 원자다.

대략적으로 말하면, 헤르브랜드 기지는 모든 지상 원자의 집합인 반면, 헤르브랜드 해석은 기지 내 각 지상 원자에 진실 값을 할당한다.

접지식

접지식 또는 접지절은 변수가 없는 공식이다.

자유 변수가 있는 공식은 다음과 같이 구문적 재귀로 정의할 수 있다.

  1. 비접지 원자의 자유 변수는 모두 그 안에서 발생하는 변수들이다.
  2. ¬p의 자유변수는 p의 자유변수와 같다.p∨q, p∧q, p→q의 자유 변수는 p의 자유 변수 또는 q의 자유 변수들이다.
  3. ∀x p와 ∃x p의 자유 변수는 x를 제외한 p의 자유 변수다.

참조

  • Dalal, M. (2000), "Logic-based computer programming paradigms", in Rosen, K.H.; Michaels, J.G. (eds.), Handbook of discrete and combinatorial mathematics, p. 68
  • Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
  • 1차 논리:구문 및 의미론