'''formal system''' WtEn:formal_system .... Bing:"formal system 형식체계" Ggl:"formal system 형식체계" 
CMP
[[논리,logic]]
[[산술,arithmetic]]
[[대수,algebra]]
[[대수학,algebra]]
calculus
[[수리논리,mathematical_logic]]
수학기초론 WpKo:수학기초론 WpEn:Foundations_of_mathematics

(비형식적인 것을 제외한 [[형식,form]]적인) 논리체계 (logic system ? WpEn:Logic_system Ggl:"logic system" Bing:"logic system" ) - 와 완전 동의어? chk
formal_logic ... maybe [[형식논리,formal_logic]]... 과 완전 동의어? chk

----
MKL
[[구조,structure]]
 esp abstract_structure { WpEn:Abstract_structure }
[[불완전성정리,incompleteness_theorem]]

----
Sub:
 Lambda calculus - [[람다대수,lambda_calculus]] [[Wiki:LambdaCalculus]]
  Untyped - untyped_lambda_calculus
  Typed - typed_lambda_calculus
 Predicate calculus - [[술어논리,predicate_logic]] (AKA [[일차논리,first-order_logic]])
## predicate_calculus - 이것은 '_calculus' 검색을 위해
 Propositional calculus - [[명제논리,propositional_logic]] (AKA [[영차논리,zeroth-order_logic]])
## propositional_calculus
 Sequent calculus - [[시퀀트계산,sequent_calculus]](writing)
## sequent_calculus
 Combinatory calculus - see [[WpEn:Combinatory_logic#Combinatory_calculi]]
## combinatory_calculus
  [[Wiki:CombinatoryLogic]]
  [[WpEn:SKI_combinator_calculus]]
   "that may be perceived as a reduced version of the untyped lambda calculus"
 Process calculus [[WpEn:Process_calculus]] { aka process_calculi process_algebra }
  "a diverse family of related approaches for formally modelling [[concurrent_system]]s" (wpen)
  pi-calculus π-calculus pi_calculus [[WpEn:π-calculus]] https://esolangs.org/wiki/Pi_Calculus
 Logical calculus https://encyclopediaofmath.org/wiki/Logical_calculus 
## logical_calculus
 Kappa calculus - [[WpEn:Kappa_calculus]]
  ...lambda calc.와 달리 함수는 항상 first-class_object 이고 higher-order_function 는 없다.
  ''Cite: Kappa-calculus can be regarded as "a reformulation of the first-order fragment of typed_lambda_calculus"''
## kappa_calculus
 ///TODO 일단 _calculus라는 이름 붙은거 여기 모았는데 이게 다 형식체계인지 CHK

 associative_calculus
  https://encyclopediaofmath.org/wiki/Associative_calculus
  "also called Thue systems" (via https://encyclopediaofmath.org/wiki/Calculus 마지막 문장)
  https://encyclopediaofmath.org/wiki/Thue_system
  MKLINK: [[semi-Thue_system]] { rel. [[string_rewriting_system]] { rel. [[rewrite_rule]] } }
  wt x 2023-12
  "associative calculus"
  Ggl:"associative calculus"
  rel [[결합법칙,associativity]] ... '결합성 대수'??

 group_calculus
  associative_calculus의 하나
  https://encyclopediaofmath.org/wiki/Group_calculus
  wt x 2023-12
  "group calculus"
  Ggl:"group calculus"

 Hoare_logic
  Hoare logic
  [[WtEn:Hoare_logic]]
   based on Hoare_triple { Hoare triple WtEn:Hoare_triple }
  [[WpEn:Hoare_logic]] : program의 [[correctness]]{[[WpEn:Correctness_(computer_science)]]}를 엄밀하게 [[추리,reasoning]]하는 것에 대한 [[규칙,rule]] 등으로 이루어진 [[형식체계,formal_system]] ? chk
  mklink [[precondition]] [[postcondition]] (앞 둘은 [[조건,condition]]에 작성중)
  https://everything2.com/title/Hoare+Logic
  "Hoare logic"
  Ggl:"Hoare logic"
  Up: [[logic]]

 [[effect_system]] - writing

 [[Gentzen_system]] and
 [[Gentzen_formal_system]] - writing
 https://encyclopediaofmath.org/wiki/Gentzen_formal_system
 ... Google:Gentzen+formal+system Naver:Gentzen+formal+system
 Gerhard_Gentzen

///그럼 이름으로 보아 order순으로 정렬하면
zeroth-order logic : [[명제논리,propositional_logic]]
first-order lgoic : [[술어논리,predicate_logic]]
higher order logic : 2 이상??

//''명제논리 vs 술어논리 구분 ↓. chk term usage''
명제논리를 "0차 술어논리" 라고도 부른다.
1차 이상의 [[술어논리,predicate_logic]]는 [[명제논리,propositional_logic]]의 확장이다.[* https://pub.mearie.org/%EB%AA%85%EC%A0%9C%EB%85%BC%EB%A6%AC]
----
[[연역,deduction]]

----
tmp bmks ko

형식체계의 정의:
https://chocobear.tistory.com/151?category=851370 의 Definition 1. 참조

----
같은 형식-/formal- 관련:
[[형식언어,formal_language]] : '''형식체계'''로 정의한 [[언어,language]].
[[형식문법,formal_grammar]]
[[formal_proof]] - [[증명,proof]]
....[[형식,formal]] or [[형태,form]]?
[[형식,form]]?

AKA '''logistic system''', '''axiomatic system'''

Twins:
[[WpKo:형식_체계]]
[[WpEn:Formal_system]]
[[WpEn:List_of_formal_systems]]
https://planetmath.org/formalsystem
https://www.britannica.com/topic/formal-system
https://proofwiki.org/wiki/Definition:Formal_System

https://encyclopediaofmath.org/wiki/Formal_system - ''deductive system''
 deductive_system ... 연역체계? ... [[연역,deduction]]

Up: [[논리,logic]] [[수학,math]] [[system]] ([[계,system]] or [[체계,system]] or [[시스템,system]] 중에 뭐가 best?)