辅导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.