5 ms·

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 eas

by jkabrg 8y ago

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 https://en.wikipedia.org/wiki/SKI_combinator_calculus [2] - https://en.wikipedia.org/wiki/Lambda_calculus https://en.wikipedia.org/wiki/Lambda_calculus

scscsc 8y ago
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).
- Sniffnoy 8y ago
  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.
jkabrg 8y ago
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)
- Twisol 8y ago
  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)".
  - pofilat 8y ago
    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)
    - Twisol 8y ago
      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.
drostie 8y ago
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.
pofilat 8y ago
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.

by jkabrg 8y ago

scscsc 8y ago

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).

Sniffnoy 8y ago
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.

jkabrg 8y ago

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)

Twisol 8y ago
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)".
- pofilat 8y ago
  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)
  - Twisol 8y ago
    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.

drostie 8y ago

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.

pofilat 8y ago

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.