extern crate pocket_prover;
use pocket_prover::*;
fn main() {
println!("REMEMBER TO TEST ASSUMPTIONS BY CHECKING ALL PROVABLE STATEMENTS");
println!("");
println!("This example shows why you should become an logical assumptionist.");
println!("An logical assumptionist only accepts a proof in general as argument when");
println!("every provable statement from the assumptions are acceptable,");
println!("not just a reasonable sounding argument.");
println!("");
println!("If you want to troll someone that are not logical assumptionists,");
println!("show them this:");
println!("");
println!("(God_exists -> good) ∧ (good ¬= evil) ∧ evil");
println!("--------------------------------------------");
println!("¬God_exists");
println!("Result {}", prove!(&mut |
god,
good,
evil
| {
imply(
and!(
imply(god, good),
not(eq(good, evil)),
evil
),
not(god)
)
}));
println!("");
println!("The problem with the assumptions above is that you can also prove");
println!("there is no good.");
println!("(God_exists -> good) ∧ (good ¬= evil) ∧ evil");
println!("--------------------------------------------");
println!("¬good");
println!("Result {}", prove!(&mut |
god,
good,
evil
| {
imply(
and!(
imply(god, good),
not(eq(good, evil)),
evil
),
not(good)
)
}));
println!("");
println!("Regardless of whether you believe a god exists or not,");
println!("it is hard to believe that no good exists.");
println!("Therefore, there must be something wrong with assumptions.");
println!("");
println!("The problem is actually that `(¬∃ P) = (∀ ¬P)` instead of a simple inverse.");
println!("An updated proof clears up the ambiguity:");
println!("");
println!("(God_exists -> all_good) ∧ (all_good ¬= evil_exists) ∧ evil_exists");
println!("= ¬God_exists ∧ ¬all_good ∧ evil_exists");
println!("Result {}", prove!(&mut |
god,
good,
evil
| {
eq(
and!(
imply(god, good),
not(eq(good, evil)),
evil
),
and!(not(god), not(good), evil)
)
}));
println!("");
println!("Now you have some assumptions that can be discussed.");
println!("");
println!("One more thing about logical assumptionists:");
println!("There is no problem accepting this proof regardless of religious beliefs,");
println!("because assumptions are clearly defined and have no obvious wrong conclusions.");
println!("The point with the proof is not to show that you are correct,");
println!("but what follows from the assumptions and then improve them!");
}