May 24, 2009

Wittgensteinian- and Laozi-an-Inspired Take on Proof Theory and Formal Logic

I want to pose a bit of a conundrum I faced inspired by readings in Wittgenstein and Laozi. The idea, or problem, or whatever you might call it came to me while writing a larger treatise on the internal logic of the Daodejing, which in this instance involved early and late Wittgensteinian elements, and since I'm not one to discriminate ideas so fiercely by origin, I'll give inspirational credit to them both. The example is original, but those keen on the two figures I mention will see its sources almost immediately.

Let's imagine that I want to show a friend the rules of chess, but don't have a proper chessboard or pieces. In this absence, I decide to improvise all sorts of ways to mimic the terrain and pieces. I'll take bits of string, stray coins, checker pieces, gum wrappers, and so forth, and set them on an eight-by-eight grid that I penciled onto a sheet of looseleaf paper. Now, when I begin to describe how the "pawns," "knights," and other such pieces move, I'm able to convey, despite absence of a more conventional chess set, how the pieces move and describe the objective of the game. There is nothing seemingly important about using a horse-shaped piece as a symbol for the knight, nor a cross-headed top for the king, and all around, the function and practice of the game is preserved.

Given this, what would drive one to claim that the following two formal propositions are distinct?
  1. (∀x)(∀y)(Pxy ⊃ Qx), (∃x)(∃y)(Pxy & Rx) |- (∃x)(Qx & Rx)
  2. [(∀x)(∀y)(Pxy ⊃ Qx) & (∃x)(∃y)(Pxy & Rx)] ⊃ (∃x)(Qx & Rx)

Is there a major difference in stating that there exists a proof from some premises to another and simply stating that those premises imply the other? Now, I know that the first implies the second, but could the second just as well be translated into a game of the first and do away with this |- ("there exists a proof") business?

Let's imagine that I want to change the way most people make their moves in the predicate calculus. Instead of creating an open list of rules of inference that one may attempt, I instead create a strict ordered list of procedures to be followed that verify that the claim 2. is a theorem and that, unlike more common practices, tell you the minimum number of members required of the domain of discourse in that proposition.
  1. Write the proposition with all material conditionals altered via material implication: ~[(∀x)(∀y)(~Pxy v Qx) & (∃x)(∃y)(Pxy & Rx)] v (∃x)(Qx & Rx).
  2. Follow DeMorgan's Law, double negation, and change of quantifier rules until the only present negations are those of literals:
    • [(∃x)(∃y)(Pxy & ~Qx) v (∀x)(∀y)(~Pxy v ~Rx)] v (∃x)(Qx & Rx).
  3. Instantiate every variable, from outside to inside, giving one non-repeating constant to each existential quantifier and conjunction strings for every constant already present to each universal quantifier after instantiating all of the existential quantifiers where possible without violating instantiation rules. This will be called the "minimum extension" of the proposition.
    • [(Pac & ~Qa) v (∀x)(∀y)(~Pxy v ~Rx)] v (Qb & Rb).
    • [(Pac & ~Qa) v (∀y)((~Pay & ~Pby & ~Pcy) v (~Ra & (~Rb & ~Rc)))] v (Qb & Rb).
    • [(Pac & ~Qa) v ([((~Paa & ~Pba) & ~Pca) & ((~Pab & ~Pbb) & ~Pcb) & ((~Pac & ~Pbc) & ~Pcc)] v (~Ra & (~Rb & ~Rc)))] v (Qb & Rb).
  4. The number of distinct instantiations is the minimum number of constants needed within the domain to prove this statement valid in all cases (In this case, three.)
  5. Check each literal for the presence of a negation, and for those present use distribution and DeMorgan's Law to show that any contradiction in them is joined to the remainder of the proposition by a disjunct, and not a conjunct. For brevity in practice, it is acceptable to remove conjuncts within every disjunct that does not have any negations to them elsewhere in the proposition (in this case, anything that's not 'Pac' or '~Pac.')
    • [(Pac) v (~Pac)].
  6. Negate the minimum extension (or its form with eliminated irrelevancies, if brevity is desired).
    • ~[(Pac) v (~Pac)].
  7. Repeat steps 4 and 5 for the negated minimum extension (here made brief).
    • ~[(Pac) v (~Pac)].
    • [~(Pac) & ~(~Pac)].
  8. If one proposition produces a contradiction, but the other does not, then the one that does not produce a contradiction is a theorem. If neither produce a contradiction, then the proposition is not a theorem.

Contrast this with a common Fitch-style proof using Classical (at most) rules of inference:

  1. (∀x)(∀y)(Pxy ⊃ Qx)
  2. (∃x)(∃y)(Pxy & Rx)
    1. (∃y)(Pay & Ra)
      1. (Pab & Ra)
      2. (∀y)(Pay ⊃ Qa)
      3. (Pab ⊃ Qa)
      4. Pab
      5. Qa
      6. Ra
      7. Qa & Ra
    2. (∃x)(Qx & Rx)
  3. (∃x)(∃y)(Pxy & Rx) ⊃ (∃x)(Qx & Rx)
  4. (∃x)(Qx & Rx)

I ought to clarify these two different proofs as analogous to the chess issue. Both areas, in very distinct ways, prove the truth of a consequent claim from (an) antecedent claim(s) (implementing notions of plurality in a logic's propositional structure is rather nonsensical given that conjunctions and separated, but dual assertions of separate premises are equivalent). However, what is most striking is not that the proofs work out (though the former is a self-styled approach), but that they get to the same place by playing what some logicians would call a "different game." But how different is this game from the other? If at the most superficial syntactical level we are worried about presentation in the game, then we're really just harping at the semiotics of the game, just as I would with impromptu chess pieces.

That concern, however, is a mass distraction from a greater intuition, at least for me, that the game doesn't change, only the look of the game changes, and it's because none of these proofs carry weight without the rules, but none of those rules carry any weight without the presumption of implication.

I see a major problem with the notion of proof as being meaningfully distinct from just an implication. If a proof is a detailed assertion that a collection of premises implies a certain conclusion, and if an implication means that from the antecedent one is able to prove (via manipulations of smaller implications, via manipulations of small proofs) the consequent, then why would we bother treating proof (X |- Y) and implication (X ⊃ Y, or more primitively, ~X v Y) as separate concepts? Why would we convolute a formal language with a distinction of this sort if the function of logic is to take the primitives of thought and language and lay the foundation of incontrovertible inference?

We usually give a hoot about proof theory because we want to talk about the connection between a language's "syntax" and its "semantics?" Yet what makes us think that a semantic method of implication is somehow distinct from some other method of arriving at a conclusion from the premises? This strikes me as a translational problem, where we have two languages that both suffice to explain how propositions assert fact, and if asserted, guarantee the assertions of other propositions. I can take a formal proposition and prove that its premises imply the conclusion by so many different means, but in inquiring how exactly truth-functions tie to inference rules, for instance, I can create implications on the languages, themselves. However, I need not venture into some "new language" to do this. I can use the same language on a different tier with separate predicates, translating the statement for the soundness of a rule as follows:

(∀P)(∀Q)(∀x)(∀y)(Pxy ⊃ Qx), (∀P)(∀R)(∃x)(∃y)(Pxy & Rx) |- (∀Q)(∀R)(∃x)(Qx & Rx) implies
(∀P)(∀Q)(∀x)(∀y)(Pxy ⊃ Qx), (∀P)(∀R)(∃x)(∃y)(Pxy & Rx) |= (∀Q)(∀R)(∃x)(Qx & Rx) as (preliminarily)...

Where "U(XY)" means, "Use of group of moves X on proposition Y."
Where "C(XY)" means, "X is a conclusion from proposition Y."

Start more generally with...

(∃"Group of Moves"){[U("Group of Moves",[(∀P)(∀Q)(∀x)(∀y)(Pxy ⊃ Qx) & (∀P)(∀R)(∃x)(∃y)(Pxy & Rx)]) ⊃ C((∀Q)(∀R)(∃x)(Qx & Rx),U("Group of Moves",[(∀P)(∀Q)(∀x)(∀y)(Pxy ⊃ Qx) & (∀P)(∀R)(∃x)(∃y)(Pxy & Rx)])} ⊃ (∃"Group of Moves"){[U("Group of Moves",[(∀P)(∀Q)(∀x)(∀y)(Pxy ⊃ Qx) & (∀P)(∀R)(∃x)(∃y)(Pxy & Rx)]) ⊃ C((∀Q)(∀R)(∃x)(Qx & Rx),U("Group of Moves",[(∀P)(∀Q)(∀x)(∀y)(Pxy ⊃ Qx) & (∀P)(∀R)(∃x)(∃y)(Pxy & Rx)])}

Now, this is not final, since I have to define the groups of moves as a sequence or unordered group of moves that alters the premises to derive its sought conclusion.

If one performed a mathematical induction from this starting point, starting with the case of there being a proposition 0 operators in length, and then upon assuming a proposition of n operators in length, to show that it implies that it works for n+1 operators in length, that one can derive the longer single proposition above for any two adequate groups of moves.

This brings me back to the area of my concern. Chess pieces are the primitive operations on a chess board like primitive operations are in a formal logic. In relation to all of the locations on a chess board, a knight doesn't reduce into "sub-knights," each with their own independent moves because none of those "sub-knight" moves are legitimate for any piece that exists as a component of a knight. Knights have no components. Put another way, knights can't do less or more per move than their definition as a moving piece in chess allots. A knight is simply the maximum of eight operations from one of sixty-four starting positions -- up-up-left, up-up-right, right-right-down, etc. A primitive operation in logic only allows one move for any given grouping of terms in "logical space" (among delineated sets). Take negation -- inside a group to outside of that group. A knight represents its moves like a primitive logical operator represents its moves.

Moving in chess actually means employing one of the operations to achieve a valid result (and invalid result in chess would be one where say, the move puts the king in check, or moves a piece outside of the allotted spaces on the board, or puts two pieces of the same team on the same square) according to the operation that the piece represents. "Moving" in logic should be seen in the same way, and this sort of moving in logic is more clearly analogous with inference, not mere operation. This is where the attention in a formal language seems to go wrong if it continually introduces characters that it does not define as abbreviations of accepted primitives, representatives of moves in a game, but move in such a way that they can be translated back into a smaller group of more primitive operations.

Hence my distaste with all of the |-, and even |= talk. If we're abbreviating, let's see the fuller statement that it abbreviates. If we're not, and if we expect these notions to stand primitively, then we should have good cause to note differences between those operations and those operations that look much alike them (like commas [,] to conjuncts [&] and proof operations [|-,|=] to next-order sentential claims [e.g. above]). Too many logic books and books on proof theory just take these sorts of symbols for granted, and talk of them floats around rather loosely for such a definitional project.

Why an obsession with the primitives and definitional rigor, and how is this possibly inspired by Laozi and Wittgenstein? Submit the formal question to philosophical critique and general arguments about why rigor in assessment is a virtue, not a pedantry. The Daodejing has a number of chapters that, on the surface, just sound contradictory, but on another level of assessment, really don't say anything more than any formalism and primitive sense of language would already tell us. The two excerpts that impressed me most and triggered a personal awakening on the topic were the following (I have lumped them together, using the Wang Bi as source and borrowing from the Mawangdui scrolls in some areas marked in red.):

“All under Heaven knows beauty. This becomes beauty, as that is ugly already. They all know goodness. This becomes goodness, as that is bad already. Thus, having and lacking live together, difficulty and ease result together, longness and shortness appear together, highness and lowness are filled together, sounds and tones harmonize together, priority and posterity follow together. Partiality means wholeness, crookedness means straightness, emptiness means fullness, and tatters mean newness (天下皆知美。之為美,斯惡已。皆知善。之為善,斯不善已。故有無相生,難易相成,長短相形,高下相,音聲相和,前後相隨。曲則全,枉則直,窪則盈,敝則新。)” (2:1 - 2:12, 22:1 - 22:4).

If we are able to isolate all of the ways in which we are even capable of evaluating a system, then what Laozi says here is trivial, giving definitions of a term by identifying it in contrast to its negation. Of course, what he says becomes vastly, supremely more involved than just this, and Laozi is plenty enigmatic and thorough to match, but those sorts of insights require a development of what he says at the barest level.

However, when we evaluate statements for primitives, the most important thing for us to do is to check many of the generally accepted primitives to see if they can be "broken down" or "reduced" any further into even simpler concepts. My findings are that many can be, and actually can be quite efficiently and to an extent that an immensely strong logic, one that is modal, tense, and of infinitely-ordered quantification, can be taken as just a well-formed cluster on a bare grouping of terms and primitive conceptual schemes. However, we are then calling into question every operation in formal logic and mathematics that is treated as primitive, especially those used in "meta-languages," since they appear most prone to introducing their own complexity. More than this follows, though. The primitives are not just the logical operators. Primitive operators are just the most easily targeted and plainly assessed. Even the terms from our ordinary lingo used in explanation or sometimes implementation into our otherwise primitive-mounted formal structure, terms like domain, set, group, proof, implication, predicate, and function all confront this evaluation and reductive effort, since they are so largely used without an explanation of their own, yet permeate so much of what we consider "knowledge" and "proof" of the relations between "semantics" and "syntax" of a logic. Despite contest from some to the contrary, lack of explanation does not imply primitiveness.

Does this remind you of logical atomism? It should! It should also ring of Kant and Schopenhauer's epistemological foundations, but that's just a historical note and point for added reference and personal reminder, not the actual source of inspiration.

At the same time, I'm urging for language-game accounts of proof, where clarity is reached by common efficacy, even at the formal level. I hear that for a Western philosopher, this point may be most controversial, as I'm defying my own muse, acknowledging the difficulties and self-criticism of the Philosophical Investigations, but not accepting one of its major conclusions. I view it not as his error, but his mortality that hindered fuller knowledge of the primitives of the linguistic moods beyond the indicative, and while he honed in on and exhausted the game of the indicative in a matter of years, he only later diagnosed his tunnel vision, laying not another exhaustive treatise, but the groundwork for others to be created. At least I like to think he inspires me in this way. It makes his disagreement with me sound less vehement.

    No comments:

    Post a Comment