Wikipedia for Formal Science

What we are after is a Wikipedia for Formal Science or formally-specified computations where the participants claim interpreted predicate logic sentences (without free variables, a.k.a. claims) used to specify computations as well as theorems that hold in a formal science.

Semantic Games

Users can contribute by participating in semantic games for claims where they take sides and exchange objects ( examples and counterexamples). This way, without proofs, they can objectively defend their own contributions and dispute the contributions of others.

Semantic games provide an objective approach to evaluate users and make it fun for users to contribute to Formal Science and Computations.

Using Hintikka's words: "Semantic games are outdoor games. They are played among the objects of the language one speaks, and they consist largely of the choices the two players between different objects" (page 38 of "The Principles of Mathematics Revisited").


One interpreted predicate logic formula (with free variables) defines a lab (laboratory, corresponding to a Wikipedia for Computations page) consisting of a claim family and several scholars contributing to the lab. We use lab relations (such as lab reductions) to solve computational problems using modularity.


We can crowdsource any formally specified component of our system to improve the system through crowdsourcing (crowdsourcing a crowdsourcing platform).

Ahmed's Thesis Proposal describing the details.

Claim Family Examples for the Formal Science Wikipedia


SaddlePoint(c) = ForAll x in [0,1] Exists y in [0,1]: x*y+(1-x)*(1-y*y)>= c.

This claim family SaddlePoint(c) consists of infinitely many claims.


Somewhere near c=0.618 is a tipping point. SaddlePoint(0.618) has been consistently defended by avatar GoodYear. SaddlePointLab1(0.619) has been consistently refuted by avatar Henry.

Highest Safe Rung

See HSRqk(q in Nat, k in Nat where k<=q)= // note the order: q comes first, k is constrained by q. Exists n in Nat where n <= 2^q: (HSR(n,k,q) and (ForAll n' > n, n' in Nat: !HSR(n',k,q)).

HSR(n,k,q) there is an experimental plan for a ladder with n rungs, k jars and a maximum of q questions to determine the highest safe rung. (That means the depth of the experimental plan, represented as a tree, is q.)

HSRnk(n,k)= Exists q in Nat < n: (HSR(n,k,q) and (ForAll q' < q, q' in Nat: !HSR(n,k,q'))

SCG Tournament Design

Design tournaments that find the good semantic game players quickly.


LocalGlobalSat(2,c) : The fraction c of the clauses that can be satisfied in any 2-satisfiable CNF formula.

Reduces to SaddlePoint.


PartialSat(R,c(R)), R is a set of relations: The fraction c of clauses can be satisfied in any boolean CSP formula whose clauses have constraints taken from R?


minVertexBasis(G) : Given a graph G, is there a minimum vertex basis size for G?


AlgorithmWorstCase(A,n): is there a worst case running time for A on inputs of size n?