First, the basic logical notions such as the definition of formulas are formalized. Then the natural deduction system plus the axiom scheme of The Law of the Excluded Middle but only for atomic formulas (ALEM) is defined and a single theorem shows that permuting, condensing or eliminating repetitions in a context does not affect the derivable formulas in that context. Following that, using induction on the complexity of formulas we derive the general law of the excluded middle and conclude: IPC + ALEM = CPC.
-
Notifications
You must be signed in to change notification settings - Fork 0
PsychoLogician/IPC_plus_ALEM_is_CPC
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Formalized: Intuitionistic Propositional Calculus (IPC) plus Atomic Law of the Excluded Middle (ALEM) is Classical Propositional Calculus (CPC)
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published