Debates and Proofs: Course Goals
We claim that winning debates is
easier than providing formal proofs.
One form of doing a debate for a claim c would be:
The verifier and the falsifier provide a proof in a formal system,
and a proof checker decides who has won the debate.
Only a few people can do formal proofs and most proofs are
informal and beyond the limits of a proof checker.
That is why we use debates based on semantic games.
They are much more lightweight than proofs and their
constructive nature has several benefits.
Structural Argument
We build our argument that debates are simpler than
proofs on the rules for semantic games.
In the following table, v stands for verifier and f for falsifier.
A is a structure defined by sets, functions and relations.
ForAll
The verifier must have a reason (but not necessarily a proof)
why no refutation is possible by falsifier.
If the verifier wins, the debate does not give a reason why.
Example: ForAll n in Nat: B(n)=C(n). The verifier of this claim
must have strong arguments why the equality holds. Ideally,
the verifier should be able to derive C(n) from B(n).
This example illustrates Karl Popper's views on Conjectures and Refutations: http://plato.stanford.edu/entries/popper/.
Exists
The verifier needs an algorithm to defend the claim but does not necessarily
need a proof why the algorithm is correct.
If the falsifier wins, the debate does not give a reason why.
And
The verifier must have a reason (but not necessarily a proof) why both subexpressions
are true, i.e., why no refutation is possible by falsifier.
Or
The verifier needs an algorithm to decide which subexpression can be defended
but not necessarily a proof why the algorithm is correct.
Special Case: Debate Results in Proof
If the claim only involves the universal quantifier ForAll and
the Boolean connective "and", and the falsifier wins,
the debate results in a proof that the claim is false.
If the claim only involves the existential quantifier Exists and
the Boolean connective "or", and the verifier wins,
the debate results in a proof that the claim is true.
In the above two cases one side takes all
actions during the debate.
What We Want to Achieve
Course Goal 1: Given a claim related to algorithms,
you correctly choose the right side (verifier or falsifier)
and you successfully defend the chosen side against another participant.
In other words, you don't let yourself be pushed into a contradiction.
Course Goal 2: For simple claims related
to algorithms you can give an informal proof why they are true or false.
Opportunity to Improve
The debater taking the correct decision (verifier or falsifier)
will always have a chance of improving its strategy when it loses, while the debater
taking the incorrect decision will not always have that chance. Therefore, assuming that the two parties are keen on winning, then, eventually, after playing several SGs and improving their strategies between SGs, the debater taking the correct decision will discover
the winning strategy and will always win.
Formal Debates

Study Groups

Domain Discourse Predicates