This website does readability filtering of other pages. All styles, scripts, forms and ads are stripped. If you want your website excluded or have other feedback, use this form.

Language and Semantics of Computability Logic

Computability Logic


Section 5

The language of CoL and its semantics

        5.1   Formulas

        5.2   Interpretations

        5.3   Validity

5.1 Formulas

It is not quite accurate to say “the language” of CoL because, as pointed out earlier, the latter has an open-ended formalism. Yet, in the present article, by “the language of CoL” we will mean the particular language defined below. It extends the language of classical logic by adding to it all operators listed in Section 3.1, and differentiating between two --- elementary and general --- sorts of nonlogical atoms.

The set Variables of variables and the set Constants of constants of the language are those fixed earlier when discussing games. We also have infinitely many nonlogical function letters, elementary game letters and general game letters. With each of these is associated a fixed natural number called the arity. We usually use f,g,h… as metavariables for function letters, p,q,r,… for elementary game letters, and P,Q,R,… for general game letters.  Other than  these nonlogical  game letters, there are three logical  letters,  all  elementary:  (nullary), (nullary) and = (binary). 

Terms are defined inductively as follows:

  • All variables are terms.
  • All constants are terms.
  • If t1,…,tn are terms (n≥0) and  f  is an n-ary function letter, then f(t1,…,tn) is a term.   

Atoms are defined by:

  • and  are atoms.
  • If tand t2 are terms, then t1=t2 is an atom.
  • If t1,…,tn are terms (n≥0)  and L is a nonlogical n-ary (elementary or general) game letter, then L(t1,…,tn) is an atom.

Finally, formulas are defined by:

  • All atoms are formulas.
  •  If E is a formula, then so are  (E),  (E),  (E),  (E),  (E),  (E),  (E),  (E),  (E),  (E),  (E), (E),  (E).
  • If E and F are formulas, then so are (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F),  (E)(F).   
  • If E is a formula and x is a variable, then x(E), x(E), x(E),  x(E),  x(E),  x(E),  x(E),  x(E),  x(E),  x(E) are formulas.

Unnecessary parentheses will be usually omitted in formulas according to the standard conventions, with partial precedence order as agreed upon earlier for the corresponding game operations. The notions of free and bound occurrences of variables are also standard, with the only adjustment that now we have eight rather than two quantifiers.

A sentence (closed formula) is a formula with no free occurrences of variables.

5.2 Interpretations

For the following definition, recall Conventions 2.4.3 and 2.4.4. Also recall that var1,…,varn are the first n variables from the lexicographic list of all variables.

Definition 5.2.1 An interpretation is a mapping * such that, for some universe U called the universe of *, we have: :

  • * sends every n-ary function letter f to an n-ary function f*(var1,…,varn) whose universe is U and whose variables are the first n variables of Variables. 
  • * sends every n-ary nonlogical game letter L to an n-ary static game L*(var1,…,varn)  whose universe is U and whose variables are the first n variables of Variables; besides, if the letter L is elementary, then so is the game L*.

Such a * is said to be admissible for a formula E (or E-admissible) iff, whenever E has an occurrence of an atom A(t1,….,tn) in the scope of  x or x and one of the terms ti (1≤in) contains the variable x, A* is unistructural in vari. We uniquely extend * to a mapping which sends each term t to a function t*, and each formula E for which it is admissible to a game E*, by stipulating the following (see Convention 2.4.3 for some notation used below):

  • Where c is a constant, c* is (the nullary function) cU
  •  Where x is a variable, x* is (the unary function) xU.
  • Where f is an n-ary function letter and t1,…,tn are terms, (f(t1,…,tn))* is f*(t1*,…,tn*).
  • * is  and * is .
  • Where t1 and t2 are terms, (t1=t2)* is t1*=t2*. 
  • Where L is an n-ary game letter and t1,…,tn are terms, (L(t1,…,tn))* is L*(t1*,…,tn*).
  • * commutes with all logical operators, seeing them as the corresponding game operations: (E)* is (E*), (E)* is (E*),  (EF)* is (E*)(F*), (xE)* is x(E*), etc.

When O is a function letter, a game letter, a term or a formula and O*=W, we say that * interprets O as W. We can also refer to such a W as “O under interpretation *”.

5.3 Validity

DeDefinition 5.3.1 Let S be a sentence. We say that:

  • S is logically (or uniformlyvalid iff there is an HPM M such that, for every S-admissible interpretation *, M computes S*. Such an M is said to be a logical (or uniformsolution of S.
  • S is nonlogically (or multiformlyvalid iff for every S-admissible interpretation * there is an HPM M such that M computes S*.

Convention 5.3.2 When S is a formula but not a sentence, its validity is understood as that of  the -closure of S, i.e., of the sentence  x1xnS, where  x1,...,xare all free variables of S listed according to their lexicographic order.

Every logically valid formula is, of course, also nonlogically valid. But some nonlogically valid formulas may fail to be logically valid. For instance, where p is a 0-ary elementary game letter, the formula p  p is valid nonlogically but not logically. It is nonlogically valid for a trivial reason: given an interpretation *, either p or p is true under *. If p is true, then the strategy that chooses the left disjunct wins; and if p is false, then the strategy that chooses the right disjunct wins. The trouble is that, even though we know that one of these two strategies succeeds, generally we have no way to tell which one does. Otherwise, we would have an answer to the question on whether there is life on Mars or not, or whether P=NP or not.  

The nonlogical validity of p p is not only non-constructive, but also a fragile sort of validity: this property, unlike logical validity, is not closed under substitution of atoms. For instance, where q is a unary elementary game letter, the formula q(x) q(x), while having the same form as p  p, is no longer nonlogically valid. The papers on CoL written prior to 2016 had a more relaxed understanding of interpretations than our present understanding. Namely, there was no requirement that an interpretation should respect the arity of a game letter. In such a case, as it turns out, the extensional difference between logical and nonlogical validity disappears: while the class of logically valid principles remains the same, the class of nonlogically valid principles shrinks down to that of logically valid ones. 

Intuitively, a logical solution M for a sentence S is an interpretation-independent winning strategy: since the “intended” or “actual” interpretation * is not visible to the machine,  M  has to play in some standard, uniform way that would be successful for any possible interpretation of S. It is uniform rather than multiform validity that is of interest in applied areas of computer science such as substantial theories (Section 7) or knowledgebase systems (Section 8). In these sorts of applications we want a logic on which a universal problem-solving machine can be based. Such a machine would or should be able to solve problems represented by logical formulas without any specific knowledge of the meanings of their atoms, i.e. without knowledge of the actual interpretation. In other words, such a machine has to be a logical rather than nonlogical solution.

For the above reasons, in the subsequent sections we will only be focused on the logical sort of validity.