Talk:Post canonical system

Improving the Understandability

The definition includes production rules with multiple antecedents, but it does not describe the manner in which such a rule is to be "applied" to a string. The example does not include any multiple-antecedent rules.

In the section "Normal-form Theorem", upper-case roman letters are apparently used to denote variables, but there is no comment on this notation. In the definition at the beginning of the page, subscripted dollar signs are used for variables (perhaps as a meta-notation). In any case, when the reader encounters, e.g., gP --> Ph, it is not immediately clear that P is to be regarded as a variable.

Dragomiloff59 (talk) 17:29, 22 August 2012 (UTC)

Funny, I looked at this talk page because I had the same experience. As a possible excuse, it comes to my mind that the notation might be just Post's original one, and Post might neither have explained his notation properly. From reading a few original papers in mathematics and metamathmatics from around the 20s, and perhaps also from talks by "post-intuitionists" (constructive mathematics ...), my impression is that time notations often were not as "formal" as nowadays, so there was no other way to understand notations than by "intuition" ... and when you try to present such works in a more formal way in the strict sense of nowadays, you realize that you really don't understand what those authors meant. Or you read a modern presentation of some old work and realize that it is just one arbitrary interpretation of the original work among other possible ones. Lueckless (talk) 08:42, 21 September 2012 (UTC)

OK, in $gP\to Ph$, $P$ is $\$_{1}$ from above, $g$ is $g_{0}$, $g_{1}$ and $h_{0}$ are empty, and $h$ is $h_{1}$. I had not read the general section properly, only after seeing PlanetMath.org. Lueckless (talk) 11:19, 21 September 2012 (UTC)

So far I had not thought about the first matter above, multiple antecedents. Typical examples are derivation rules in formal logic (e.g., thinking of propositional calculus#Argument)—intuitively, I am unable right now to represent, e.g., propositional logic as a Post canonical system, problem being respecting brackets. But see a restricted example: A = {"0", "1", "2", "<"}, I = {"0<1", "1<2"}, R = {(S<T, T<U → S<U)} (this notation still is sloppy). The only possibility to apply the single production rule to elements of I produces "0<2". The only possibilities to apply the single production rule to elements of I twice result from applying the rule once to the results L = I ∪ {"0<2"} = {"0<1", "1<2", "0<2"} and still only yield "0<2". The latter reasoning generalizes to the induction step of a mathematical induction on the number of applications of the rule, and this proves that the "formal language" generated by this system just is the set of words L. So this system represents all the true statements about for which numbers m and n from {0, 1, 2} the relation m < n holds. The production rule "formalizes" that < is a transitive relation. Lueckless (talk) 14:02, 21 September 2012 (UTC)

Example (well-formed bracket expressions)

This example seams inconsistent. Rule (3) appears to be backwords. Shouldn't:

(3)       $1[]$2 → $1$2

be:

(3)       $1$2 → $1[]$2

That just to be consistent with the way rules 1 and 2 transforms are applied:

Alphabet: {[, ]}
Initial word: []
Production rules: 
(1)       $ → [$]
(2)       $ → $$
(3)       $1$2 → $1[]$2

Derivation of a few words in the language of well-formed bracket expressions:

       []             initial word
       [][]           by (2)
       [[][]]         by (1)
       [[][]][[][]]   by (2)
       [[][]][][[][]] by (3)
       ...

Note. Rule 3 has two symbols on the left taking it out of the Chomsky CFG catagory.

Steamerandy (talk) 20:54, 2 March 2016 (UTC)