# 辅导IFLAI2程序语言、辅导R编程

- 首页 >> Algorithm 算法 Question #1: Groovy Logic Decidable?

Selmer Bringsjord

IFLAI2 Fall 2021

version 0927211730NY

Submission Mechanics, Deadline

a proposed answer in the form of a pdf file produced from use of LATEX. You must use LATEX to

write your answer. The question itself is given at the end of the present document, and, note,

leaves wide open the possibility of getting full credit on this without supplying anything like a full

proof. The most important thing is effort and thoughtfulness. (The second requires the first.) We

will have some time to discuss this question in class, starting with class on Sept 27.

Background

We now know from Church’s Theorem that theoremhood in L1 is Turing-undecidable (where

theorems must be proved using the inference rules/schemata of HyperSlate? for L1). In the Fall

2020 version of IFLAI2, students therein undertook to settle whether theoremhood in L0 is Turing-

decidable (the answer is “Yes,” but we don’t review any proof of this affirmative here). Now we

consider another logic: groovy logic.

Let’s consider first an example of a formula in groovy logic. Here’s an English sentence s that

defines the new concept of pairs of people who are hyper-compatible with each other, a concept

that we identify with the binary relation HC:

“Hyper-compatible pairs (of people) are compatible pairs all of whose mutual friends

are compatible with someone.”

Let’s use the binary relation C to denote compatibility, and MF to denote mutual friendship. Then

here’s a representation of s in L1:

φs := ?x1?x2[HC(x1, x2)? (C(x1, x2) ∧ ?x3(MF (x1, x2, x3)→ ?x4C(x3, x4)))]

Do you notice anything, so to say, “well-behaved” about this formula? Hopefully you do.

For one thing, all the sub-formulas that use relation symbols keep their variables “lined up” in a

sequence — assuming that there is some ordered set in the background for the available variables,

and indeed (I hereby inform you that) there is; it’s

X4 := {x1, x2, x3, x4}.

We might say that our variables are placed neatly into “grooves.” In addition, the quantification

scoping isn’t nested in a complicated way.

We can make the well-behavedness of groovy logic precise by way a trio of formation principles

for the well-formed formulae of groovy logic. These principles assume that we have a finite set R

of n-ary relation symbols, and an ordered set

Xk := {x1, x2, . . . , xk}

1

of object variables. These principles also assume that we define an atomic groovy formula over R

and Xi as an atomic formula

Rn(xl, . . . , xi)

where n ≤ i and the sequence of variables here are in ascending order relative to the given ordered

set Xk of object variables. Look at how this works in the formula φs above. There, MF is a ternary

relation, and the sub-formula MF (x1, x2, x3) has variables in ascending order. Now here are the

three formation principles that define the formulae of groovy logic:

P1 Every atomic groovy formulae over a R and Xi is a groovy formula over R and Xi.

P2 If φ is a groovy formula over R and Xi+1, then ?xi+1φ and ?xi+1φ are groovy

formulae over R and Xi.

P3 If φ and ψ are groovy formula over R and Xi, then so are φ ∨ ψ, φ ∧ ψ, φ → ψ,

φ? ψ, and ?φ (and ?ψ).

As you can see (perhaps after some study) all atomic formulae of groovy logic must obey the under-

lying ordering of variables that is pre-set. We also consider, of course, proper fragments of groovy

logic, e.g. the fragment in which we restrict k in the background Xk to some particular natural

number, say 4 (as I did above). Let’s dub groovy logic by ‘Lg,’ and the fragment corresponding

to an ordered set of 4 variables by ‘Lg4.’ Obviously the ‘4’ here is completely arbitrary: there is a

fragment for every natural number.

The Question Itself

And now, finally, we come to our question, which is really quite simple to express:

Q1 Is theoremhood in Lg Turing-decidable?

Answer with ‘Yes’ or ‘No,’ and justify your answer as rigorously as you can. While a full

proof would certainly be ideal, a thoughtful, rigorous argument is sufficient if such a proof can’t

be obtained. Even incorrect answers that show hard-won thoughtfulness can get full credit on this

question. In addition, assign yourself a grade on the scale of 4 = truly excellent, 3 = good, 2 =

acceptable, 1 = unacceptable.

Selmer Bringsjord

IFLAI2 Fall 2021

version 0927211730NY

Submission Mechanics, Deadline

a proposed answer in the form of a pdf file produced from use of LATEX. You must use LATEX to

write your answer. The question itself is given at the end of the present document, and, note,

leaves wide open the possibility of getting full credit on this without supplying anything like a full

proof. The most important thing is effort and thoughtfulness. (The second requires the first.) We

will have some time to discuss this question in class, starting with class on Sept 27.

Background

We now know from Church’s Theorem that theoremhood in L1 is Turing-undecidable (where

theorems must be proved using the inference rules/schemata of HyperSlate? for L1). In the Fall

2020 version of IFLAI2, students therein undertook to settle whether theoremhood in L0 is Turing-

decidable (the answer is “Yes,” but we don’t review any proof of this affirmative here). Now we

consider another logic: groovy logic.

Let’s consider first an example of a formula in groovy logic. Here’s an English sentence s that

defines the new concept of pairs of people who are hyper-compatible with each other, a concept

that we identify with the binary relation HC:

“Hyper-compatible pairs (of people) are compatible pairs all of whose mutual friends

are compatible with someone.”

Let’s use the binary relation C to denote compatibility, and MF to denote mutual friendship. Then

here’s a representation of s in L1:

φs := ?x1?x2[HC(x1, x2)? (C(x1, x2) ∧ ?x3(MF (x1, x2, x3)→ ?x4C(x3, x4)))]

Do you notice anything, so to say, “well-behaved” about this formula? Hopefully you do.

For one thing, all the sub-formulas that use relation symbols keep their variables “lined up” in a

sequence — assuming that there is some ordered set in the background for the available variables,

and indeed (I hereby inform you that) there is; it’s

X4 := {x1, x2, x3, x4}.

We might say that our variables are placed neatly into “grooves.” In addition, the quantification

scoping isn’t nested in a complicated way.

We can make the well-behavedness of groovy logic precise by way a trio of formation principles

for the well-formed formulae of groovy logic. These principles assume that we have a finite set R

of n-ary relation symbols, and an ordered set

Xk := {x1, x2, . . . , xk}

1

of object variables. These principles also assume that we define an atomic groovy formula over R

and Xi as an atomic formula

Rn(xl, . . . , xi)

where n ≤ i and the sequence of variables here are in ascending order relative to the given ordered

set Xk of object variables. Look at how this works in the formula φs above. There, MF is a ternary

relation, and the sub-formula MF (x1, x2, x3) has variables in ascending order. Now here are the

three formation principles that define the formulae of groovy logic:

P1 Every atomic groovy formulae over a R and Xi is a groovy formula over R and Xi.

P2 If φ is a groovy formula over R and Xi+1, then ?xi+1φ and ?xi+1φ are groovy

formulae over R and Xi.

P3 If φ and ψ are groovy formula over R and Xi, then so are φ ∨ ψ, φ ∧ ψ, φ → ψ,

φ? ψ, and ?φ (and ?ψ).

As you can see (perhaps after some study) all atomic formulae of groovy logic must obey the under-

lying ordering of variables that is pre-set. We also consider, of course, proper fragments of groovy

logic, e.g. the fragment in which we restrict k in the background Xk to some particular natural

number, say 4 (as I did above). Let’s dub groovy logic by ‘Lg,’ and the fragment corresponding

to an ordered set of 4 variables by ‘Lg4.’ Obviously the ‘4’ here is completely arbitrary: there is a

fragment for every natural number.

The Question Itself

And now, finally, we come to our question, which is really quite simple to express:

Q1 Is theoremhood in Lg Turing-decidable?

Answer with ‘Yes’ or ‘No,’ and justify your answer as rigorously as you can. While a full

proof would certainly be ideal, a thoughtful, rigorous argument is sufficient if such a proof can’t

be obtained. Even incorrect answers that show hard-won thoughtfulness can get full credit on this

question. In addition, assign yourself a grade on the scale of 4 = truly excellent, 3 = good, 2 =

acceptable, 1 = unacceptable.