Question #1: Groovy Logic Decidable? Selmer Bringsjord IFLAI2 Fall 2021 version 0927211215NY Submission Mechanics, Deadline This, the first of our questions for grading factor 2 (see syllabus), is due by October 7 at 3pm NY time that day. Submission is by emailing Selmer.Bringsjord@gmail.com 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 inL1 is Turing-decidable (where theorems must be proved using the inference rules/schemata of HyperSlate® forL1). 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. 2


































































学霸联盟