The breakdown from natural language to logic seems incomplete in respect to the level of mechanism required. In the S4 example there are pharses like S1:”this topic”, S2:”those five”, S3:”conversely” which do not make sense when read only on their own but refer to shared objects. The natural language is also strctured to be claim-evidence when logic structure is axioms-theorem.
Part of the point is that in the debate only the last “stop claim” needs to be checked by the judge. If I try to read only “is judged” arrowed part I can’t judge it. What is y, a, b or a1, b1, an, bn? If the letters broken down into number subscripts is supposed to represent a unselected explanation it kinda fails as I have to refer to it to get subscript terms defined. Y is defined two levels up. This is fine if I have been following the generation of the tree but not if I want to have accessed only as few nodes as possible.
Feels handwavy where the reader is left to make it technically competent if they are interested to do so.
Good observation.sfinal is not the same as the string that represents it in the transcript (the “Now we have y=a⋅b [...]” in the example). I can see how the way I’ve written the post suggests that it is; this is a mistake.
sfinal (and statements in general) can depend on other concepts in the transcript. If cross-examination (which I think does have a place in Ideal Debate) is allowed, they can even depend on concepts that haven’t been introduced in the transcript, and which the first agent only defines after the second agent pointed to sfinal. E.g., the first agent could just postulate that a set Pq exists without saying anything about its properties until they matter for the argument. This is fine as long as there is a mechanism that forces the first agent to be consistent (which is exactly what cross-examination does).
In general, statements are not strings. The same string can map to several different statements if the words refer to different things, and the length of the corresponding string doesn’t meaningfully restrict the actual complexity. I think of ambiguous words much like of concepts that haven’t yet been defined. This is what I was getting at by saying that ambiguity has been abstracted away.
What this does suggest in the formalism as-is is that the difficulty (in terms of dh) of statements will tend to go up if they are later in the debate since they depend on more prior concepts. (Does that mean the judge effectively has to deal with the entire problem after all? Absolutely not; the key move the first agent can pull over and over again is to hide most of the complexity of a concept. The second agent can only question one claim, so whenever she accepts that a certain thing exists, the first agent gets away with only defining the properties of that thing that are relevant for sfinal. E.g., in a more complicated mathematical proof, the first agent may say something like ‘there is a function with properties x and y’, and if the second agent chooses not to doubt that this function exists, then the first agent gets away with never talking about how the function was constructed, which may exclude pages of work. This is why I’ve written post #-1.)
I’ve previously had the vague plan to make an additional post about this stuff after the main sequence. Maybe instead, what I’ve just said here should be in this post, not sure yet. I’ll definitely change something to make it clear that statements≠strings. [Edit: for now, I added two paragraphs at the end of chapter 1.]
I’ve so far not thought about extending the formalism to model this explicitly. It’s not an unreasonable idea, but my current sense is that it doesn’t need to be included. Maybe I’ll change my mind about this.
The breakdown from natural language to logic seems incomplete in respect to the level of mechanism required. In the S4 example there are pharses like S1:”this topic”, S2:”those five”, S3:”conversely” which do not make sense when read only on their own but refer to shared objects. The natural language is also strctured to be claim-evidence when logic structure is axioms-theorem.
Part of the point is that in the debate only the last “stop claim” needs to be checked by the judge. If I try to read only “is judged” arrowed part I can’t judge it. What is y, a, b or a1, b1, an, bn? If the letters broken down into number subscripts is supposed to represent a unselected explanation it kinda fails as I have to refer to it to get subscript terms defined. Y is defined two levels up. This is fine if I have been following the generation of the tree but not if I want to have accessed only as few nodes as possible.
Feels handwavy where the reader is left to make it technically competent if they are interested to do so.
Good observation.sfinal is not the same as the string that represents it in the transcript (the “Now we have y=a⋅b [...]” in the example). I can see how the way I’ve written the post suggests that it is; this is a mistake.
sfinal (and statements in general) can depend on other concepts in the transcript. If cross-examination (which I think does have a place in Ideal Debate) is allowed, they can even depend on concepts that haven’t been introduced in the transcript, and which the first agent only defines after the second agent pointed to sfinal. E.g., the first agent could just postulate that a set Pq exists without saying anything about its properties until they matter for the argument. This is fine as long as there is a mechanism that forces the first agent to be consistent (which is exactly what cross-examination does).
In general, statements are not strings. The same string can map to several different statements if the words refer to different things, and the length of the corresponding string doesn’t meaningfully restrict the actual complexity. I think of ambiguous words much like of concepts that haven’t yet been defined. This is what I was getting at by saying that ambiguity has been abstracted away.
What this does suggest in the formalism as-is is that the difficulty (in terms of dh) of statements will tend to go up if they are later in the debate since they depend on more prior concepts. (Does that mean the judge effectively has to deal with the entire problem after all? Absolutely not; the key move the first agent can pull over and over again is to hide most of the complexity of a concept. The second agent can only question one claim, so whenever she accepts that a certain thing exists, the first agent gets away with only defining the properties of that thing that are relevant for sfinal. E.g., in a more complicated mathematical proof, the first agent may say something like ‘there is a function with properties x and y’, and if the second agent chooses not to doubt that this function exists, then the first agent gets away with never talking about how the function was constructed, which may exclude pages of work. This is why I’ve written post #-1.)
I’ve previously had the vague plan to make an additional post about this stuff after the main sequence. Maybe instead, what I’ve just said here should be in this post, not sure yet. I’ll definitely change something to make it clear that statements≠strings. [Edit: for now, I added two paragraphs at the end of chapter 1.]
I’ve so far not thought about extending the formalism to model this explicitly. It’s not an unreasonable idea, but my current sense is that it doesn’t need to be included. Maybe I’ll change my mind about this.