User:Wvbailey/Parsing PM

This is a sandbox page for a look at how to parse the propositional formulas in Principia Mathematica. ⊃ Ɔ ≡ ⊂ ∪ ∩ ∨ ∧ ∨ ∩ ∪ ⊂ ⊃ Ɔ ≡ ε Λ ℩ ⊓ ⊔ ▪■︰✸ ✹ ✱ ∪ ∩ ∨ 〉 〈 ≡ ⇒ ⊃ ⊏ ⊐ ⊢ ⊦

Algorithm development

Peano 1889

van Heijenoort comments that "Peaon's notation is quite superior to that of Boole and schroeder, and it marks an important transition toward modern logic" (p. 84). He primarily faults Peano on his lack of a rule of detachment (modus ponens). But what about his symbolism? How does that fare?

Peano states:

We shall generally write signs on a single line. To show the order in which they should be taken, we use parentheses, as in algebra, or dots, ., :, :., ::, and so on.

"To understand a formula divded by dots we first take together the signs that are not separated by any dot, next those sperarted by one dot, then thos seqparated by two dots, and so on.

For example, let a, b, c, . . . be any signs. Then ab.cd means (ab)(cd); and ab.cd:ef.gh:.k means (((ab)(cd))((ef)(gh)))k." (p. 86)

What is key here is Peano's definition of logical and and his subsequent abbreviation:

"The sign ∩ is read and. Let a and b be propositions; then a ∩ b is the simultaneious affirmation of the propositions a and b. For the sake of brevity, we ordinarily write ab instead of a ∩ b." (p. 87)

The question becomes, can the example be parsed, i.e. converted back into a formula with the familiar parentheses. What we will attemp is have a "production" of the following form, where ssss is a symbol-string made of symbols that are not dots. In other words the search left or right through the string stops when a dot is encountered, or an end of the formula. The symbols ⊏ and ⊐ are "directives" to remind us that we have to go left and right through the string s

s.s ⇒ s[ )( ]s

s:s ⇒ s[ )( ]s, etc.

But what happens when the symbol string includes dots of a lower number? For example, what happens in this case:

abc.def:gh:.jk.l

Peano wants us to start with the lowest number of dots. In this example this would be 1 dot. This occurs two places

ab.cd:ef.gh:.k ⇒ ab [ )( ] cd:ef.gh:.k

search left thru ab and hit left end of formula: [ab)( ]cd:ef.gh:.k

search right through cd and hit double-dot and stop: [ab)(cd]:ef.gh:.k

[ab)(cd]:ef.gh:.k ⇒ [ab)(cd]:ef [ )( ] gh:.k ⇒

search left until either dots are hit or end of string: [ab)(cd]:[ef)( ] gh:.k

search right until either dots are hit or end of string: [ab)(cd]:[ef)(gh]:.k

One-dot occurrences are exhausted. Now proceed to 2-dot occurrences:

[ab)(cd]:[ef)(gh]:.k ⇒ [ab)(cd] [ )( ] [ef)(gh]:.k

search left until either dots are hit or end of string: [[ab)(cd])( ] [ef)(gh]:.k

search right until either dots are hit or end of string: [[ab)(cd])([ef)(gh]]:.k

Two-dot occurrences are exhausted. Now proceed to 3-dot occurrences:

[[ab)(cd])([ef)(gh]]:.k ⇒ [[ab)(cd])([ef)(gh]][ )( ] k

search left until either dots are hit or end of string: [[[ab)(cd])([ef)(gh]])( ] k

search right until either dots are hit or end of string: [[[ab)(cd])([ef)(gh]])(k]

Clean-up: change the brackets to parentheses:

(((ab)(cd))((ef)(gh)))(k)

With the exception of the right-most (k) this agrees with Peano's example.

Let try #6 in his list of "Propositions of logic"

a = b.b ⊃ c :⊃. a⊃c ⇒ a = b [ )( ] b ⊃ c :⊃. a⊃c ⇒ [ a = b )( b ⊃ c ]:⊃. a⊃c ⇒

[ a = b )( b ⊃ c ] : ⊃. a ⊃ c ⇒ [ a = b )( b ⊃ c ] : ⊃ [ )( ] a⊃c ⇒ [ a = b )( b ⊃ c ] :[ ⊃ )( a⊃c ] ⇒

[ a = b )( b ⊃ c ] :[ ⊃ )( a⊃c ] ⇒ [ a = b )( b ⊃ c ] [ )( ] [ ⊃ )( a⊃c ] ⇒ [[ a = b )( b ⊃ c ] )([ ⊃ )( a⊃c ] ]

cleanup the : ((a = b )( b ⊃ c )) (( ⊃ ) ( a⊃c ))

Reinsert the sign for logical and:

cleanup the : ((a = b )∩( b ⊃ c )) ∩(( ⊃ )∩ ( a⊃c ))

Does this make sense? If a equals b and b implies c, then a implies c. it does make sense but only if we can figure out what is to be done with the odd ∩(( ⊃ )∩. Here's Peano's answer:

"Punctuation signs may be omitted if . . . only one formula, which is just the one we want to write, has meaning." (p. 87)

In other words, just use your intuition.

References

• Pope, Taylor, Waylaard [no date], "Monadic Parsing: A Case Study",