Well-formed formula

수학적 논리(mathematical logic), 명제 논리(propositional logic)와 술어 논리(predicate logic)에서, 잘-형성된 공식(well-formed formula), 약어로 WFF 또는 wff, 종종 단순히 공식(formula)은 형식적 언어(formal language)의 일부인 주어진 알파벳(alphabet)에서 기호(symbols)의 유한 수열(sequence)입니다.^[1] 형식적 언어는 언어에서 공식의 집합으로 식별될 수 있습니다.

공식은 해석을 수단으로 의미론적 뜻(meaning)을 부여할 수 있는 통사론의(syntactic) 대상입니다. 공식의 두 가지 핵심 용도는 명제 논리와 술어 논리입니다.

Introduction

공식의 핵심 용도는 명제 논리(propositional logic)와 일-차 논리(first-order logic)와 같은 술어 논리(predicate logic)에 있습니다. 그것들 문맥에서, 공식은 φ에서 한번 임의의 자유 변수(free variable)가 인스턴스화되면, "φ가 참입니까?"라고 묻는 것이 의미가 있는 기호 φ의 문자열입니다. 형식적 논리에서, 증명(proof)은 특정 속성을 갖는 공식의 수열에 의해 표현될 수 있고, 수열에서 최종 공식은 증명된 것입니다.

비록 용어 "공식"이 쓰는 표식 (예를 들어, 종이 또는 칠판의 일부)에 사용될 수 있을지라도, 기호의 수열이 표현되는 것으로 보다 정확하게 이해되며, 표식은 공식의 토큰(token) 인스턴스입니다. 따라서, 같은 공식이 한번보다 많이 쓰일 수 있고, 공식은 원칙적으로 그것이 물리적 우주 내에 전혀 쓰일 수 없을 만큼 너무 길 수 있습니다.

수식 자체는 통사론의 대상입니다. 그것들은 해석에 의해 의미가 부여됩니다. 예를 들어, 명제 공식에서, 각 명제 변수는 전체 공식이 이들 명제 사이의 관계를 표현하도록 구체적인 명제로 해석될 수 있습니다. 공식이 오로지 하나의 공식으로 여겨지기 위해, 어쨌든, 해석될 필요는 없습니다.

Propositional calculus

명제 계산법(propositional calculus)의 공식은, 역시 명제 공식(propositional formula)이라고 불리며, $(A\land (B\lor C))$ 와 같은 표현입니다.^[2] 그들의 정의는 명제 변수(propositional variable)의 집합 V의 임의적인 선택으로 시작합니다. 알파벳은 V에서 문자와 명제 연결(propositional connective)과 괄호 "(" 및 ")"의 기호로 구성되며, 그것의 모두는 V 안에 없는 것으로 가정됩니다. 공식은 이 알파벳에 걸쳐 특정 표현 (즉, 기호의 문자열 )일 것입니다.

공식은 다음과 같이 귀납적으로(inductively) 정의됩니다:

각 명제 변수는, 그 자체로, 공식입니다.
만약 φ가 공식이면, ¬φ는 공식입니다.
만약 φ 및 ψ가 공식이고, •가 임의의 이진 연결이면, (φ • ψ)는 공식입니다. 여기서 •는 보통 연산자 ∨, ∧, →, 또는 ↔일 수 있습니다 (그러나 제한되지는 않습니다).

이 정의는 역시 배커스–나우르 형식(Backus–Naur form)의 형식적 문법으로 쓰일 수 있으며, 변수의 집합이 유한하다는 조건 아래에서 제공됩니다:

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> | ¬<form> | (<form>∧<form>) | (<form>∨<form>) | (<form>→<form>) | (<form>↔<form>)

이 문법을 사용하여, 다음 기호의 수열은

(((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s))

하나의 공식인데, 왜냐하면 그것은 문법적으로 정확하기 때문입니다. 다음 기호의 수열은

((p → q)→(qq))p))

하나의 공식이 아닌데, 왜냐하면 그것은 문법에 맞지 않기 때문입니다.

복잡한 공식은, 예를 들어, 괄호의 확산으로 인해, 읽기 어려울 수 있습니다. 이 마지막 현상을 완화하기 위해, 우선-순위 규칙 (표준 수학적 연산의 순서와 유사)이 가정되어, 일부 연산자를 다른 연산자보다 더 많이 바인딩되게 만듭니다. 예를 들어, 우선-순위 (최대 바인딩에서 최소 바인딩까지) 1. ¬ 2. → 3. ∧ 4. ∨를 가정합니다. 그런-다음 다음 공식은

(((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s))

다음으로 축약될 수 있습니다:

p → q ∧ r → s ∨ ¬q ∧ ¬s

이것은, 어쨌든, 오직 공식의 서면 표현을 단순화하기 위해 사용되는 관례입니다. 만약 우선순위가, 예를 들어, 다음 순서: 1. ¬ 2. ∧ 3. ∨ 4. →에서 왼쪽-오른쪽 결합인 것으로 가정되면, 위와 같은 공식 (괄호 없음)이 다음으로 다시-쓰일 것입니다:

(p → (q ∧ r)) → (s ∨ ((¬q) ∧ (¬s)))

Predicate logic

일-차 논리(first-order logic) ${\mathcal {QS}}$ 에서 공식의 정의는 당면한 이론의 시그니처(signature)와 관련이 있습니다. 이 시그니처는 함수와 술어 기호의 애리티(arities)와 함께 당면한 이론의 상수 기호, 술어 기호, 및 함수 기호를 지정합니다.

공식의 정의는 여러 부분으로 나뉩니다. 첫째, 항(terms)의 집합이 재귀적으로 정의됩니다. 항은, 비공식적으로, 담론의 도메인(domain of discourse)의 대상을 나타내는 표현입니다.

임의의 변수는 항입니다.
시그니처에서 임의의 상수 기호는 항입니다.
형식 f(t₁,…,t_n)의 표현은, 여기서 f가 n-항 함수 기호이고, t₁,…,t_n가 항이며, 다시 하나의 항입니다.

다음 단계는 원자 공식(atomic formula)을 정의하는 것입니다.

만약 t₁와 t₂가 항이면, t₁=t₂는 원자 공식입니다.
만약 R이 n-항 술어 기호이고, t₁,…,t_n가 항이면, R(t₁,…,t_n)는 원자 공식입니다.

마지막으로, 공식의 집합은 다음이 유지됨을 만족하는 원자 공식의 집합을 포함하는 가장 작은 집합으로 정의됩니다:

$\neg \phi$ 는 $\phi$ 가 공식일 때 공식입니다.
$(\phi \land \psi )$ 와 $(\phi \lor \psi )$ 는 $\phi$ 와 $\psi$ 가 공식일 때 공식입니다;
$\exists x\,\phi$ 는 $x$ 가 변수이고 $\phi$ 가 공식일 때 공식입니다;
$\forall x\,\phi$ 는 $x$ 가 변수이고 $\phi$ 가 공식일 때 공식입니다 (대안적으로, $\forall x\,\phi$ 가 $\neg \exists x\,\neg \phi$ 에 대해 축약으로 정의될 수 있습니다).

만약 공식이 임의의 변수 $x$ 에 대해 $\exists x$ 또는 $\forall x$ 의 발생을 가지지 않으면, 그것은 한정어-자유(quantifier-free)라고 불립니다. 존재적 공식(existential formula)은 한정자-자유 공식을 따르는 존재적 정량화(existential quantification)의 수열로 시작하는 공식입니다.

Atomic and open formulas

원자 공식은 논리적 연결(logical connective)을 포함하지 않고 한정어(quantifiers)도 포함하지 않는 공식, 또는 동등하게 엄격한 부분공식을 가지지 않는 공식입니다. 원자 공식의 정확한 형식은 고려중인 형식적 시스템에 따라 다릅니다; 명제 논리(propositional logic)에 대해, 예를 들어, 원자 공식은 명제 변수(propositional variable)입니다. 술어 논리(predicate logic)에 대해, 원자는 인수와 함께 술어 기호이며, 각 인수는 항(term)입니다.

일부 용어에 따르면, 열린 공식은 한정어를 제외하고 오직 논리적 연결을 사용하여 원자 공식을 결합함으로써 형성됩니다.^[3] 이것은 닫혀있지 않은 공식과 혼동해서는 안됩니다.

Closed formulas

닫힌 공식, 역시 바닥(ground) 공식 또는 구문은 임의의 변수(variable)의 자유 발생(free occurrences)이 없는 공식입니다. 만약 A가 변수 v₁, …, v_n가 자유 발생을 가지는 일-차 언어에서 공식이면, $\forall$ v₁ ⋯ $\forall$ v_n에 선행하는 A는 A의 클로저입니다.

Properties applicable to formulas

언어 ${\mathcal {Q}}$ 에서 공식 A는 만약 그것이 ${\mathcal {Q}}$ 의 모든 각 해석(interpretation)에 대해 참이면 타당(valid)합니다.
언어 ${\mathcal {Q}}$ 에서 공식 A는 만약 그것이 ${\mathcal {Q}}$ 의 일부 해석(interpretation)에 대해 참이면 충족-가능(satisfiable)입니다.
산술(arithmetic)의 언어의 공식 A가 만약 그것이 결정-가능 집합(decidable set)을 나타내면, 즉, A의 자유 변수의 치환(substitution)이 주어지면, A의 결과 인스턴스가 입증-가능 또는 그것의 부정이 그런 것이라고 말하는 효과적인 방법(effective method)이 있으면 결정-가능입니다.

Usage of the terminology

수학 논리에 대한 이른 연구 (예를 들어, 처치(Church)^[4]에 의한 것)에서, 공식은 임의의 기호의 문자열을 참조했고 이들 문자열 중에서, 잘-형성된 공식의 (올바른) 공식의 형성화 규칙을 따르는 문자열이었습니다.

여러 저자는 단순히 공식을 말합니다.^[5]^[6]^[7]^[8] 현대적 사용 (특히 모델 검사기(model checkers), 자동화된 정리 증명기(automated theorem prover), 대화형 정리 증명기(interactive theorem provers)와 같은 수학적 소프트웨어를 갖는 컴퓨터 과학의 문맥에서)은 공식의 개념을 오직 대수적 개념에 유지하고 잘-형성성(well-formedness), 즉, 단지 표기법적 문제로서의 (연결과 한정어에 대해 이것 또는 저것 기호를 사용하여, 이것 또는 저것 괄호화 관례(parenthesizing convention)를 사용하여, 폴란드(Polish) 또는 중위(infix) 표기법을 사용하여, 등) 공식의 구체적인 문자열 표현의 문제를 남기는 경향이 있습니다.

표현 잘-형성된 공식이 여전히 사용되고 있지만,^[9]^[10]^[11] 이들 저자들은 더 이상 수학적 논리에서 공통적이지 않은 공식의 예전 의미와 모순되게 그것을 반드시^{[weasel words]} 사용하지는 않습니다.^{[citation needed]}

표현 "잘-형성된 공식" (WFF)은 역시 대중 문화에 침투했습니다. WFF는 레이먼 앨런(Layman Allen)에 의한, 그가 에일 법률 학교(Yale Law School)에 있던 동안 개발했던, 학술 게임 "WFF 'N PROOF: 현대 논리의 게임"의 이름에서 사용되는 난해한 말장난의 일부입니다 (그는 나중에 미시간 대학(University of Michigan)에서 교수였습니다).^[12] 게임 모음은 (폴란드 표기법(Polish notation)에서) 아이들에게 기호적 논리의 원리를 가르치기 위해 고안되었습니다.^[13] 그것의 이름은 The Whiffenpoof Song과 The Whiffenpoofs에서 인기를 얻은 예일 대학교(Yale University)에서 응원으로 사용되는 whiffenpoof, 비상식 단어(nonsense word)의 반향입니다.^[14]

Notes

^ Formulas are a standard topic in introductory logic, and are covered by all introductory textbooks, including Enderton (2001), Gamut (1990), and Kleene (1967)
^ First-order logic and automated theorem proving, Melvin Fitting, Springer, 1996 [1]
^ Handbook of the history of logic, (Vol 5, Logic from Russell to Church), Tarski's logic by Keith Simmons, D. Gabbay and J. Woods Eds, p568 [2].
^ Alonzo Church, [1996] (1944), Introduction to mathematical logic, page 49
^ Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea
^ Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
^ Barwise, Jon, ed. (1982), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
^ Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3
^ Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
^ R. L. Simpson (1999), Essentials of Symbolic Logic, page 12
^ Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall
^ Ehrenburg 2002
^ More technically, propositional logic using the Fitch-style calculus.
^ Allen (1965) acknowledges the pun.

References

Allen, Layman E. (1965), "Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games", Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council, Monographs of the Society for Research in Child Development, 30 (1): 29–41
Boolos, George; Burgess, John; Jeffrey, Richard (2002), Computability and Logic (4th ed.), Cambridge University Press, ISBN 978-0-521-00758-0
Ehrenberg, Rachel (Spring 2002). "He's Positively Logical". Michigan Today. University of Michigan. Archived from the original on 2009-02-08. Retrieved 2007-08-19.
Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
Gamut, L.T.F. (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic, University Of Chicago Press, ISBN 0-226-28085-3
Hodges, Wilfrid (2001), "Classical Logic I: First-Order Logic", in Goble, Lou (ed.), The Blackwell Guide to Philosophical Logic, Blackwell, ISBN 978-0-631-20692-7
Hofstadter, Douglas (1980), Gödel, Escher, Bach: An Eternal Golden Braid, Penguin Books, ISBN 978-0-14-005579-5
Kleene, Stephen Cole (2002) [1967], Mathematical logic, New York: Dover Publications, ISBN 978-0-486-42533-7, MR 1950307
Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6

External links

Well-Formed Formula for First Order Predicate Logic - includes a short Java quiz.
Well-Formed Formula at ProvenMath

[1] Formulas are a standard topic in introductory logic, and are covered by all introductory textbooks, including Enderton (2001), Gamut (1990), and Kleene (1967)

[2] First-order logic and automated theorem proving, Melvin Fitting, Springer, 1996 [1]

[3] Handbook of the history of logic, (Vol 5, Logic from Russell to Church), Tarski's logic by Keith Simmons, D. Gabbay and J. Woods Eds, p568 [2].

[4] Alonzo Church, [1996] (1944), Introduction to mathematical logic, page 49

[5] Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea

[6] Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6

[7] Barwise, Jon, ed. (1982), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1

[8] Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3

[9] Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3

[10] R. L. Simpson (1999), Essentials of Symbolic Logic, page 12

[11] Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall

[12] Ehrenburg 2002

[13] More technically, propositional logic using the Fitch-style calculus.

[14] Allen (1965) acknowledges the pun.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]