이걸 아주 아주 잘 발전시킬거임, 깃헙 커밋으로 ㄱㄱ
거의 됬네 기분좋다.
∀x (각각 유일)∃!n(x) s.t. n = ObjectID(x) ∈ Scala
| AlkalicVectorSpace = Scalaᵗ [t := | Scala | ] |
| AlkalicMetrixSpace = AlkalicVectorSpaceᵗ [t := | Scala | ] |
| Alkalraum은 여기서, Scala가 객체의 집합으로 확장되어서, | Scala | = κ가 된다. |
Alkalic Algbra서 AlkalicVectorSpace나 oidfield = Σᵢ ObjectID eᵢ에 대해, 입력받는 Tensor입력으로 람다, 대수함수, Alkalic Algbra서 다가함수를 포함한 함수 구현.
폐지되었기 때문에
람다를 아예 삭제해서, 람다가 아닌 걍 연산 과정인 Subrootine으로 바꿨다.
Alkalic Algbra서 AlkalicVectorSpace나 oidfield = Σᵢ ObjectID eᵢ에 대해, 입력받는 Tensor입력으로 대수함수, Alkalic Algbra서 다가함수를 포함한 함수 구현.
하는 체계로 바뀜.
연산 괴정이다.
모든 미지수는 이 람다 체계에서 함수 내부변항으로 고정되어서, 두 함수의 합성에서 초기화되어 창출되거나, 아니면 인자로 된다. 따라서, 어떤 수학 이론은 인자를 가지며, 모델이나 진리값배정은 그 값을 넣는다. (어떻게든 대입됨)
변항은 이론에 인자로 설명 가능
⊢ KönigsbergAxiom(x, y, Φ) := (x = y → (Φ ↔ (Φ [x := y])))
이때 [x := y]는 단순히 의미론적 대입 연산자.
⊢ VectorAxiom : “모든 벡터 공간은 기저를 가진다”
다음 글을 읽어 보라.
먼저 중위표기결합자 * 에 대해, 다음과 같은 표기법을 도입한다, (*x)(y) ≡ y * x
f(x) ≡ (∈x)라고 공역이 치역으로 정의된 f와 g(x) ≡ (=x)라고 공역이 치역으로 정의된 g를 정의하겠다, 이떄, f와 g의 전사함수임이 당연하며, `≡`는 구문론적 등호다, 참고로 정의역은 집합임으로, 해당 집합이 존재해야 들어갈 수 있다, 또한 f와 g는 표기법이기 때문에, 실제 대수적 객체가 아니며, x ∈ f⁻¹(Φ)가 Φ(x)임은 당연하다, 참고로 공역을 치역으로 정의했다는 뜻은, 저 표기법이 표기하는 수학적 객체의 집합은 저 표기법이 표기하는 수학적 객체의 집합이지, 표기법에서 따로 정의하지 않기에, 최소한의 응용이 아닌 공역이 치역이 되지 않는 큰 응용을 하는것을 형식 언어 형식 문법 수준에서 금지한다고 하는것이다. (당연하다고 말한 내용들은 정의가 아니다, 태클을 걸수 있다.), 마지막으로 h̅는 h의 진리값배정이다. 진리값배정을 뜻하는 표기법이다.
외연 공리(Axiom of Extensionality)와 같은뜻인 명제를 보자, `(∀A∀B)(((x∈A) = (x∈B)) → (A = B))` ≡ `(∀A∀B)((f(A) = f(B)) → (A = B))`이기에, 외연공리는 f가 (전)단사함수임과 동치로, 외연 공리에 따라, 외연공리꼴의 다른 표현인 `f가 (전)단사함수이다`는건 외연 공리가 참일떄 참이다.
외연 공리가 의미하는 바는, 외연 공리가 만족되는 조건은, f가 일대일대응으로 동작하도록 정의된것과 같다,
따라서, 지금부터 f는 외연공리를 만족하는 f인 F로 재정의된다, F⁻¹도 외연 공리를 만족하는 f⁻¹과 같음이, f에 대한 F의 정의상 당연하다
짝 공리(Axiom of Pairing)와 같은뜻인 명제를 보자, ∃{A, B} = ∃{x | (x=A)∨(x=B)}인데 (x=A)∨(x=B) ≡ g(A)(x)∨g(B)(x) = (g(A)∨g(B))(x)로, ∃{A, B} = ∃{x | (x=A)∨(x=B)} = ∃{x | (g(A)∨g(B))(x)}이고, ∃{A, B} f({A, B})(x) = f({x | (g(A)∨g(B))(x)})(x) = (g(A)∨g(B))(x)으로, ∃{A, B} f({A, B}) = g(A)∨g(B)이기에, {A, B} = f⁻¹(g(A)∨g(B))에서, ∃f⁻¹(g(A)∨g(B))가 짝 공리와 동치로, 짝 공리에 따라, 짝 공리의 다른 표현 `∃f⁻¹(g(A)∨g(B))`은 짝 보장될때, 항진이다.
합집합 공리(Axiom of Union)와 같은뜻인 명제를 보자, ∃{x | (x∈A)∨(x∈B)} ≡ ∃{x | f(A)(x)∨f(B)(x)} = ∃{x | (f(A)∨f(B))(x)}에서, ∃{x | (x∈A)∨(x∈B)} f({x | (x∈A)∨(x∈B)})(x) = f({x | (f(A)∨f(B))(x)}) = (f(A)∨f(B))(x)이므로, ∃{x | (x∈A)∨(x∈B)} f({x | (x∈A)∨(x∈B)}) = (f(A)∨f(B))서, ∃f⁻¹(f(A)∨f(B))임이 합집합 공리와 같은 뜻이고, 합집합 공리에 따라, 합집합 공리의 다른 표현 `∃f⁻¹(f(A)∨f(B))`은 합집합 공리가 보장될때, 항진이다.
이때, 합집합 공리과 짝 공리가 다 참이라는 "합집합 공리와 짝 공리가 보장됨 공리"라는 공리를 세우겠다, 이 공리는 합집합 공리는 합집합 공리의 논리식 표현 p와 짝 공리의 논리식 표현 q에 대해 p와 q가 항진이라는 뜻으로 정의된다. 합집합 공리와 짝 공리가 보장됨 공리와 같은 명제를 보자, "합집합 공리와 짝 공리가 보장됨 공리" = "`∃f⁻¹(g(A)∨g(B))`와, `∃f⁻¹(f(A)∨f(B))`임이 보장됨 공리" = "`∃f⁻¹(g(A)∨g(B)), ∃f⁻¹(f(A)∨f(B))`"으로, , 이는, h̅ = (f, g) ⊨ (∃f⁻¹(h(A)∧h(B)))과 같으므로, 우리가 가정한 "합집합 공리와 짝 공리가 보장됨 공리"에 대해 "합집합 공리와 짝 공리가 보장됨 공리"에 따라, "합집합 공리와 짝 공리가 보장됨 공리"의 다른 표현인 `h̅ = (f, g) ⊨ (∃f⁻¹(h(A)∨h(B)))`는 "합집합 공리와 짝 공리가 보장됨 공리"가 참일때 참이다.
멱집합 공리(Axiom of Power Set)는 멱집합의 존재성을 보장한다.
사실 이는 f가 아닌 F에서도 동일하기에, "합집합 공리와 짝 공리가 보장됨 공리"는 외연공리가 성립하는 F에 대해서 다룰수 있다면, "`h̅ = (F, g) ⊨ (∃F⁻¹(h(A)∨h(B)))`"이다.
치환 공리꼴(Axiom Schema of Replacement)의 다른 표현을 보자, 치환 공리꼴이란 무엇일까? 한마디로 치환 공리꼴은 함수 h에 대해, {h(x) | x ∈ A}의 존재성은 A가 존재해야 보장돼야한다는것이다. 한마디로, ∃A ⇒ ∃{h(x) | x ∈ A}이다. 이때, f({h(x) | x ∈ A})(x) = (∃v ∈ A)((h(v) =)(x)) = ((∃v ∈ A)(h(v) =))(x) 이므로, {h(x) | x ∈ A} = f⁻¹(((∃v ∈ A)(h(v) =)))에서, ∃A ⇒ ∃f⁻¹(((∃v ∈ A)(h(v) =)))임이 치환 공리꼴과 동치이다, 따라서, 치환 공리꼴에 따라 치환 공리꼴의 다른 표현 `∃A ⇒ ∃f⁻¹(((∃v ∈ A)(h(v) =)))`은 치환 공리꼴이 보장될때 항진이다.
치환 공리꼴도 f가 아닌 F에서도 동일하기에, 외연공리가 성립하는 F에 대해서 다룰수 있다면 "∃A ⇒ ∃F⁻¹(((∃v ∈ A)(h(v) =)))"이다.
분류 공리꼴(Axiom Schema of Separation/Specification)은 성질 Φ를 만족하는 부분집합이 존재한다는거다, 성질 Φ를 만족하는 부분집합이 존재한다는뜻은 ∀S ∃{x |(Φ(x)) ∧ (x∈S)}이며, ∀S ∃{x |(Φ(x)) ∧ (x∈S)} ≡ ∀S ∃{x |(Φ(x)) ∧ f(S)(x)}이고, ∀S ∃{x |(Φ(x)) ∧ f(S)(x)}라는건 ∀S ∃f(P) = Φ∧f(S)임과 동치이기에, 분류공리꼴에 따라 분류공리꼴의 다른 표현 `f(P) = Φ∧f(S)`은 분류 공리꼴이 보장될때 항진이다, 이후에 분류 공리꼴을 이용하여 집합론에 대해 논하겠다.
ZF안에 ZF를 만든다고 가정하면, 범주론적으로(함자에 대한 서술로) 접근할때, "∃A ⇒ ∃F⁻¹(((∃v ∈ A)(h(v) =)))"안에서 "h̅ = (f, g) ⊨ (∃f⁻¹(h(A)∨h(B)))", "∃A ⇒ ∃F⁻¹(((∃v ∈ A)(h(v) =)))"가 성립한다, 그러나 이것은 ZF내의 ZF에서만 성립한다. `"메타언어가 서술하는 "내부언어에 관한" 구문"`꼴이기 때문이다.
따라서,
ℙ1 : "∃A ⇒ ∃F⁻¹(((∃v ∈ A)(h(v) =)))"
ℙ2 : "h̅ = (f, g) ⊨ (∃f⁻¹(h(A)∨h(B)))"
를 따로 정의하겠다.
공집합 공리(Axiom of Empty Set)와 같은뜻인 명제를 보자, `(∃S ∀x)(￢(x∈S))` ≡ `(∃S ∀x)(￢f(S)(x))` 이고 `(∃S ∀x)(￢f(S)(x))`와 같은뜻인 명제 `(∃S ∀x)(f(S)(x) = F)`는 `x⊥y = x⊥ = ⊥y = ⊥ = F`인 `⊥`정의에따라서, `(∃S)(f(S) = ⊥)`임과 동치이다, 즉, `∃f⁻¹(⊥)`은 공집합공리와 동치이기에, 공집합 공리에 따라, 공집합 공리의 다른 표현 `∃f⁻¹(⊥)`은 공집합 공리가 보장될때, 항진이다.
무한 공리 (Axiom of Infinity)는 자연수 집합의 존재성을 보장하는 공리이다. "모든 자연수 x에 대해, (∃ℕ)(f(ℕ)(x))"는 무한공리와 같다,
정칙 공리 (Axiom of Regularity / Foundation)는 랭크 함수 Rank의 존재성을 보장한다.
이때, 무한 유향 비순환 가중 그래프 preZFSetThoeremModel에 대한 중복도 W를 정의하고, W(x, y) := int(x ∈ y)로 정의하면, (또한, 동시에, 멱집합의 존재도 보장하여 구성하면,)
멤버십 관계 ∈는 분류 공리꼴을 이용하여, 다음과 같이 재정의된다 ((x ∈ y) s.t. (x ∈ y) when (h(x) = Φ(x))) := F(y)(x) s.t. (∀P ∈ 2ᴬ)(F(P) = h(P)∧F(A)) (단. F는 가능한 한 전단사인 표기법이며, 현제의 정의에서 (∃h(P), F(A) ⇒ ∃(x ∈ y)라고 치역이 정의된다)
이는 분류 공리꼴을 만족시키는 정의이다.
preZFSetThoeremModel들 중에서, ℙ1, ℙ2를 만족시키는 preZFSetThoeremModel를 ZFSetThoeremModel라 할수 있는데, 이들 중 공집합과 자연수를 이론 내부에서 논하는 집합으로 가지는 ZFSetThoeremModel는 메타 언어로 동작할 수 있고, ℙ1를 만족시키는 preZFSetThoeremModel들 중에서 공집합과 자연수를 가지는 preZFSetThoeremModel는 ZFSetThoeremModel와 위계 이외엔 동등하다.
더 나아가서, 상수로써 자연수와 공집합을 가지고, 멱집합 연산과 ℙ1, ℙ2를 구성하는 연산이 정의되는 튜링 언어를 이용하는 형식문법 G 문법의 형식언어 L의 모델은 preZFSetThoeremModel이다. 따라서 FOL에서 HOL로 확장가능한 대수공리계에서 모델론과 구문론과 집합론과 논리까지 싹다 서술 가능하다면, preZFSetThoeremModel도 서술 가능하므로, 그런 대수공리계는 ZF와 동등하다. (이러한 모델의 존재성이 참이 된다는 전제하에)
저러한 대수 공리계는 존재한다, 예컨데 alkalic이 그렇다.
Königsberg Axiom은 alkalic을 구성하여, 저 조건을 만족한다. 따라서 ZF공리계와 Königsberg Axiom체제 (25.07.16 커밋 이전)는 ZFC랑 그 능력이 동등하다. (상호 서술)
VectorAxiom은 AC와 동치이다, 따라서 Königsberg Axiom + VectorAxiom은 ZFC와 동등하다. (상호 서술)
이때 다음 공리를 도입하자, 아래 공리계는 Alkalic-LinearAlgebra의 ZFC로 구성되었다 ⊢ InaccessibleCardinalExistanceAxiom : ∃κ cf(κ) = κ ∧ κ > ℵ₀ ∀λ<κ, 2^λ < κ [cf(x) := least δ ∈ Ord s.t. ∃f : δ → x, (∀i < δ)(f(i) < x) ∧ (∀α < x)(∃i < δ)(α < f(i))]
이때 κ가 Alkalraum의 구성에 쓰인다.
Alkalraum은 κ로 그 크기가 확장된 Alkalic-LinearAlgebra의 객체를 Scala에 포함하는 Hilbertraum같은 (((Scala^κ)^κ)^….)^κ식으로 구성된 κ Rank Covector공간이며, 복소수나 분발복소수/이원수나 2ⁿ원수 등의 행렬표현에서 그 원래 집합의 원소 역할을 하는 객체로의 대응된것 등이 있을수 있는 실수 및 함수 및 객체들로 된 선형대수 텐서공간인데, κ크기를 보장하기에, Grothendieck 우주가 존재하는 ZFC를 표현할수 있어, 여기서 SetTheorem은 자동으로 Grothendieck 우주가 존재하는 ZFC로, 범주론이 서술된다.
이전에 나온 CSFBAlgebra에서 모델론이 안먹히나 했는데 먹힘, 그래서 아이 새로 CSFBAlgebra를 정리(바꿈), 그게 Alkalic.
M = (ℕ, 0 = ∅, s(x) = x ∪ {x}) 대신
수열의 곱을 다가함수로 써서,
M = Π<ℕ, [0 := ∅], [s := λx. x ∪ {x}]>
같은 서수의 정의가 가능하다는 점에서,
이제 Structure와 변수 대입까지 함수 안에서 됬음.
이제 구조체도 non-structial 논리적 귀결에서 씀으로 쓸수있음
에초에 CSFBAlgebra를 대체할 목적으로 만든거니
나머지는 이하 생략.
KönigsbergAxiom 에 따라서,
규칙
using x = y → (Φ ↔ (Φ [x := y])))원리 :
x = y → (Φ ↔ (Φ [x := y])))서x = y가 결론 (5번 라인)과 같음을 보임□.1. using x = y → (Φ ↔ (Φ [x := y]))) □.2. x = y □.3. Φ □.4. Φ [x := y] □.5. Φ ↔ (Φ [x := y])
모든 추론은 규칙 using x = y → (Φ ↔ (Φ [x := y])))에서 시작되며, 규칙 using x = y → (Φ ↔ (Φ [x := y])))는 기본적으로 modus ponens 추론 규칙을 따르기에 타당 (valid)하다. (심지어 Königsberg Axiom이 항진인데, Königsberg Axiom을 제외하고는 대수 연산밖에 활용하지 않기에, alkalic은 건전하다)
(전건부정의 오류 하나 있어서 삭제함)
내부적으로 결론(5번 라인)이 참일때만 계속 동작함, 또한 결론은 리스트에 쌓이면서, 마지막 줄인 Theorem에 도달할때까지 Lemma가 리스트업되서, 문장이 참인지는 Lemma로 보임.
규칙 :
Starting Listup Hyperthesis미리 Hyperthesis나열을 시작함
규칙 :
Quit Listup Hyperthesis더이상 Hyperthesis를 받지 아니함
규칙 :
Starting Another Subproof새 스택프레임을 만들어, 새로운 부분증명을 시작함
규칙 :
Quit Another Subproof부분증명을 끝내, Lemma List에 추가하고, 스택프레임을 pop함
규칙 :
APAristotel-y(nonHyperVersion 형식증명 only)HAPA Theorem이라는 외부정리를 이용하여서, y = x이고 y = z이면 x = z임을 보임
규칙 :
APAristotel-z(nonHyperVersion 형식증명 only) HAPA Theorem이라는 외부정리를 이용하여서, x = z이고 y = z이면 y = x임을 보임
Alkalic-Proofmood nonHyperVersion 형식증명의 근거.
동시에 유일한 Alkalic-Proofmood HyperVersion에서의 형식증명
y = x, y = z가 가설일때,
규칙 using x = y → (Φ ↔ (Φ [x := y])))를 통하여, y = z ↔ x = z를 보인다, 즉,
문법상, y = z → (y = z ↔ (y = z [y := x])) = y = z ↔ (y = z ↔ x = z)이므로,
y = z ↔ (y = z ↔ x = z)를 표현하기 위한 잉여적인 체계다.
(그치만 이전에 있었던 전건부정 오류때문에 또 고쳐야함 ㅠㅠ)
증명에 앞부분에 붙여야 할 한정사가 추가되었다, 부분증명을 만들어서 중첩 가능하기에, 각 기능을 동시에 붙일수 없다.
∴ Φₜ, Φₜ₊₁, ..., Φₖ ⊨ Φₖ₊₁ (강함), ∴ Φₖ ⊨ Φₖ₊₁ (약함), ∴ Mod(Φ) = ℕ (일반적인 수학적 귀납법) 으로 기제한다.∴ ⊥ ∴ ⊭ ¬
Φ ∴ Φ를 놓는다. (¬Φ는 결론을 뜻한다.)또한 검증 프로그램 정지를 피하기 위해,
�를 삽입한다, 이 부분•전체 증명은 가설(Hyperthesis)로 취급된다.마지막으로, 다항식의 계산을 원활하게 하기 위해,
Polynomial Simplify라는 부분증명 폼을 넣고 다음을 인수분해하거나, P(x) = 0꼴을 풀면 (후자는 미리 using P(x) = 0 Algorithm이라고 명시) 오류 없이 증명을 받아들여준다.
A. LinearSimplify명령을 통해, LinearSimplify Theorem에 근거하여, 미지수가 여러개인 일차식을 정리한다
B. Substracting [y := xⁿ]명령을 통해, xⁿ을 y로 치환한 문장 Φ에 대해, Substracting Variable필드에 넣은 참인 문장 y = xⁿ에 따라서, Φ [y := xⁿ]가 나올때까지, 미리 일차식마냥 치환한 상태로 작업하게 해준다. (치환 변수 필드 논법; Substracting Variable Field Proofs)
C. Solution (a, b, c, d, e)명령을 통해, 2차 ~ 4차식을 인수분해(근의공식) / 전개(비에트의 정리)한다.
D. TschirnhausTheoremSubsituate (n, a, b, x)명령을 통해, [x := t + b/na]를 적용한다, 마찬가지로 증명의 원활함을 위해 Substracting명령에 근거한다 (사실 그럴 필요도 없이 구문론적으로 연산자를 정의해도 되는 간단한 문장([x := t + b/na])이지만)
E. 부분증명 문법에서 synthetic division 한정사로, 조립제법 이용 (생략표기가, 매거적 귀납에서 고정된 열의 다수의 행에대해 쓰이므로, 여기서는 쓸때, 행을 다항식으로, 계산 과정순이 열로 되므로, 돌려봐야하는 단점이 있다.)
F. Alright synthetic division한정사로, 일반적인 조립제법을 쓰고, 전처리 단계에서 synthetic division로 컴파일
G. 분배법칙을 위해서, distribute[ 대상 ] 안에 전부 넣어가지고, 이 증명 시스템용으로 있는 분배법칙의 일반화 정리에 따라, 분배함
H. AlgebraicFormula : 미리 증명한 곱셈공식을 이용해서, 계산되었음을 명시한다.
I. Gaussian Eimination or ERO & Subsituate : 가우스 소거 혹은 가감/대입
J. System of Quadratic Equations by Quadratic Form : 이차형식으로 연립이차방 풀이
K. System of Quadratic Equations by Cubic Form : 삼차형식으로 연립삼차방 풀이
L. Règle de Cramer : 크래머의 공식으로 풀이
M. Extraneous Root is (□) : 무연근 명시
N. PolynomialFractionize : 다항함수 분수화
O. SolvePolynomialFraction : 해당값 풀이
P. Fractions Solution is (□) : 해 명시
□. 라인이 부분증명이라면, □.line.식으로 라인을 표기한다.
그리도, 라인과 라인 사이에 오직 whitespace및 -,–,—만 있을경우 해당 라인을 가독성 용도로 보고 주석처리한다.
또한, line표기에 앞선 점찍은 부분 앞에서 |부분이 문자열의 특정 열마다 이어지고, 끝나는 말단이 앞서 설명한 -꼴의 주석에 연결되어있다면, 해당 부분도 따로 오류처리하지 않는다.
그외에는, 열 구분자이기에 주석으로 보지 않는다
마지막으로, [NOTE : ]형식을 주석으로 본다.
마크다운 문서 내부에 위치했다면, HAlkalic-Proofmood(Hyper Version), Alkalic-Proofmood(일반 버전), PowerAP(Power Up버전)으로 코드 이름인 부분만 읽는다. 또한, 마크다운 부분에 부분증명 코드부분은, 부분증명으로 렌더링한다.
마지막으로 그렇게 html화되어 정리된 렌더링 뷰는, LaTeX 표기 기능을 추가해야만 할것이다.
(그럼에도 해당 html뷰는 아직 형식증명 검토가 안돌아갔으므로, 컴파일 상태인거지, 실행 상태가 아니다. 실행은 실행기에 돌려야, 문서 내부를 파싱해서, 부가적으로 제공된, labare•unbare 코드와 함깨 해석하여(labare•unbare는 인터프리터 언어가 아니고, 정형 대이터 겸 사용자 편의 대이터 겸 Low Level 컴파일 언어다.), 검토된다; 이제보니 실행기보다는, 형식증명 검토기라는 명칭이 더 적합하다, 프로그래밍 언어는 하나도 실행하지 않고, 추론규칙을 재대로 활용했는지만 검사하여 검토작업(오류나 로그나 상태 표시)만 하기 때문이다.)
논리적으로 다룬다 전재할때, 대수식은 논리적으로 그 뜻이 해석 • 계산된다.의 발췌그렇지 아니하면, 논리적 해석 흐름에서 논리기호가 도출될수가 없다.
식의 계산은 그 값의 배정인 (x̄, f(x̄))와 같이 이루어지는데, 이 방식을 거부하는것은, 논리를 쓰지 않겠다는 말과 같다. (장자 왈 갓나서 죽은 아기보다 오래 산 사람은 없으니 팽조(760살이 넘게 살았다는 전설 상의 신선)도 일찍 요절한 사람)
먼저, 다음을 보이겠다
함자
f :≜ (-F)를 정의해서, 여기에 대해,
x = y 이면이 f(x) = f(y)
이말은, 진리값 T, F를 다루는 식에서, F = 0으로 가정하고 푸는거나, F ≠ 0이 아닐때 푸는거나, 전부 x = y인 등식을 쓸때 f(x) = f(y)가 F와 무관히 동등함이 당연함으로, F = 0인 경우로 잠정적으로 취급하겠음
Step.1. 방정식을 만족하는 집합으로써의 모델집합이 해집합임을 보이자
먼저, 다음과 같은 다항식 함수 P를 정의하자.
P :≜ λA. λx. Πᵢ x - Aᵢ
그리고 다음과 같은 방정식화 논리함수 Φ를 정의하자.
Φ :≜ λf. (f(x) = 0)
그리고 마지막으로, 다항 방정식 ㅍ을 정의하겠다.
ㅍ :≜ φ • P
그러면,
Mod(ㅍ(A)) = {x | x ⊨ (Πᵢ x - Aᵢ = 0)} = {x̄ | Πᵢ x̄ - Aᵢ = 0} = {Aᵢ | ∀i}
임이 당연하다.
Step.2. 논리적 귀결관계의 도출
다항방정식 ㅍ(A), ㅍ(B)에 대해,
| {Aᵢ | ∀i} ⊆ {Bᵢ | ∀i} |
| P(A) | P(B) |
으로,
다항식 f, g에 대해 다항방정식 Φ(f) ⊨ Φ(g)
이면이
f g
¬x = T - x로 해석됨을 보이자. (경고 : 형식증명 아님)
A. proof of x ≠ T ⊢ T ± x ≠ (1 ± 1)T
x ≠ T (비 귀류법식 전제 문장)T ± x ≠ T ± T (이항 by 함자 (T ±))T ± x ≠ T ± T = (1 ± 1)T (1번의 연장선에서 계산)T ± x ≠ (1 ± 1)T (2번에서 식 요약) ⋯ ■B. proof of ⊭ (1 + 1)T = 0 ∨ (1 + 1)T = T
⊭ (1 + 1)T = 0와 part B bt ⊭ (1 + 1)T = T로 나눠서 생각하자.
1.A. (1 + 1)T = 0 (귀류법식 전재 문장)
2.A. (1 + 1)T = 2T = 0 (1.A.번의 연장선에서 계산)
3.A. T = 0 ⊨ 2.A. ⊨ (1 + 1)T = 0 (연역)
4.A. ⊭ T = 0 ⊨ 2.A. ⊨ (1 + 1)T = 0 (연역)
5.A. ⊭ (1 + 1)T = 0 (연역) ⋯ ⊥
6.A. ∴ ⊭ (1 + 1)T = 0 (연역) ⋯ ■
1.B. (1 + 1)T = T (귀류법식 전재 문장)
2.B. (1 + 1)T = 2T = T (1.B.번의 연장선에서 계산)
3.B. T = 0 ⊨ 2.A. ⊨ (1 + 1)T = T (연역)
4.B. ⊭ T = 0 ⊨ 2.A. ⊨ (1 + 1)T = T (연역)
5.B. ⊭ (1 + 1)T = T (연역) ⋯ ⊥
6.B. ∴ ⊭ (1 + 1)T = T (연역) ⋯ ■C.1. A, B ⊨ (x ≠ T ⊢ T - x ≠ (1 - 1)T) (A, B번에서 귀결) C.2. A, B ⊨ (x ≠ T ⊢ T - x ≠ (1 - 1)T = 0T = 0) (C.1.번의 연장선에서 계산) C.3. A, B ⊨ (x ≠ T ⊢ T - x ≠ 0) (C.2.번에서 식 요약) C.4. A, B ⊨ (T - x = 0 ⊨ x = T ⊨ x) (C.3.번에서 연역추론 : 대우) 《주의 : “x = T”의 의미를 “진리값 x가 참”관점으로 해석함.》 C.5. A, B ⊨ (T - x = 0 ⊨ x) (C.4.번에서 식 요약) 《주의 : 근거인 C.4.에서 “x = T”의 의미를 “진리값 x가 참”관점으로 해석함.》 C.6. C.5.번 내용 ⊢ ¬x = T - x (최종결론)《주의 : “x = T”의 의미를 “진리값 x가 참”관점으로 해석함.》 Q.E.D.
x ∧ y는 xy로 해석됨을 보이자. T에대한 방정식 (T - x)(T - y) = 0의 해는 x = T ∨ y = T이다. 따라서, x = T ∨ y = T ⊨ T - (T - x)(T - y) = T고, x ∨ y = T - (T - x)(T - y)로 해석된다.
이때 De Morgan’s Law, ¬(¬x ∨ ¬y) = x ∧ y서
T - T + (T - T + x)(T - T + y) = xy이다. ⋯ Done.
방정식 P(x) = 0이 불능이란것은
∄P(x) = 0란 뜻이며
∀P(x) ≠ 0이란 뜻이고 ⋯ ①
방정식 P(x) = 0가 불능이 아니라면
∃P(x) = 0이다. ⋯ ②
방정식 P(x) = 0이 부정이란것은,
부정방정식이므로,
∀P(x) = 0이다. ⋯ ③
①에서, 불능형 방정식 P(x) = 0에 대해,
P(x) ≠ 0은 부정형이고, ⋯ ④
부정형 방정식 P(x) = 0에 대해,
P(x) ≠ 0은 불능형이다 ⋯ ⑤
그렇다면 ③에 따라 다음을 정의하자,
Φ :≜ λf. (∃f(x) = 0)`P :≜ λf. (∃f(x) ≠ 0)
그러면 다음을 알수 있다.
④에 따라, Φ(f)가 거짓 이면이 P(f)는 부정형 ⑤에 따라, Φ(f)가 부정형 이면이 P(f)는 거짓
Φ(f)가 참 이면이, f(x) = 0를 만족시키는 x존재 P(f)가 참 이면이, f(x) = 0을 불만족시키는 x존재
부정형 방정식을 만들고 싶다? 하면
¬Φ(f) = P(f), Φ(x) = ¬P(f)에서,
불능형 방정식 Φ(f)에 대해 부정하거나, 불능형 방정식 P(f)에 대해 부정하면된다.
술어 P에 대해 Mod(P) = ∅ 이면이 ∄P(x) 이면이 ⊭ P 이면이 Mod(¬P) = U 이면이 ∀¬P(x) 이면이 ⊨ ¬P
따라서, 방정식은 기본적으로 특칭 술어로써, 사용할수 있음