REVISED: Monday, October 28, 2024
1. INTRODUCTION
A Direct Proof is a mathematical method that uses known facts to show the truth or falsehood of a statement. It's a sequence of statements that use definitions, theorems, and logic to prove a conclusion.
If P then Q or P implies Q is a Direct Proof. For our Direct Proof, we assume P is True and accomplish the proof by using P to prove Q is True.
An expression of the form P => Q (if P, then Q; Q if P) is called the implication of P and Q. P is the antecedent of the implication and Q the consequent.
If we want to implement implication in Haskell, we can do so in terms of if, then, not, and || or.
The Boolean otherwise is defined as the value True.
The only time an implication is False is when the antecedent P is True and the consequent Q is False.
2. DEFINITIONS (DEF)
DEF 1
An integer 'n' is even if and only if there exists an integer 'k' such that n = 2k
DEF 2
An integer 'n' is odd if and only if there exists an integer 'k' such that n = 2k+ 1
DEF 3
Two integers 'a' and 'b' are consecutive if and only if b = a + 1
3. PROOF 1
Theorem: The sum of any two consecutive integers is odd.
Assume 'a' and 'b' are consecutive integers.
b = a + 1 -- def 3
If 'a' and 'b' are consecutive integers, then by Definition 3, 'b' must be one more than 'a'.
(a + b) = a + (a + 1) -- def 3
(a + b) = 2a + 1 -- def 2
Since 2a is an even integer (by Definition 1), and adding 1 to an even integer always results in an odd integer (by Definition 2), (a + b) is odd.
Q.E.D. “Which was to be demonstrated".
Signifies the end of a proof.
A
□ tombstone symbol is also often used to signify the end of a proof.
4. PROOF 2
While Haskell can be used to represent and reason about mathematical proofs, it's not a direct tool for automating the process of constructing complex proofs. However, we can leverage its type system and functional paradigm to encode simple proofs and reason about them.
A Simple Proof in Haskell: The Sum of Two Even Numbers
Let's consider a simple proof: "The sum of two even numbers is even." We can represent this in Haskell using types and functions:
Theorem: The sum of two even numbers is even.
Haskell
-- Define an even number as a number divisible by 2
data Even = Even Int
-- Define a function to add two even numbers
addEven :: Even -> Even -> Even
addEven (Even x) (Even y) = Even (x + y)
Breakdown:
Data Type Even:
This data type represents an even number. It takes an integer and wraps it in the Even constructor.
Function addEven:
This function takes two Even values and returns an Even value.
It extracts the underlying integers, adds them, and constructs a new Even value.
How Does This Represent a Proof?
Type Safety: The type system ensures that the addEven function can only be applied to two Even values. This guarantees that the input numbers are indeed even.
Functional Purity: Haskell's functional nature ensures that the addEven function always produces the same output for the same input. This eliminates side effects and makes reasoning about the function's behavior straightforward.
Limitations and Advanced Techniques:
While this simple example demonstrates the potential of Haskell for representing and reasoning about mathematical proofs, it's important to note its limitations:
Complex Proofs: For more complex proofs involving multiple steps, quantifiers, and logical connectives, Haskell's type system alone may not be sufficient.
Proof Automation: While Haskell can help formalize and reason about proofs, it doesn't automate the discovery of proofs. Human ingenuity is still required to devise proof strategies.
Advanced Techniques:
Dependent Types: Dependent types allow types to depend on values, enabling more expressive and precise type systems. This can be used to encode more complex mathematical properties.
Proof Assistants: Tools like Agda and Coq are built on top of dependent type theories and provide formal proof systems for verifying mathematical theorems.
5. CONCLUSION
While Haskell is a powerful tool for representing and reasoning about mathematical concepts,
it's not a substitute for human mathematical reasoning. However, it can be used to formalize and verify proofs, especially in conjunction with advanced techniques like dependent types and proof assistants.
The goal of a proof is not only to arrive at the correct conclusion but also to present a clear and convincing argument. You want to make your proofs rigorous and easy to understand.
6. REFERENCES
Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.
Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.
Goerzen, J. & O'Sullivan, B. & Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.
Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.
Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.
Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.
