Alea @alea@schelling.pt

Here is a new reasoning principle which I have not encountered before.

Majority Decision Principle:

Given propositions p₁, p₂, p₃ and q, suppose
(1) ¬pᵢ ⇒ ¬q ∨ ¬¬q, for i = 1, 2, 3
(2) pᵢ ⇒ ¬pⱼ, for i ≠ j
Then ¬q ∨ ¬¬q.

The principle is classically valid, but not intuitionistically provable. Nevertheless, it is realized by a program, here's the idea. Suppose we are given three algorithms for the same decision problem, but any one of them might be faulty—producing a wrong answer or no answer at all. Interpreting pᵢ as “the i-th algorithm is faulty,” condition (1) says that a non-faulty algorithm makes the correct decision, and condition (2) ensures that at most one algorithm is faulty. In this situation, we can make the decision by running all three algorithms in parallel and waiting for two of them to agree.

To turn this into a program, we need a model of computation that supports interleaving or parallel execution. So the validity of the principle depends on the computational model. For instance, Turing machines can realize it, since a machine can be constructed that interleaves multiple computations. It should be impossible to realize the principle in λ-calculus, although I don’t have a proof.

You might be tempted to generalize the conclusion to q ∨ ¬ q, but that won't work: if two realizers claim to have realized q, we don't know which one provided a valid realizer for q (realizing q requires evidence, but realizing ¬q does not).

There will be “k out of n” variations. Here's one, as an exercise: give a Majority Decision Principle whose conclusion is ¬q ∨ ¬r where q and r are arbitrary.