Classical logic ( \(K_0\) )๏
This package formalizes [MGZ21, chapter 2.4.3 - Classical logic] .
The report content.
๐ผ๐ ๐บ๐๐๐๐ผ๐บ๐ ๐ ๐๐๐๐ผ # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฝ๐ฟ๐ผ๐ฝ๐ฒ๐ฟ๐๐ถ๐ฒ๐ ๐๐ผ๐ป๐๐ถ๐๐๐ฒ๐ป๐ฐ๐: undetermined ๐ฆ๐๐ฎ๐ฏ๐ถ๐น๐ถ๐๐ฒ๐ฑ: False ๐๐ ๐๐ฒ๐ป๐ฑ๐ฒ๐ฑ ๐๐ต๐ฒ๐ผ๐ฟ๐: ๐๐๐๐๐๐๐๐๐๐๐๐๐๐ผ ๐ ๐๐๐๐ผ (๐ฉโ) # ๐ฆ๐ถ๐บ๐ฝ๐น๐ฒ-๐ผ๐ฏ๐ท๐ฒ๐ฐ๐๐ ๐ฑ๐ฒ๐ฐ๐น๐ฎ๐ฟ๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ ๐ป๐พ ๐ ๐๐๐๐๐-๐๐๐๐๐๐ก๐ ๐๐ ๐ฐโ. # ๐ฅ๐ฒ๐น๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โยฌโ ๐ป๐พ ๐บ ๐ข๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โโนโ, โโจโ, โโงโ ๐ป๐พ ๐๐๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. # ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ๐ ๐ณ๐๐พ ๐ฟ๐๐ ๐ ๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ๐ ๐บ๐๐พ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐๐ฝ๐พ๐ ๐๐๐๐ ๐๐๐พ๐๐๐: ๐ซ๐พ๐ โ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐๐ ๐ฐโ. # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฒ๐น๐ฎ๐ฏ๐ผ๐ฟ๐ฎ๐๐ถ๐ผ๐ป ๐๐ฒ๐พ๐๐ฒ๐ป๐ฐ๐ฒ # ๐ญ: ๐๐น๐ฎ๐๐๐ถ๐ฐ๐ฎ๐น ๐น๐ผ๐ด๐ถ๐ฐ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ๐ฎ (๐ชโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโโ โยฌยฌ๐ด โ ๐ดโ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ชโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ชโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ชโ.๐โโ): (ยฌ(ยฌ(๐)) โน ๐).
The report content.
๐ผ๐ ๐บ๐๐๐๐ผ๐บ๐ ๐ ๐๐๐๐ผ # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฝ๐ฟ๐ผ๐ฝ๐ฒ๐ฟ๐๐ถ๐ฒ๐ ๐๐ผ๐ป๐๐ถ๐๐๐ฒ๐ป๐ฐ๐: undetermined ๐ฆ๐๐ฎ๐ฏ๐ถ๐น๐ถ๐๐ฒ๐ฑ: False ๐๐ ๐๐ฒ๐ป๐ฑ๐ฒ๐ฑ ๐๐ต๐ฒ๐ผ๐ฟ๐: ๐๐๐๐๐๐๐๐๐๐๐๐๐๐ผ ๐ ๐๐๐๐ผ (๐ฉโ) # ๐ฆ๐ถ๐บ๐ฝ๐น๐ฒ-๐ผ๐ฏ๐ท๐ฒ๐ฐ๐๐ ๐ฑ๐ฒ๐ฐ๐น๐ฎ๐ฟ๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ ๐ป๐พ ๐ ๐๐๐๐๐-๐๐๐๐๐๐ก๐ ๐๐ ๐ฐโ. # ๐ฅ๐ฒ๐น๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โยฌโ ๐ป๐พ ๐บ ๐ข๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โโนโ, โโจโ, โโงโ ๐ป๐พ ๐๐๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. # ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ๐ ๐ณ๐๐พ ๐ฟ๐๐ ๐ ๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ๐ ๐บ๐๐พ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐๐ฝ๐พ๐ ๐๐๐๐ ๐๐๐พ๐๐๐: ๐ซ๐พ๐ โ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐๐ ๐ฐโ. # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฒ๐น๐ฎ๐ฏ๐ผ๐ฟ๐ฎ๐๐ถ๐ผ๐ป ๐๐ฒ๐พ๐๐ฒ๐ป๐ฐ๐ฒ # ๐ญ: ๐๐น๐ฎ๐๐๐ถ๐ฐ๐ฎ๐น ๐น๐ผ๐ด๐ถ๐ฐ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ๐ฎ (๐ชโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโโ โยฌยฌ๐ด โ ๐ดโ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ชโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ชโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ชโ.๐โโ): (ยฌ(ยฌ(๐)) โน ๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โยฌยฌ๐ด โ ๐ดโ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ๐ฎ (๐ฏ๐ซโ). (ยฌ(ยฌ(๐)) โน ๐) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (ยฌ(ยฌ(๐)) โน ๐). โ
The report content.
๐ผ๐ ๐บ๐๐๐๐ผ๐บ๐ ๐ ๐๐๐๐ผ # Theory properties Consistency: undetermined Stabilized: False Extended theory: ๐๐๐๐๐๐๐๐๐๐๐๐๐๐ผ ๐ ๐๐๐๐ผ (๐ฉโ) # Simple-objects declarations Let be simple-objects in U3. # Connectives Let "not" be a unary-connective in U3. Let "==>", "or", "and" be binary-connectives in U3. # Inference rules The following inference rules are considered valid under this theory: Let "axiom-interpretation" be an inference-rule defined as "(A, P |- P)" in U3. # Theory elaboration sequence # 1: Classical logic Axiom PL12 (K0.PL1): Let axiom PL12 "!!A A" be included (postulated) in K0. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in K0. Proposition (K0.P23): (not(not(A)) ==> A).
The report content.
๐ผ๐ ๐บ๐๐๐๐ผ๐บ๐ ๐ ๐๐๐๐ผ # Theory properties Consistency: undetermined Stabilized: False Extended theory: ๐๐๐๐๐๐๐๐๐๐๐๐๐๐ผ ๐ ๐๐๐๐ผ (๐ฉโ) # Simple-objects declarations Let be simple-objects in U3. # Connectives Let "not" be a unary-connective in U3. Let "==>", "or", "and" be binary-connectives in U3. # Inference rules The following inference rules are considered valid under this theory: Let "axiom-interpretation" be an inference-rule defined as "(A, P |- P)" in U3. # Theory elaboration sequence # 1: Classical logic Axiom PL12 (K0.PL1): Let axiom PL12 "!!A A" be included (postulated) in K0. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in K0. Proposition (K0.P23): (not(not(A)) ==> A). Proof: "!!A A" is postulated by axiom PL12 (PL1). (not(not(A)) ==> A) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (not(not(A)) ==> A). QED