Minimal logic ( \(M_0\) )๏
This package formalizes [MGZ21, chapter 2.4.1 - Minimal logic] .
The report content.
๐๐๐๐๐๐บ๐ ๐ ๐๐๐๐ผ # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฝ๐ฟ๐ผ๐ฝ๐ฒ๐ฟ๐๐ถ๐ฒ๐ ๐๐ผ๐ป๐๐ถ๐๐๐ฒ๐ป๐ฐ๐: undetermined ๐ฆ๐๐ฎ๐ฏ๐ถ๐น๐ถ๐๐ฒ๐ฑ: False ๐๐ ๐๐ฒ๐ป๐ฑ๐ฒ๐ฑ ๐๐ต๐ฒ๐ผ๐ฟ๐: N/A # ๐ฆ๐ถ๐บ๐ฝ๐น๐ฒ-๐ผ๐ฏ๐ท๐ฒ๐ฐ๐๐ ๐ฑ๐ฒ๐ฐ๐น๐ฎ๐ฟ๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ ๐ป๐พ ๐ ๐๐๐๐๐-๐๐๐๐๐๐ก๐ ๐๐ ๐ฐโ. # ๐ฅ๐ฒ๐น๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โยฌโ ๐ป๐พ ๐บ ๐ข๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โโนโ, โโจโ, โโงโ ๐ป๐พ ๐๐๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. # ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ๐ ๐ณ๐๐พ ๐ฟ๐๐ ๐ ๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ๐ ๐บ๐๐พ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐๐ฝ๐พ๐ ๐๐๐๐ ๐๐๐พ๐๐๐: ๐ซ๐พ๐ โ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐ข๐ -๐๐๐๐๐๐ โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฒ๐น๐ฎ๐ฏ๐ผ๐ฟ๐ฎ๐๐ถ๐ผ๐ป ๐๐ฒ๐พ๐๐ฒ๐ป๐ฐ๐ฒ # ๐ญ: ๐ ๐ถ๐ป๐ถ๐บ๐ฎ๐น ๐น๐ผ๐ด๐ถ๐ฐ ## ๐ญ.๐ญ: ๐๐ ๐ถ๐ผ๐บ๐ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ๐ด โ (๐ด โง ๐ด)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): (๐ โน (๐ โง ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฎ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โง ๐ต) โ (๐ต โง ๐ด)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โง ๐) โน (๐ โง ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฏ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โ ๐ต) โ [(๐ด โง ๐ถ) โ (๐ต โง ๐ถ)]โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โน ๐) โน ((๐ โง ๐) โน (๐ โง ๐))). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฐ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ[(๐ด โ ๐ต) โง (๐ต โ ๐ถ)] โ (๐ด โ ๐ถ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): (((๐ โน ๐) โง (๐ โน ๐)) โน (๐ โน ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฑ (๐ฌโ.๐ฏ๐ซโ ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ๐ต โ (๐ด โ ๐ต)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ ): (๐ โน (๐ โน ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฒ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โง (๐ด โ ๐ต)) โ ๐ตโ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โง (๐ โน ๐)) โน ๐). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ณ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ๐ด โ (๐ด โจ ๐ต)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฃ๐๐ณ (๐ฌโ.๐โ): (๐ โน (๐ โจ ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ด (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โจ ๐ต) โ (๐ต โจ ๐ด)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โจ ๐) โน (๐ โจ ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ต (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ[(๐ด โ ๐ถ) โง (๐ต โ ๐ถ)] โ [(๐ด โจ ๐ต) โ ๐ถ]โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): (((๐ โน ๐) โง (๐ โน ๐)) โน ((๐ โจ ๐) โน ๐)). ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ๐ฌ (๐ฌโ.๐ฏ๐ซโโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโโ โ[(๐ด โ ๐ต) โง (๐ด โ ยฌ๐ต)] โ ยฌ๐ดโ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โโ): (((๐ โน ๐) โง (๐ โน ยฌ(๐))) โน ยฌ(๐)). ## ๐ญ.๐ฎ: ๐๐ถ๐ฟ๐๐ ๐ฑ๐ฒ๐ฟ๐ถ๐๐ฎ๐๐ถ๐ผ๐ป ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ญ (๐ฌโ.๐โโ): (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ (๐ฌโ.๐โโ): ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)))). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐ข๐ -๐๐๐๐๐๐ ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฏ (๐ฌโ.๐โโ): (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฐ (๐ฌโ.๐โโ): ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))) โน ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฑ (๐ฌโ.๐โโ ): ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฒ (๐ฌโ.๐โโ): (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ณ (๐ฌโ.๐โโ): ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ด (๐ฌโ.๐โโ): (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ต (๐ฌโ.๐โโ): ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ญ๐ฌ (๐ฌโ.๐โโ): (((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ญ๐ญ (๐ฌโ.๐โโ): (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)).
The report content.
๐๐๐๐๐๐บ๐ ๐ ๐๐๐๐ผ # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฝ๐ฟ๐ผ๐ฝ๐ฒ๐ฟ๐๐ถ๐ฒ๐ ๐๐ผ๐ป๐๐ถ๐๐๐ฒ๐ป๐ฐ๐: undetermined ๐ฆ๐๐ฎ๐ฏ๐ถ๐น๐ถ๐๐ฒ๐ฑ: False ๐๐ ๐๐ฒ๐ป๐ฑ๐ฒ๐ฑ ๐๐ต๐ฒ๐ผ๐ฟ๐: N/A # ๐ฆ๐ถ๐บ๐ฝ๐น๐ฒ-๐ผ๐ฏ๐ท๐ฒ๐ฐ๐๐ ๐ฑ๐ฒ๐ฐ๐น๐ฎ๐ฟ๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ ๐ป๐พ ๐ ๐๐๐๐๐-๐๐๐๐๐๐ก๐ ๐๐ ๐ฐโ. # ๐ฅ๐ฒ๐น๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โยฌโ ๐ป๐พ ๐บ ๐ข๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โโนโ, โโจโ, โโงโ ๐ป๐พ ๐๐๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. # ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ๐ ๐ณ๐๐พ ๐ฟ๐๐ ๐ ๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ๐ ๐บ๐๐พ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐๐ฝ๐พ๐ ๐๐๐๐ ๐๐๐พ๐๐๐: ๐ซ๐พ๐ โ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐ข๐ -๐๐๐๐๐๐ โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฒ๐น๐ฎ๐ฏ๐ผ๐ฟ๐ฎ๐๐ถ๐ผ๐ป ๐๐ฒ๐พ๐๐ฒ๐ป๐ฐ๐ฒ # ๐ญ: ๐ ๐ถ๐ป๐ถ๐บ๐ฎ๐น ๐น๐ผ๐ด๐ถ๐ฐ ## ๐ญ.๐ญ: ๐๐ ๐ถ๐ผ๐บ๐ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ๐ด โ (๐ด โง ๐ด)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): (๐ โน (๐ โง ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐ด โ (๐ด โง ๐ด)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ (๐ฏ๐ซโ). (๐ โน (๐ โง ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (๐ โน (๐ โง ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฎ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โง ๐ต) โ (๐ต โง ๐ด)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โง ๐) โน (๐ โง ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ(๐ด โง ๐ต) โ (๐ต โง ๐ด)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฎ (๐ฏ๐ซโ). ((๐ โง ๐) โน (๐ โง ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ โง ๐) โน (๐ โง ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฏ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โ ๐ต) โ [(๐ด โง ๐ถ) โ (๐ต โง ๐ถ)]โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โน ๐) โน ((๐ โง ๐) โน (๐ โง ๐))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ(๐ด โ ๐ต) โ [(๐ด โง ๐ถ) โ (๐ต โง ๐ถ)]โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฏ (๐ฏ๐ซโ). ((๐ โน ๐) โน ((๐ โง ๐) โน (๐ โง ๐))) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ โน ๐) โน ((๐ โง ๐) โน (๐ โง ๐))). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฐ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ[(๐ด โ ๐ต) โง (๐ต โ ๐ถ)] โ (๐ด โ ๐ถ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): (((๐ โน ๐) โง (๐ โน ๐)) โน (๐ โน ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ[(๐ด โ ๐ต) โง (๐ต โ ๐ถ)] โ (๐ด โ ๐ถ)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฐ (๐ฏ๐ซโ). (((๐ โน ๐) โง (๐ โน ๐)) โน (๐ โน ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ โน ๐) โง (๐ โน ๐)) โน (๐ โน ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฑ (๐ฌโ.๐ฏ๐ซโ ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ๐ต โ (๐ด โ ๐ต)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ ): (๐ โน (๐ โน ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐ต โ (๐ด โ ๐ต)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฑ (๐ฏ๐ซโ ). (๐ โน (๐ โน ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (๐ โน (๐ โน ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฒ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โง (๐ด โ ๐ต)) โ ๐ตโ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โง (๐ โน ๐)) โน ๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ(๐ด โง (๐ด โ ๐ต)) โ ๐ตโ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ฒ (๐ฏ๐ซโ). ((๐ โง (๐ โน ๐)) โน ๐) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ โง (๐ โน ๐)) โน ๐). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ณ (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ๐ด โ (๐ด โจ ๐ต)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฃ๐๐ณ (๐ฌโ.๐โ): (๐ โน (๐ โจ ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐ด โ (๐ด โจ ๐ต)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ณ (๐ฏ๐ซโ). (๐ โน (๐ โจ ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (๐ โน (๐ โจ ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ด (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ(๐ด โจ ๐ต) โ (๐ต โจ ๐ด)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): ((๐ โจ ๐) โน (๐ โจ ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ(๐ด โจ ๐ต) โ (๐ต โจ ๐ด)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ด (๐ฏ๐ซโ). ((๐ โจ ๐) โน (๐ โจ ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ โจ ๐) โน (๐ โจ ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ต (๐ฌโ.๐ฏ๐ซโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโ โ[(๐ด โ ๐ถ) โง (๐ต โ ๐ถ)] โ [(๐ด โจ ๐ต) โ ๐ถ]โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โ): (((๐ โน ๐) โง (๐ โน ๐)) โน ((๐ โจ ๐) โน ๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ[(๐ด โ ๐ถ) โง (๐ต โ ๐ถ)] โ [(๐ด โจ ๐ต) โ ๐ถ]โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ต (๐ฏ๐ซโ). (((๐ โน ๐) โง (๐ โน ๐)) โน ((๐ โจ ๐) โน ๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ โน ๐) โง (๐ โน ๐)) โน ((๐ โจ ๐) โน ๐)). โ ๐๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ๐ฌ (๐ฌโ.๐ฏ๐ซโโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐ฏ๐ซโโ โ[(๐ด โ ๐ต) โง (๐ด โ ยฌ๐ต)] โ ยฌ๐ดโ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฌโ.๐โโ): (((๐ โน ๐) โง (๐ โน ยฌ(๐))) โน ยฌ(๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ[(๐ด โ ๐ต) โง (๐ด โ ยฌ๐ต)] โ ยฌ๐ดโ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฃ๐๐ญ๐ฌ (๐ฏ๐ซโโ). (((๐ โน ๐) โง (๐ โน ยฌ(๐))) โน ยฌ(๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ โน ๐) โง (๐ โน ยฌ(๐))) โน ยฌ(๐)). โ ## ๐ญ.๐ฎ: ๐๐ถ๐ฟ๐๐ ๐ฑ๐ฒ๐ฟ๐ถ๐๐ฎ๐๐ถ๐ผ๐ป ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ญ (๐ฌโ.๐โโ): (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (๐ โน (๐ โจ ๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฃ๐๐ณ (๐โ). ๐ซ๐พ๐ ๐ = ๐ฉโ, ๐ = ๐ฉโ. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ (๐ฌโ.๐โโ): ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (๐ โน (๐ โน ๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ ). ๐ซ๐พ๐ ๐ = (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)), ๐ = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)))). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐ข๐ -๐๐๐๐๐๐ ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฌโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฏ (๐ฌโ.๐โโ): (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฎ (๐โโ).(๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ญ (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฐ (๐ฌโ.๐โโ): ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))) โน ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐ โน ๐) โน ((๐ โง ๐) โน (๐ โง ๐))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐ = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)), ๐ = (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)), ๐ = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))) โน ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฑ (๐ฌโ.๐โโ ): ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))) โน ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฐ (๐โโ).(((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฏ (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฒ (๐ฌโ.๐โโ): (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (๐ โน (๐ โง ๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐ = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ณ (๐ฌโ.๐โโ): ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐ โจ ๐) โน (๐ โจ ๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐ = ๐ฉโ, ๐ = ๐ฉโ. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ด (๐ฌโ.๐โโ): (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โน (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฒ (๐โโ).((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ณ (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ต (๐ฌโ.๐โโ): ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฑ (๐โโ ).(((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ด (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ญ๐ฌ (๐ฌโ.๐โโ): (((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((๐ โน ๐) โง (๐ โน ๐)) โน (๐ โน ๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐ = ๐ฉโ, ๐ = (๐ฉโ โจ ๐ฉโ), ๐ = (๐ฉโ โจ ๐ฉโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ญ๐ญ (๐ฌโ.๐โโ): (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) โน (๐ฉโ โน (๐ฉโ โจ ๐ฉโ))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ญ๐ฌ (๐โโ).((๐ฉโ โน (๐ฉโ โจ ๐ฉโ)) โง ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ))) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ต (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)). โ
The report content.
๐๐๐๐๐๐บ๐ ๐ ๐๐๐๐ผ # Theory properties Consistency: undetermined Stabilized: False Extended theory: N/A # Simple-objects declarations Let be simple-objects in U1. # Connectives Let "not" be a unary-connective in U1. Let "==>", "or", "and" be binary-connectives in U1. # 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 U1. Let "modus-ponens" be an inference-rule defined as "((P3 ==> Q2), P3 |- Q2)" in U1. Let "variable-substitution" be an inference-rule defined as "(P1, O1 |- Q1)" in U1. # Theory elaboration sequence # 1: Minimal logic ## 1.1: Axioms Axiom PL1 (M0.PL1): Let axiom PL1 "A (A A)" be included (postulated) in M0. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in M0. Proposition (M0.P1): (A ==> (A and A)). Axiom PL2 (M0.PL2): Let axiom PL2 "(A B) (B A)" be included (postulated) in M0. Proposition (M0.P2): ((A and B) ==> (B and A)). Axiom PL3 (M0.PL3): Let axiom PL3 "(A B) [(A C) (B C)]" be included (postulated) in M0. Proposition (M0.P3): ((A ==> B) ==> ((A and C) ==> (B and C))). Axiom PL4 (M0.PL4): Let axiom PL4 "[(A B) (B C)] (A C)" be included (postulated) in M0. Proposition (M0.P4): (((A ==> B) and (B ==> C)) ==> (A ==> C)). Axiom PL5 (M0.PL5): Let axiom PL5 "B (A B)" be included (postulated) in M0. Proposition (M0.P5): (B ==> (A ==> B)). Axiom PL6 (M0.PL6): Let axiom PL6 "(A (A B)) B" be included (postulated) in M0. Proposition (M0.P6): ((A and (A ==> B)) ==> B). Axiom PL7 (M0.PL7): Let axiom PL7 "A (A B)" be included (postulated) in M0. Proposition PL7 (M0.P7): (A ==> (A or B)). Axiom PL8 (M0.PL8): Let axiom PL8 "(A B) (B A)" be included (postulated) in M0. Proposition (M0.P8): ((A or B) ==> (B or A)). Axiom PL9 (M0.PL9): Let axiom PL9 "[(A C) (B C)] [(A B) C]" be included (postulated) in M0. Proposition (M0.P9): (((A ==> C) and (B ==> C)) ==> ((A or B) ==> C)). Axiom PL10 (M0.PL10): Let axiom PL10 "[(A B) (A !B)] !A" be included (postulated) in M0. Proposition (M0.P10): (((A ==> B) and (A ==> not(B))) ==> not(A)). ## 1.2: First derivation Inference rule (variable-substitution): Let inference-rule variable-substitution defined as "(P1, O1 |- Q1)" be included and considered valid in M0. Proposition 1 (M0.P11): (p1 ==> (p1 or p2)). Proposition 2 (M0.P12): ((p1 ==> (p1 or p2)) ==> (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2)))). Inference rule (modus-ponens): Let inference-rule modus-ponens defined as "((P3 ==> Q2), P3 |- Q2)" be included and considered valid in M0. Proposition 3 (M0.P13): (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))). Proposition 4 (M0.P14): ((((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))) ==> ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))))). Proposition 5 (M0.P15): ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1)))). Proposition 6 (M0.P16): (((p1 or p2) ==> (p2 or p1)) ==> (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1)))). Proposition 7 (M0.P17): ((p1 or p2) ==> (p2 or p1)). Proposition 8 (M0.P18): (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))). Proposition 9 (M0.P19): ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))). Proposition 10 (M0.P20): (((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))) ==> (p1 ==> (p2 or p1))). Proposition 11 (M0.P21): (p1 ==> (p2 or p1)).
The report content.
๐๐๐๐๐๐บ๐ ๐ ๐๐๐๐ผ # Theory properties Consistency: undetermined Stabilized: False Extended theory: N/A # Simple-objects declarations Let be simple-objects in U1. # Connectives Let "not" be a unary-connective in U1. Let "==>", "or", "and" be binary-connectives in U1. # 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 U1. Let "modus-ponens" be an inference-rule defined as "((P3 ==> Q2), P3 |- Q2)" in U1. Let "variable-substitution" be an inference-rule defined as "(P1, O1 |- Q1)" in U1. # Theory elaboration sequence # 1: Minimal logic ## 1.1: Axioms Axiom PL1 (M0.PL1): Let axiom PL1 "A (A A)" be included (postulated) in M0. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in M0. Proposition (M0.P1): (A ==> (A and A)). Proof: "A (A A)" is postulated by axiom PL1 (PL1). (A ==> (A and A)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (A ==> (A and A)). QED Axiom PL2 (M0.PL2): Let axiom PL2 "(A B) (B A)" be included (postulated) in M0. Proposition (M0.P2): ((A and B) ==> (B and A)). Proof: "(A B) (B A)" is postulated by axiom PL2 (PL2). ((A and B) ==> (B and A)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((A and B) ==> (B and A)). QED Axiom PL3 (M0.PL3): Let axiom PL3 "(A B) [(A C) (B C)]" be included (postulated) in M0. Proposition (M0.P3): ((A ==> B) ==> ((A and C) ==> (B and C))). Proof: "(A B) [(A C) (B C)]" is postulated by axiom PL3 (PL3). ((A ==> B) ==> ((A and C) ==> (B and C))) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((A ==> B) ==> ((A and C) ==> (B and C))). QED Axiom PL4 (M0.PL4): Let axiom PL4 "[(A B) (B C)] (A C)" be included (postulated) in M0. Proposition (M0.P4): (((A ==> B) and (B ==> C)) ==> (A ==> C)). Proof: "[(A B) (B C)] (A C)" is postulated by axiom PL4 (PL4). (((A ==> B) and (B ==> C)) ==> (A ==> C)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (((A ==> B) and (B ==> C)) ==> (A ==> C)). QED Axiom PL5 (M0.PL5): Let axiom PL5 "B (A B)" be included (postulated) in M0. Proposition (M0.P5): (B ==> (A ==> B)). Proof: "B (A B)" is postulated by axiom PL5 (PL5). (B ==> (A ==> B)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (B ==> (A ==> B)). QED Axiom PL6 (M0.PL6): Let axiom PL6 "(A (A B)) B" be included (postulated) in M0. Proposition (M0.P6): ((A and (A ==> B)) ==> B). Proof: "(A (A B)) B" is postulated by axiom PL6 (PL6). ((A and (A ==> B)) ==> B) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((A and (A ==> B)) ==> B). QED Axiom PL7 (M0.PL7): Let axiom PL7 "A (A B)" be included (postulated) in M0. Proposition PL7 (M0.P7): (A ==> (A or B)). Proof: "A (A B)" is postulated by axiom PL7 (PL7). (A ==> (A or B)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (A ==> (A or B)). QED Axiom PL8 (M0.PL8): Let axiom PL8 "(A B) (B A)" be included (postulated) in M0. Proposition (M0.P8): ((A or B) ==> (B or A)). Proof: "(A B) (B A)" is postulated by axiom PL8 (PL8). ((A or B) ==> (B or A)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((A or B) ==> (B or A)). QED Axiom PL9 (M0.PL9): Let axiom PL9 "[(A C) (B C)] [(A B) C]" be included (postulated) in M0. Proposition (M0.P9): (((A ==> C) and (B ==> C)) ==> ((A or B) ==> C)). Proof: "[(A C) (B C)] [(A B) C]" is postulated by axiom PL9 (PL9). (((A ==> C) and (B ==> C)) ==> ((A or B) ==> C)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (((A ==> C) and (B ==> C)) ==> ((A or B) ==> C)). QED Axiom PL10 (M0.PL10): Let axiom PL10 "[(A B) (A !B)] !A" be included (postulated) in M0. Proposition (M0.P10): (((A ==> B) and (A ==> not(B))) ==> not(A)). Proof: "[(A B) (A !B)] !A" is postulated by axiom PL10 (PL10). (((A ==> B) and (A ==> not(B))) ==> not(A)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (((A ==> B) and (A ==> not(B))) ==> not(A)). QED ## 1.2: First derivation Inference rule (variable-substitution): Let inference-rule variable-substitution defined as "(P1, O1 |- Q1)" be included and considered valid in M0. Proposition 1 (M0.P11): (p1 ==> (p1 or p2)). Proof: (A ==> (A or B)) follows from prop. PL7 (P7). Let A = ๐ฉโ, B = ๐ฉโ. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that (p1 ==> (p1 or p2)). QED Proposition 2 (M0.P12): ((p1 ==> (p1 or p2)) ==> (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2)))). Proof: (B ==> (A ==> B)) follows from prop. (P5). Let B = (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)), A = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((p1 ==> (p1 or p2)) ==> (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2)))). QED Inference rule (modus-ponens): Let inference-rule modus-ponens defined as "((P3 ==> Q2), P3 |- Q2)" be included and considered valid in M0. Proposition 3 (M0.P13): (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))). Proof: ((p1 ==> (p1 or p2)) ==> (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2)))) follows from prop. 2 (P12).(p1 ==> (p1 or p2)) follows from prop. 1 (P11). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))). QED Proposition 4 (M0.P14): ((((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))) ==> ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))))). Proof: ((A ==> B) ==> ((A and C) ==> (B and C))) follows from prop. (P3). Let A = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)), B = (๐ฉโ โน (๐ฉโ โจ ๐ฉโ)), C = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))) ==> ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))))). QED Proposition 5 (M0.P15): ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1)))). Proof: ((((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))) ==> ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))))) follows from prop. 4 (P14).(((p1 or p2) ==> (p2 or p1)) ==> (p1 ==> (p1 or p2))) follows from prop. 3 (P13). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1)))). QED Proposition 6 (M0.P16): (((p1 or p2) ==> (p2 or p1)) ==> (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1)))). Proof: (A ==> (A and A)) follows from prop. (P1). Let A = ((๐ฉโ โจ ๐ฉโ) โน (๐ฉโ โจ ๐ฉโ)). Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that (((p1 or p2) ==> (p2 or p1)) ==> (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1)))). QED Proposition 7 (M0.P17): ((p1 or p2) ==> (p2 or p1)). Proof: ((A or B) ==> (B or A)) follows from prop. (P8). Let A = ๐ฉโ, B = ๐ฉโ. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((p1 or p2) ==> (p2 or p1)). QED Proposition 8 (M0.P18): (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))). Proof: (((p1 or p2) ==> (p2 or p1)) ==> (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1)))) follows from prop. 6 (P16).((p1 or p2) ==> (p2 or p1)) follows from prop. 7 (P17). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))). QED Proposition 9 (M0.P19): ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))). Proof: ((((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) ==> ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1)))) follows from prop. 5 (P15).(((p1 or p2) ==> (p2 or p1)) and ((p1 or p2) ==> (p2 or p1))) follows from prop. 8 (P18). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))). QED Proposition 10 (M0.P20): (((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))) ==> (p1 ==> (p2 or p1))). Proof: (((A ==> B) and (B ==> C)) ==> (A ==> C)) follows from prop. (P4). Let A = ๐ฉโ, B = (๐ฉโ โจ ๐ฉโ), C = (๐ฉโ โจ ๐ฉโ). Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that (((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))) ==> (p1 ==> (p2 or p1))). QED Proposition 11 (M0.P21): (p1 ==> (p2 or p1)). Proof: (((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))) ==> (p1 ==> (p2 or p1))) follows from prop. 10 (P20).((p1 ==> (p1 or p2)) and ((p1 or p2) ==> (p2 or p1))) follows from prop. 9 (P19). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (p1 ==> (p2 or p1)). QED