Problems 2003.
 
1. Kripke style models for LP. Even a soundness alone would be a good thing. A completeness is desirable. This problem is vague by its nature. There are some known solutions which do not count. For example, Artemov/Sidon models for mixed languages with \Box and p:F, where every "quasiatomic" formula p:F is either uniformly true or uniformly false do not do the job. A projection of such a model on the language of LP is trivial, hence, has no value for studying LP itself. What one has to look for is a real semantics, where a model has something like a collection of possible worlds (= states of knowledge) and accessibility relation reflecting degrees of knowledge, a formula is evaluated by an induction on complexity. It is natural to expect that some kind of a limit procedure should give the usual S4 models. This is a sort of solution which "you know it, when you see it". Possible starting points here are Kripke models for lambda-calculi (cf. [Mitchell 1990]), "maximal consistent" model for LP [Artemov 1995], [Artemov 2001] and Mkrtychev models for LP [Mkrtychev 1997].
   
   Comment. A solution was given in [Fitting 2003] and [Fitting 2005]. This semantics combines Kripke features and the `evidence function' first appeared in [Mkrtychev 1997]. In particular, Mkrtychev models are Fitting models with singleton domains. Fitting models and their more advanced versions became a valuable tool in the logics of evidence-based knowledge featuring both modalities and proof polynomials (cf. [Artemov and Nogina 2005], [Artemov 2004b]).
    
2. Give a game semantics for proof polynomials and the Logic of Proofs.
    
3. Find a categorical semantics for the Logic of Proofs.
    
4. Consider Basic Intuitionistic Logic of Proofs (BILP) which is a system where the only proof polynomials are variables and axioms/rules are propositional intuitionistic axioms;
   x:F->F (reflexivity);
   x:F v -x:F (decidability of x:F);
   modus ponens.
   Question: whether BILP is complete with respect to HA? More general problems: find complete logics of proofs for HA
   a) in the language of BILP;
   b) in the language with application, proof checker;
   c) in the language with application, proof checker, union.
   Study extensions of ILP and ILP+ by new operations corresponding to other admissible rules in HA.
   
   Comment. Iemhoff noticed that BILP was not complete with respect to HA. Problem 4a) was solved in [Artemov and Iemhoff 2005]. It looks 4b) and 4c) could be approached within the same group of ideas.
    
5. The arithmetical completeness of LP operated with the class of "normal" proof predicates, not necessarily the usual Goedel proof predicate. Find the propositional Logic of Proofs for the usual Goedel proof predicate. Some partial results can be found in: [Artemov and Strassen 1993], [Yavorsky 2000].
    
6. Logic of Proofs with quantifiers over proofs. Consider LP-language without operations and constants, i.e. in a formula t:F, term t is a proof variable. Extend it by adding quantifiers and over proof variables. The collection of all formulas true for all normal proof predicates is not axiomatizable, i.e. not recursively enumerable (cf. [Yavorsky 2002]).
   a) Assume the abbreviation []F= x(x:F). Consider the following formal system LPq in the language with quantifiers over proofs (above):
   1. axioms and rules of the FO classical logic in the language of LPq
   2. [](F->G)->([]F->[]G)
   3. []F->[][]F
   4. -x:A -> []-x:A
   5. c:F->F, c a constant
   Rules: F => [] F, []F => F.
   Whether LPq is decidable? The same question about the fragment of LPq without propositional variables (with \bot the only atomic formula)? What are Kripke models for LPq? Since the usual LP operations are definable in LPq (see [Yavorsky 2002]), this could provide a Kripke semantics for LP.
   b) Take all tautologies on the language of LPq true for the standard Goedel proof predicate. Whether this system is decidable? Recursively enumerable? Again: what about this system without propositional variables? Some interesting fragment of this logic was proved to be decidable in [Yavorsky 2003].
   
   Comment: 6a) was answered negatively by R.Yavorsky in 2003 (private communication). He also showed that the fragment of LPq without propositional variables was undecidable. M.Fitting in [Fitting 2004b] found a conservative extension of LP by quantifiers over proofs such that its modal projection is exactly S4. Fitting's logic provides a promising tool in studying epistemic logic with evidence.
    
7. Confirm the Artemov-Buss conjecture that LP is the logic of proofs for bounded arithmetics S-1-2. The standard completeness proofs for LP w.r.t PA ([Artemov 1995], [Artemov 2001]) should work for S-1-2 with some modifications.
    
8. Find a second order logic of proofs that corresponds to the second order arithmetic in some of its standard formulations. There are two natural versions of this problem: classical and intuitionistic. One could expect new second order principles for lambda-calculus there.
    
9. Establish exact place of LP in the known complexity classes. Roma Kuznetz in [Kuznets 2000], proved that SAT for LP is in \Sigma-2-P. Nikolai Krupski in [N.Krupski 2003], found a representative fragment of LP, so-called Reflected LP, in NP.
   
   Comment: A fundamental study on the complexity of realization of S4 derivations by proof polynomials was made in [Brezhnev and Kuznets 2005].
    
10. Strong normalization for a Gentzen style formulation of LP. Normalization is proven in Artemov-BSL. The same for a natural deduction system for LP (cf. [Artemov 2002].)
     
11. Does the first order analogue of the realization theorem of S4 in LP hold? About the first order LP cf. [Artemov and T.Sidon-Yavorskaya 2001].
     
12. Extend the Brouwer-Heyting-Kolmogorov semantics of propositional intuitionistic logic HPC in LP to the first order case. One way to handle this is to skolemize the usual quantifiers in HPC first and then to realize the resulting system in the quantifier-free first order LP. Mind the fact that skolemization in intuitionistic logic is not at all trivial. Is Markov Principle realizable?
    
    Comment: Problem #33 points to the next natural step toward solving #12.
     
13. Find a tableau proof system for LP. Compare this to S4 tableau proof system. Find a realization algorithm of S4 in LP via tableau proofs.
    
    Comment: Solved in [Renne 2004]. Cf. also [Fitting 2004a].
     
14. Find a proof of the Realization Theorem of S4 in LP which does not use cut-elimination of S4. This could shed some more light on how to prove realization theorems for not cut-free systems. Even for modal logics with cut-elimination this could be a step forward, since eliminating cuts is a computationally costly procedure.
    
    Comment: Solved in [Fitting 2003] and [Fitting 2005].
     
15. Consider basic Epistemic Logic with Justification ELJ=S4+LP+ some natural principles connecting \Box and t:F. Those principles can be taken from [Yavorskaya 2002]. A possible approach: start with reading Yavoraskaya paper above, find Kripke style models, establish cut-elimination, decidability, internalization property, reasonable complexity bounds. Establish a property that every ELJ theorem admits a realization of its modalities by ELJ proof polynomials.
    
    Comment: Solved in [Artemov and Nogina 2005] and [Artemov 2004b]. The remaining question has been shaped as #29.
     
16. Similar projects for S5 and other major epistemic logics.
     
17. Is modal logic self-referential? A realization algorithm of S4 in LP (cf. [Artemov 2001]), in principle, can lead to self-referential constant specification c:A(c). Can one realize S4 in LP without such specifications? There is an obvious generalization of self-referentiality that accommodates longer circles of dependencies like c:A(d) and d:B(c). Is there a realization of S4 in LP without this kind of self-referential circles?
    
    Comment: Solved by Kuznets, cf. [Brezhnev and Kuznets 2005]
     
18. Find bi-modal logic of proofs corresponding to two interacting proof systems. There are several natural cases: systems are of equal power, one is superior to the other (is able to proof check its proofs?).
    
    Comment: See a more specific version of this problem in #23 of this list.
     
19. System \lambda-inf ([Alt and Artemov 2001]) can be naturally embedded to LP by emulated lambda-abstraction a la Curry. In this respect \lambda-inf is a proper fragment of LP without polymorphism and without +. Find lambda-calculi that correspond to intuitionistic versions of Z (i.e. a +-free LP). Starting from a lambda-calculus for the classical logic, find a lambda-calculus corresponding to the whole of LP. This may be closely related to another question: find the propositional logic of natural deduction proofs. This line of research is really about finding new powerful operations for lambda-calculi in general to be applied in a wide range of environments, including computational and programming languages ones.
     
20. Is there a natural embedding of LP, \lambda-inf into ITT? This would provide an interesting new semantics of LP. Build a reflexive extension of ITT in the style of \lambda-inf, find a model.
     
21. Is there a system in the Barendregt cube which naturally contains \lambda-inf? A research program: build reflexive extensions of all known \lambda-calculi in the style of \lambda-inf. The program adds a new "fourth" dimension to the Barendregt cube.
     
22. Build the logic of proofs for resource-conscious systems (Girard's Linear Logic, Japaridze's Computability Logic). A possible semantics here: a formula A is a resource; a proof polynomial p is an address there this resource can be stored; p:A is a formula stating that A is indeed stored in p, which itself can be regarded as a(n intelligence) resource.
     

 
  Problems 2005.
 
23. Study "bimodal" LP, consisting of two copies of LP with disjoint sets of proof polynomials and with proof assertions t:F denoted as t[1]F for the first of them and t[2]F for the second. Examples of such systems suggested are:
    (A) Basic = LP[1]+LP[2] and no cross principles. In particular, c[1](t[1]F->F) is in Basic, but c[2](t[1]F->F) is not.
    (B) One way trust = Basic plus c[2]A for each axiom A of LP[1].
    (C) Mutual trust = Basic plus c[i]A for each axiom A of LP[j], i,j=1,2.
    (D) Trust-but-verify = Mutual trust plus t[1]F -> !t[2]t[1]F.
    (F) Mutual verification = Trust-but-verify both ways.
    Other possible principles to consider
    t[1]F -> t[2]F (hidden dominance)
    t[1]F -> t[2]F under the scope of constant specification for LP[1] = secret (for 2) dominance
    t[1]F -> t[2]F with constant specifications for both LP[1] and LP[2] = open dominance
    Natural questions here are: internalization property, Mkrtychev and Fitting models and decidability, correspondence to bi-modal logics. What kind of bimodal LP is needed for realization of bimodal S4?
     
24. Establish decidability of evidence-based knowledge systems T_nLP, S4_nLP, S5_nLP (and their forgetful counterparts T_nS4, S4_nS4, S5_nS4). The same question for the systems with the weak negative introspection principle -t:F -> []-t:F (cf. [Artemov 2004b], [Artemov and Nogina 2005]).
     
25. Consider the belief version of LP, LP_K4}, which we will call here the Logic of explicit Beliefs (LB). As was shown in [Brezhnev 2000], LB is arithmetically complete and realizes K4. Mkrtychev- and Fitting-models for LB, decidability and complexity bounds were found in [Kuznets 2000] and [Fitting 2005]. Study logic of explicit and implicit beliefs K4+LB (similar to S4LP) and its generalizations: T_nLB, S4_nLB, S5_nLB, K4_nLB, etc. (cf. [Artemov 2004b], [Artemov and Nogina 2005]). Natural questions here are models, complexity, realization theorem similar to #29 in this list.
     
26. Find complexity classes that suit to systems from 24 and 25. The expected result here is the the evidence-based knowledge and belief systems are generally less complex than the corresponding common knowledge and belief systems. (Cf. [Fagin, Halpern, Moses, and Vardi 1995].)
     
27. Find topological models for the basic epistemic logics with justification S4LP and S4LPN from [Artemov and Nogina 2005]. Investigate completeness (cf. [Esakia 2004]).
     
28. Find game theoretical semantics for the evidence-based knowledge systems. This may be relevant to future applications of the evidence-based knowledge systems in game theory. Cf. [Johan van Benthem 2001] for a survey of games in epistemic logics.
     
29. Prove the realization theorem for the epistemic logic with justifications S4LP: In any S4LP-derivation all modalities which are not under the scope of explicit justifications can be realized by S4LP proof polynomials. This result would substantially extend the realization theorem of S4 in LP. (Cf. [Artemov 2001], [Brezhnev and Kuznets 2005])
     
30. Introduce S5LP (= S4LP + "-[]F -> []-[]F" (cf. [Artemov and Nogina 2005], study its models, decidability and complexity, its forgetful projection. Establish the realization theorem: S5LP realizes all S4-modalities in S5₁S4 (in the notations from [Artemov 2004b]. The problem here is that S5 does not have the usual cut-elimination with subformula property, neither does S5₁S4, hence some tricks are needed. Some useful ideas could also be found in [Fitting 2005], where a technique of proving realization theorem has been developed which does not use cut-elimination.
     
31. Prove that S5_nS4 can be realized in S5_nLP. This is an important case in the evidence-based knowledge which we still don't have a realization theorem (cf. [Artemov 2004b]). The key case is n=1 (cf. # 30 in this list).
     
32. Introduce and study evidence-based systems S5_nAKS, where AKS is the explicit version of S5 from [Artemov, Kazakov and Shapiro 1999]. S5_nAKS is the strongest evidence-based knowledge system so far. Prove that its forgetful projection is S5_nS5. Again, the key case here is n=1.
     
33. Find axiomatization of the quantifier-free first order logic of proofs with equality. The main challenge here will be to find the right formulation of the equality axiom. The standard form of it, (u=v) -> (F(u)->F(v)), is not epistemically valid when F(x) is t:G(x). Indeed, if an agent has an evidence t of F(u) but does not know that u=v, then there is no reason for the agent to assume that t is an evidence for F(v) as well. For basic definitions of the first order logic of proofs see [Artemov and Yavorksya 2001]. This problem may become a step toward solving #12.
     
34. Introduce and study distributed knowledge into the systems of evidence-based knowledge. (Cf. [Fagin, Halpern, Moses, and Vardi 1995].)
     
35. Consider the reflexive combinatory logic RLC from [Artemov 2004a] , [N.Krupski 2005]. Along with the usual typed combinatory logic reductions
    i) Kxy => x
    ii) sxyz => xz(yz)
    consider new reductions
    iii) d(cy) => y
    iv) d(!u) => u
    v) c(!u) => !!u
    vi) o(!u)(!v) => !(u v)
    Study Church-Rosser property and normalization of RCL with respect to reductions
    a) i - iii
    b) i - v
    c) i - vi .
    Introduce a congruence relation based on these reductions and emulate lambda-abstraction in the resulting system, for example, in the Curry style ([Troelstra and Schwichtenberg 1996]).
     
36. What kind of (reflexive) lambda-calculi corresponds to the reflexive combinatory logic RCL? The same question about RCL with congruences a), b), and c) from #35.
     

References.