Formal Two-Party Debates

A Semantic Game (SG) is a two-party debate of the truth of a particular interpreted logic sentence, or claim for short. The debate is structured as a two-person game with two distinguished participants, the verifier and the falsifier. The party taking the position that the underlying claim is true (respectively false) becomes the verifier (respectively falsifier). The rules of the game are derived from the syntax of the underlying sentence such that the game gives a meaning to the underlying claim in the sense that if there is a winning strategy for the verifier (respectively falsifier) then the underlying claim is true (respectively false).

Semantic games are best explained through an analogy to formal debates between a proponent and opponent. A decision has to be made about a claim. A debate has the purpose of testing whether the claim is indeed true. We have two debate participants whom we ask the question: is a given claim true?

Let's assume one participant says yes and the other says no. We choose the participant who said "yes" as proponent and the participant who said "no" as opponent. They engage in the debate following a defined protocol. If the proponent (opponent) loses she has made a mistake and the opponent (proponent) participant wins a point.

Let's assume both participants make the same choice, e.g., they both say "yes". Then we choose a participant to be proponent and we force another participant to be the opponent, taking on the role of devil's advocate. If the opponent wins, the proponent must have made a mistake and the opponent wins a point. If the proponent wins, we cannot blame the opponent because she was forced.

Here is the correspondence to semantic games:

Debate				Semantic Game

proposition 			claim
proponent			verifier
opponent			falsifier
winning strategy for proponent	winning strategy for verifier
dialog				dialog, game
mistake				mistake, contradiction
debating rules			semantic game rules
debate depends on proposition   game depends on claim

Script for Debates

A debate between Alice and Bob works as follows in the context of a claim family H(c:C) = parameterized predicate logic claim. We consider a specific instance H(c0).

First Alice and Bob analyze the claim and they come up with a defense strategy for the side they take. The defense strategy might be vague and might not work. The result of the analysis is a truth value: true means verifier, false means falsifier.

aA = analyse(Alice,H(c0))
aB = analyse(Bob,H(c0))

If Alice and Bob are taking different sides, they play a regular semantic game SG(H(c0),verifier,falsifier).

if aA and !aB then r=SG(H(c0),Alice,Bob)
if !aA and aB then r=SG(H(c0),Bob,Alice)

If Alice and Bob are taking the same sides, they play a semantic game where one player is forced. The forced party is determined randomly. In SG1 the verifier is forced. In SG2 the falsifier is forced.

if !aA and !aB then r1=SG1(H(c0),Alice,Bob)
if  aA and  aB then r2=SG2(H(c0),Alice,Bob)

Being a forced player is not bad. You can never lose as the forced player and you might be able to score a point by bringing the verifier into a contradiction.

Example 1: Optimization Claim Family

The claim family: H(q) = problem p has a solution of quality q that cannot be improved. We consider the claim H(q0). Alice decides that the claim is true and she wants to be verifier. Bob decides that the claim is false and he wants to be falsifier. The defense strategy for Alice is that she thinks that she has tried all solutions to p and she did not find a better one. The refutation strategy for Bob: he already has a higher quality solution. Alice and Bob play the semantic game SG(H(q0),Alice,Bob). During the scientific discourse, Bob delivers a solution to problem p that has higher quality q0' > q0. This contradicts Alice' claim that q0 is optimum and Alice has made a mistake and loses the debate.

Example 2: Landau Notation

The claim is H()= 2*n in o(n^2) where o(g(n)) = {f(n): ForAll c>0 Exists n0>0 ForAll n>n0: 0 <=f(n) < c*g(n)}. Alice wants to be verifier and her defense strategy is that n^2 grows much faster than 2*n. Bob wants to be falsifier but his refutation strategy contains a bug.

Possible semantic games:

falsifier c=1
verifier n0=9
falsifier n=10
0 <= 2*n < c*n^2
0 <= 20 < 100: true verifier wins.

falsifier c=10^-3
verifier n0=-1+ 3*10^3
falsifier n=3*10^3
0 <= 6*10^3 < 9*10^3: true verifier wins.

Example 3: Landau Notation

Claim H() = n^0.1 in O(1000+ log(n)^3) is false. Definition: f(n) in O(g(n)) = Exists (c,n0) in (pR,pR) ForAll n > n0 in N: 0 <= f(n) <= c*g(n). Refutation strategy = Falsifier's winning strategy: polynomials grow much faster than logarithms. The verifier has a mistake in the winning strategy.

Possible semantic game: crossover = 2.08 * 10^65 for c=1, n0=1000

verifier provides c=1,n0=1000
falsifier provides large n = 2.08 * 10^66 
falsifier chooses f(n) <= c*g(n)
which is false so the falsifier wins.
Use: plot  n^0.1 and 1000+(log(n))^3 for n from 1..10^66

Example 4: Strassen claim family

Claim Strassen(c in [2,3)) = Exists M in MatrixMultiplicationAlgorithms: RunTime(M) in O(n^c). We choose c0 = 2.81: Strassen(2.81). Defense strategy: Use Strassen's algorithm from text book.

Note that there are quantifiers hidden in O(n^c)? What is the detailed protocol? Verifier provides M and c > 0 and n0 > 0. Falsifier provides input i larger than size n0. M is run on i.

How small can we make c?

Example 5: Parenthesizing a product of n objects.

Claim: There are 13 ways to parenthesize a product of 5 numbers and there are no more parenthesizations possible.

Which side do you take on this claim? What is your defense strategy?