tag

#classical-logic

2 pages tagged

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.13 Classical vs Constructive Logic

Lean is constructive by default. This affects which proofs are available and what information a proof must contain. Classical reasoning can be enabled explicitly when needed. Problem You want to understand why some statements are easy to prove in mathematics but require additional assumptions in Lean, and how to control that boundary. Constructive Logic In constructive logic, a proof must provide explicit evidence. To prove ∃ x, P x ,...

Maths › 00. General Mathematics ›

01.5 Constructive vs Classical Viewpoints

1.5 Constructive vs Classical Viewpoints Mathematics has more than one standard way to interpret proof. The two most important viewpoints are classical and constructive mathematics. Classical mathematics accepts the usual laws of logic, including the law of excluded middle: P or not P For any proposition P , classical logic says that either P is true or P is false. This principle allows indirect proofs. To prove that an object...