Intuitionistic logic ( \(J_0\) )๏
This package formalizes [MGZ21, chapter 2.4.2 - Intuitionistic 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 U2. # Connectives Let "not" be a unary-connective in U2. Let "==>", "and", "or" be binary-connectives in U2. # 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 U2. # Theory elaboration sequence # 1: Intuitionistic logic Axiom PL11 (J0.PL1): Let axiom PL11 "!A (A B)" be included (postulated) in J0. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in J0. Proposition (J0.P22): (not(A) ==> (A ==> B)).
The report content.
๐๐๐๐๐๐๐๐๐๐๐๐๐๐ผ ๐ ๐๐๐๐ผ # Theory properties Consistency: undetermined Stabilized: False Extended theory: ๐๐๐๐๐๐บ๐ ๐ ๐๐๐๐ผ (๐ฌโ) # Simple-objects declarations Let be simple-objects in U2. # Connectives Let "not" be a unary-connective in U2. Let "==>", "and", "or" be binary-connectives in U2. # 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 U2. # Theory elaboration sequence # 1: Intuitionistic logic Axiom PL11 (J0.PL1): Let axiom PL11 "!A (A B)" be included (postulated) in J0. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in J0. Proposition (J0.P22): (not(A) ==> (A ==> B)). Proof: "!A (A B)" is postulated by axiom PL11 (PL1). (not(A) ==> (A ==> B)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (not(A) ==> (A ==> B)). QED