Hacker News Reader

Comment by rgovostes | Hacker News Reader

Here is more information on Logic Theorist's improved proof of a theorem in Principia Mathematica:

https://books.google.com/books?id=iYHuBwAAQBAJ&pg=PA52&lpg=P...

For people who don't understand the dots and colons, OP's proposition can be expressed in modern notation as

  ((p V q) -> (p V r)) -> (p V (q -> r))

It's easy to justify this tautology by considering the case when (p) is true and (p) is false.

By contrast, the proof in PM and by LT strike me as highly unintuitive. I guess it's an example of using Hilbert Deduction instead of Natural Deduction, where Natural Deduction is closer to how people normally prove things. For programmers, it's as if they programmed in Combinatory Logic [1] instead of Lambda Calculus[2].

[1] - https://en.wikipedia.org/wiki/SKI_combinator_calculus [2] - https://en.wikipedia.org/wiki/Lambda_calculus

Just to give the proof as a whole in this notation for others, assume (→) has lower precedence than (∨) and is right-associative (i.e. that a → b → c = a → (b → c)):

  Proving: (p ∨ q → p ∨ r) → p ∨ (q → r)
  Start from:
    (x → y) → (y → z) → x → z
  Replace x with q, y with p ∨ q, z with p ∨ r:
    (q → p ∨ q) → (p ∨ q → p ∨ r) → q → p ∨ r
  The first part (q → p ∨ q) is already a known tautology so via modus ponens
    (p ∨ q → p ∨ r) → q → p ∨ r
  Replace the last → with its definition, (a → b) = ¬a ∨ b:
    (p ∨ q → p ∨ r) → ¬q ∨ p ∨ r
  Use the commutative property of (∨):
    (p ∨ q → p ∨ r) → p ∨ ¬q ∨ r
  Then use the definition again:
    (p ∨ q → p ∨ r) → p ∨ (q → r)
  QED.

The first part is also valid in intuitionistic logic and essentially just transforms a known truth `x → y` into "continuation passing style" `∀z. (y → z) → x → z` with a valid result, I think this is why the authors were quite pleased with the proof.

The second half is the shifty bit for intuitionistic logic, going from `q -> Either p r` to `Either p (q -> r)` where it's really easy to see that you could not, say, have a Haskell function of that type generally.

Assuming p V !p (read: p or not p) as an axiom means that you are admitting excluded middle. This axiom is part of "classical propositional logic". So a proof using this case distinction (p true or p false) would be valid, in the classical sense.

There is a stronger system, called "intuitionistic propositional logic", where this axiom is not valid. There are less formulae that are valid intuitionistically, but any formula that is valid intuitionistically is also valid clasically.

There are various philosophical reasons why one prefers intuitionistic logic, but note that in any case it is stronger to have an intuitionistic proof, so these are preferable (when they exist).

The formula ((p V q) -> (p V r)) -> (p V (q -> r)) isn't valid intuitionistically, though (you can get excluded middle from it by taking q=p and r=⊥), so there's no reason to want an intuitionstic proof.

I'll add that the significance of the formula is it's similar to

  a*b + a*c = a*(b + c)

which you ought to remember from school as "factoring/factorization". Except in this case, " * " is replaced with "V", and "+" is replaced with "->". In mathematics, you call that a "distributive law". Some more examples are

  a^c * b^c = (a*b)^c
  p/\q V p/\r = p/\(q V r)
  (pVq) /\ (pVr) = pV(q /\ r)

While you're absolutely right that this is a kind of distributivity, conventionally + is related to "or", * to "and", and ^ to "implies". So the theorem as given would be rendered as something more like "(p + r)^(p + q) implies (p + r^q)".

That's interesting.... + and * theorems correspond between logic and arithmetic, but taking ^ as implication generates theorems that are true in logic but not in arithmetic.

(The truth table of implication is clearly different from binary exxponentiation)

Is it? I checked before commenting (because I also wanted to make sure the arithmetic analogy actually held):

    irb(main):001:0> 0**0
    => 1
    irb(main):002:0> 0**1
    => 0
    irb(main):003:0> 1**0
    => 1
    irb(main):004:0> 1**1
    => 1

Notice that `p -> q` becomes `q^p`, i.e. the operands swap position.

Does natural deduction scale beyond first-order propositional logic with a small number of variables? It seems to me that it would have bad exponential blowup, checking all the cases.

Reply on news.ycombinator.com