Jump to content

Formal calculation

This is a fully translated article. Click here for more information.
From DawoumWiki, the free Mathematics self-learning

수학적 논리(mathematical logic)에서 형식적 계산(formal calculation), 또는 형식적 연산(formal operation)은 시스템적이지만 엄격한 정당화가 없는 계산입니다. 여기에는 필요한 조건이 성립함을 입증하는 것 없이 일반적 치환을 사용하여 표현에서 기호를 조작하는 것이 포함됩니다. 필수적으로, 그것은 놓여있는 의미를 고려하는 것 없이 표현의 형식(form)을 포함합니다. 이 추론은 증명을 제공하는 것이 어렵거나 불필요할 때 일부 명제가 참이라는 긍정적인 증거가 되거나 새로운 (완전하게 엄격한) 정의를 만드는 영감이 될 수 있습니다.

어쨌든, 형식적이라는 용어에 대한 이러한 해석은 보편적으로 받아들여지지 않고, 일부는 그것을 정반대의 의미로 고려합니다: 형식적 수학적 논리(formal mathematical logic)에서와 같이 완전하게 엄격한 논증입니다.

Examples

형식적 계산은 한 상황에서는 잘못된 결과로 이어지지만, 또 다른 상황에서는 올바른 결과로 이어질 수 있습니다. 다음 방정식은

만약 q의 절댓값이 1보다 작으면 유지됩니다. 이 제한을 무시하고, q = 2로 대입하면 다음으로 이어집니다:

첫 번째 방정식의 증명에 q=2를 대입하면 마지막 방정식을 생성하는 공식 계산을 산출합니다. 그러나 급수가 수렴하지 않기 때문에 그것은 실수에 대해서는 틀립니다. 어쨌든, 다른 상황에서 (예를 들어, 2-진수 숫자 또는 정수 모듈로 2의 거듭제곱으로 연산), 그 급수가 수렴합니다. 형식적 계산은 마지막 방정식이 해당 문맥에서 유효해야 함을 의미합니다.

또 다른 예제는 q=–1로 대입하여 얻습니다. 결과 수열 1-1+1-1+...은 (실수와 p-진수 숫자에 대해) 발산하지만 체사로 합(Cesàro summation)과 같은 다른 합계 방법을 사용하여 값을 할당할 수 있습니다. 결과 값, 1/2은 형식적 계산에서 얻은 값과 같습니다.

Formal power series

형식적 거듭제곱 급수(Formal power series)실수 해석학(real analysis)에서 거듭제곱 급수(power series)의 형식을 차용한 개념입니다. "형식적"이라는 단어는 급수가 수렴할 필요가 없음을 나타냅니다. 수학, 특히 대수학에서, 형식적 급수는 임의의 수렴의 개념과는 독립적으로 고려되는 무한 합이고 급수에 대한 대수적 연산 (덧셈, 뺄셈, 곱셈, 나눗셈, 및 부분 합, 등)으로 조작될 수 있습니다.

형식적 거듭제곱 급수는 특별한 종류의 형식적 급수이며, 이는 다항식의 일반화로 볼 수 있으며, 여기서 항의 개수는 수렴할 필요 없이 무한대가 될 수 있습니다. 따라서, 수렴의 반지름 내에서 변수에 대한 수치적 값을 취함으로써 함수를 정의하는 거듭제곱 급수와 달리 그 급수는 더 이상 그것의 변수의 함수를 나타내지 않을 수 있고, 단지 계수의 형식적 급수일 수 있습니다. 형식적 거듭제곱에서, 변수의 거듭제곱은 의 계수가 수열에서 다섯 번째 항이 되도록 계수의 위치-보유자로만 사용됩니다. 조합론에서, 함수를 생성하는 방법은, 예를 들어 재귀가 명시적으로 해결될 수 있는지 여부에 관계없이 재귀적으로 정의된 수열에 대한 간결한 표현을 허용하는 형식적 거듭제곱 급수를 사용하여 수치적 수열과 중복집합을 나타냅니다. 더 일반적으로, 형식적 거듭제곱 급수는 변수의 임의의 유한한 (또는 셀-수-있는) 수와 임의적인 링에서 계수를 갖는 급수를 포함할 수 있습니다.

형식적 거듭제곱의 링은 대수적 기하학(algebraic geometry)교환 대수(commutative algebra)의 순수 대수적 틀에서 미적분과 유사한 방법을 지원하는 완비 지역적 링입니다. 그것들은 p의 거듭제곱의 형식적 급수로 정의될 수 있는 p-진수 정수와 유사합니다.

Symbol manipulation

다음 미분 방정식(differential equation)을 풀기 위해

이들 기호는 보통의 대수적 기호로 취급될 수 있고, 이 단계의 유효성에 관한 어떤 정당성을 제공하는 것 없이, 양쪽 변의 역수를 취합니다:

단순 역도함수(antiderivative):

이것은 형식적 계산이므로, 그것은 로 두고 또 다른 해를 구하는 것이 허용됩니다:

마지막 해는 그것들이 방정식을 푸는지 확인하기 위해 검사될 수 있습니다.

See also

References